A Polymorphic Intermediate Verification Language: Design and Logical Encoding
Conference: Tools and Algorithms for the Construction and Analysis of Systems, 16th International Conference, TACAS 2010, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2010, Paphos, Cyprus, March 20-28, 2010. |
Intermediate languages are a paradigm to separate concerns in software verification systems when bridging the gap between programming languages and the logics understood by theorem provers. While such intermediate languages traditionally only offer rather simple type systems, this paper argues that it is both advantageous and feasible to integrate richer type systems with features like (higher-ranked) polymorphism and quantification over types. As a concrete solution, the paper presents the type system of Boogie 2, an intermediate verification language that is used in several program verifiers. The paper gives two encodings of types and formulae in simply typed logic such that SMT solvers and other theorem provers can be used to discharge verification conditions.