Verification Condition Generation Via Theorem Proving

DOI10.1007/11916277_25MaRDI QIDQ5387904zbMATH OpenOpenAlexFDO

Authors

Publication date 27 May 2008

Published in Logic for Programming, Artificial Intelligence, and Reasoning (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/11916277_25

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60)

Recommendations

• Building verification condition generators by compositional extension
• A Machine Checked Soundness Proof for an Intermediate Verification Language
• Verification conditions for source-level imperative programs
• Mechanical verification of mutually recursive procedures
• Secure mechanical verification of mutually recursive procedures

Cited in

(14)

• Integrating external deduction tools with ACL2
• VST-Floyd: a separation logic tool to verify correctness of C programs
• Mechanized result verification: An industrial application
• Parameterized synthesis for fragments of first-order logic over data words
• Building verification condition generators by compositional extension
• Effective generation of verification conditions for non-deterministic unstructured programs
• Sound and complete verification condition generator for functional recursive programs
• Function extraction
• Verification conditions for source-level imperative programs
• Highly automated formal proofs over memory usage of assembly code
• Avoiding exponential explosion: generating compact verification conditions
• Transforming programs into recursive functions
• A generic intermediate representation for verification condition generation
• A mechanical analysis of program verification strategies

Describes a project that uses

Uses Software

• ACL2
• StateFlow

This page was built for publication: Verification Condition Generation Via Theorem Proving

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