Property directed equivalence via abstract simulation

DOI10.1007/978-3-319-41540-6_24zbMATH Open1411.68065OpenAlexW2498229092MaRDI QIDQ4633561FDOQ4633561

Authors: Grigory Fedyukovich, Arie Gurfinkel, Natasha Sharygina 

Publication date: 3 May 2019

Published in: Computer Aided Verification (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/978-3-319-41540-6_24

Recommendations

• Automated discovery of simulation between programs
• Relational verification via invariant-guided synchronization
• Property-directed incremental invariant generation
• Incremental verification using trace abstraction
• Property-directed inference of universal invariants or proving their absence

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 (8)

• Predicate pairing for program verification
• Incremental and modular context-sensitive analysis
• SMT-based verification of program changes through summary repair
• Relational verification via invariant-guided synchronization
• Learning inductive invariants by sampling from frequency distributions
• Automated discovery of simulation between programs
• Maximizing branch coverage with constrained Horn clauses
• Lockstep composition for unbalanced loops

This page was built for publication: Property directed equivalence via abstract simulation

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