A Polymorphic Intermediate Verification Language: Design and Logical Encoding

DOI10.1007/978-3-642-12002-2_26zbMath1284.68409OpenAlexW1946187443MaRDI QIDQ3557085

K. Rustan M. Leino, Philipp Rümmer

Publication date: 27 April 2010

Published in: Tools and Algorithms for the Construction and Analysis of Systems (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/978-3-642-12002-2_26

Mathematics Subject Classification ID

Logic in computer science (03B70) Specification and verification (program logics, model checking, etc.) (68Q60)

Related Items (8)

Automating Induction with an SMT Solver ⋮ Expressing Polymorphic Types in a Many-Sorted Language ⋮ Encoding Monomorphic and Polymorphic Types ⋮ Extending Sledgehammer with SMT Solvers ⋮ Identity-Based Cryptosystems and Quadratic Residuosity ⋮ A Dynamic Logic for Unstructured Programs with Embedded Assertions ⋮ Axiomatization of Typed First-Order Logic ⋮ Verifying Whiley programs with Boogie

Uses Software

• Metis_
• SIMPLIFY
• ESC/Java
• Boogie

This page was built for publication: A Polymorphic Intermediate Verification Language: Design and Logical Encoding