Towards modularly comparing programs using automated theorem provers

DOI10.1007/978-3-642-38574-2_20zbMATH Open1381.68054OpenAlexW26752331MaRDI QIDQ4928447FDOQ4928447

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

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

Mathematics Subject Classification ID

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

Cited In (12)

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

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)