Property directed equivalence via abstract simulation

DOI10.1007/978-3-319-41540-6_24MaRDI QIDQ4633561zbMATH OpenOpenAlexFDO

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

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

• 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

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)