SMT-based verification of program changes through summary repair
From MaRDI portal
Publication:6056638
DOI10.1007/s10703-023-00423-0MaRDI QIDQ6056638
Natasha Sharygina, Antti E. J. Hyvärinen, Martin Blicha, Sepideh Asadi, Grigory Fedyukovich
Publication date: 30 October 2023
Published in: Formal Methods in System Design (Search for Journal in Brave)
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Proof tree preserving tree interpolation
- Farkas-based tree interpolation
- An interpolating theorem prover
- OpenSMT2: An SMT Solver for Multi-core and Cloud Computing
- Tree Interpolation in Vampire
- PeRIPLO: A Framework for Producing Effective Interpolants in SAT-Based Software Verification
- Whale: An Interpolation-Based Algorithm for Inter-procedural Verification
- Three uses of the Herbrand-Gentzen theorem in relating model theory and proof theory
- Abstractions from proofs
- Satisfiability Modulo Theories: An Appetizer
- Lower bounds for resolution and cutting plane proofs and monotone computations
- Property Directed Equivalence via Abstract Simulation
- Interpolation Properties and SAT-Based Model Checking
- Function Summarization Modulo Theories
- Modular Demand-Driven Analysis of Semantic Difference for Program Versions
- Tools and Algorithms for the Construction and Analysis of Systems
- eVolCheck: Incremental Upgrade Checker for C
- Computer Aided Verification
- Computer Aided Verification
- Exploiting synchrony and symmetry in relational verification
- Incremental verification using trace abstraction
This page was built for publication: SMT-based verification of program changes through summary repair
