Modular Verification of Procedure Equivalence in the Presence of Memory Allocation

DOI10.1007/978-3-662-54434-1_35zbMath1485.68077OpenAlexW2591626899MaRDI QIDQ2988675

Tim Wood, Shuvendu K. Lahiri, Sophia Drossopolou, Susan Eisenbach

Publication date: 19 May 2017

Published in: Programming Languages and Systems (Search for Journal in Brave)

Full work available at URL: http://hdl.handle.net/10044/1/43956

zbMATH Keywords

program verificationprogram equivalenceversion-aware verification

Mathematics Subject Classification ID

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

Related Items (2)

Automating regression verification of pointer programs by predicate abstraction ⋮ PEQtest: testing functional equivalence

Uses Software

• Unnamed Item
• z3
• LLVM
• SIMPLIFY
• Boogie
• SymDiff
• CoVaC
• RVT

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Program equivalence in a simple language with state
• Proving mutual termination
• Relational separation logic
• Inference rules for proving the equivalence of recursive procedures
• Fully abstract models of typed \(\lambda\)-calculi
• Abstract models of storage
• A semantic approach to secure information flow
• Regression verification for unbalanced recursive functions
• Product programs and relational program logics
• Abstract Semantic Differencing for Numerical Programs
• Dafny: An Automatic Program Verifier for Functional Correctness
• Relational Decomposition
• Secure information flow by self-composition
• Simple relational correctness proofs for static analyses and program transformations
• Beyond 2-Safety: Asymmetric Product Programs for Relational Program Verification
• Simplify: a theorem prover for program checking
• Abstracting Allocation
• Towards Modularly Comparing Programs Using Automated Theorem Provers
• Small bisimulations for reasoning about higher-order imperative programs
• Verification of Equivalent-Results Methods
• An axiomatic basis for computer programming
• Static Analysis

This page was built for publication: Modular Verification of Procedure Equivalence in the Presence of Memory Allocation