Inscriere cercetatori

Daca aveti cont Ad Astra si de Facebook, intrati pe pagina de profil pentru a da dreptul sa va logati pe site doar cu acest buton.

Site nou !

Daca nu va puteti recupera parola (sau aveti alte probleme), scrieti-ne la pagina de contact. Situl vechi se gaseste la adresa


Automatically Verifying Typing Constraints for a Data Processing Language

Domenii publicaţii > Ştiinţe informatice + Tipuri publicaţii > Articol în volumul unei conferinţe

Autori: Michael Backes, Catalin Hritcu, Thorsten Tarrach

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


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