Autori: Michael Backes, Catalin Hritcu, Thorsten Tarrach

Editorial: Springer, First International Conference on Certified Programs and Proofs (CPP 2011), p.296-313, 2011.

Rezumat:

In this paper we present a new technique for automatically verifying typing
constraints in the setting of Dminor, a first-order data processing language with
refinement types and dynamic type-tests. We achieve this by translating Dminor programs
into a standard while language and then using a general-purpose verification
tool. Our translation generates assertions in the while program that faithfully represent
the sophisticated typing constraints in the original program. We use a generic
verification condition generator together with an SMT solver to prove statically that
these assertions succeed in all executions. We formalise our translation algorithm
using an interactive theorem prover and provide a machine-checkable proof of its
soundness. We provide a prototype implementation using Boogie and Z3 that can
already be used to efficiently verify a large number of test programs.

Cuvinte cheie: type systems, data processing, refinement types, verification conditions, intermediate verification language

URL: http://www.infsec.cs.uni-saarland.de/~hritcu/publications/dverify-cpp2011.pdf