Automatically Verifying Typing Constraints for a Data Processing Language

Abstract. 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.

• Type: Journal
• Year: 2011
• Where: CPP
• Authors: Michael Backes, Catalin Hritcu, Thorsten Tarrach
• Keywords: Condition Generator, CPP 2011, Interactive Theorem Prover, Prototype Implementation