SMT-based verification of program changes through summary repair

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)

zbMATH Keywords

Craig interpolationsymbolic model checkingSMT solvingincremental verificationprogram changes

Mathematics Subject Classification ID

Computer science (68-XX)

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