A polymorphic intermediate verification language: design and logical encoding

DOI10.1007/978-3-642-12002-2_26MaRDI QIDQ3557085zbMATH OpenOpenAlexFDO

Authors 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

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

Recommendations

• Verifying Whiley programs with Boogie
• Leveraging compiler intermediate representation for multi- and cross-language verification
• A Machine Checked Soundness Proof for an Intermediate Verification Language
• A generic intermediate representation for verification condition generation
• Integration of a Software Model Checker into Isabelle

Cited in

(11)

• Extending Sledgehammer with SMT solvers
• Verifying Whiley programs with Boogie
• Automating Induction with an SMT Solver
• Identity-Based Cryptosystems and Quadratic Residuosity
• Expressing polymorphic types in a many-sorted language
• Identifying overly restrictive matching patterns in SMT-based program verifiers (extended version)
• Encoding monomorphic and polymorphic types
• A generic intermediate representation for verification condition generation
• Leveraging compiler intermediate representation for multi- and cross-language verification
• Axiomatization of typed first-order logic
• A dynamic logic for unstructured programs with embedded assertions

Describes a project that uses

Uses Software

• Boogie
• ESC/Java
• SIMPLIFY
• Metis

This page was built for publication: A polymorphic intermediate verification language: design and logical encoding

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3557085)