Modular Verification of Procedure Equivalence in the Presence of Memory Allocation
From MaRDI portal
Publication:2988675
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
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 (1)
Uses Software
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
