Towards modularly comparing programs using automated theorem provers

DOI10.1007/978-3-642-38574-2_20MaRDI QIDQ4928447zbMATH OpenOpenAlexFDO

Authors Chris Hawblitzel, Ming Kawaguchi, Shuvendu K. Lahiri, Henrique Rebêlo

Publication date 14 June 2013

Published in Automated Deduction – CADE-24 (Search for Journal in Brave)

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

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

• Equivalence checking of two functional programs using inductive theorem provers
• scientific article; zbMATH DE number 177256
• Verifying procedural programs via constrained rewriting induction
• scientific article; zbMATH DE number 176727
• Simplify: a theorem prover for program checking

Cited in

(13)

• Automating regression verification of pointer programs by predicate abstraction
• Relational program reasoning using compiler IR
• Certified verification of relational properties
• Equivalence checking of two functional programs using inductive theorem provers
• Modular verification of procedure equivalence in the presence of memory allocation
• Relational verification via invariant-guided synchronization
• A language-independent proof system for full program equivalence
• Verifying procedural programs via constrained rewriting induction
• Verifying relative safety, accuracy, and termination for program approximations
• Alignment complete relational Hoare logics for some and all
• Proving mutual termination
• Product programs in the wild: retrofitting program verifiers to check information flow security
• Constraint-based relational verification

Describes a project that uses

Uses Software

• z3
• SymDiff

This page was built for publication: Towards modularly comparing programs using automated theorem provers

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