A generic intermediate representation for verification condition generation

DOI10.1007/978-3-319-27436-2_14MaRDI QIDQ5743596zbMATH OpenOpenAlexFDO

Authors Manuel Montenegro, Jaime Sánchez-Hernández, Ricardo Peña

Publication date 5 February 2016

Published in Logic-Based Program Synthesis and Transformation (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-319-27436-2_14

zbMATH Keywords

intermediate representationprogram transformationverification conditionsverification platforms

Mathematics Subject Classification ID

Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Specification and verification (program logics, model checking, etc.) (68Q60)

Recommendations

• Verification conditions for source-level imperative programs
• Verification Condition Generation Via Theorem Proving
• Building verification condition generators by compositional extension
• A Machine Checked Soundness Proof for an Intermediate Verification Language
• A polymorphic intermediate verification language: design and logical encoding

Cites work

• scientific article; zbMATH DE number 2090729 (Why is no real title available?)
• Introduction to algorithms.
• One logic to use them all
• Why3 -- where programs meet provers

Cited in

(2)

• Building verification condition generators by compositional extension
• A polymorphic intermediate verification language: design and logical encoding

Describes a project that uses

Uses Software

• GHC
• CVC4
• WhyML
• z3
• Why3
• OCaml
• KeY

This page was built for publication: A generic intermediate representation for verification condition generation

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