A Generic Intermediate Representation for Verification Condition Generation

DOI10.1007/978-3-319-27436-2_14zbMath1473.68051OpenAlexW2294420626MaRDI QIDQ5743596

Jaime Sánchez-Hernández, Manuel Montenegro, 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

program transformationintermediate representationverification conditionsverification platforms

Mathematics Subject Classification ID

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

Uses Software

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

Cites Work

• One Logic to Use Them All
• Why3 — Where Programs Meet Provers
• Unnamed Item
• Unnamed Item

This page was built for publication: A Generic Intermediate Representation for Verification Condition Generation