Exploiting partial variable assignment in interpolation-based model checking
From MaRDI portal
Publication:2009611
DOI10.1007/s10703-019-00342-zzbMath1425.68257OpenAlexW2985349785MaRDI QIDQ2009611
Leonardo Alt, Antti E. J. Hyvärinen, Jan Kofroň, Grigory Fedyukovich, Natasha Sharygina, Pavel Jančík
Publication date: 29 November 2019
Published in: Formal Methods in System Design (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1007/s10703-019-00342-z
Specification and verification (program logics, model checking, etc.) (68Q60) Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.) (68T20) Interpolation, preservation, definability (03C40)
Uses Software
Cites Work
- Unnamed Item
- PeRIPLO
- Computer aided verification. 24th international conference, CAV 2012, Berkeley, CA, USA, July 7--13, 2012. Proceedings
- Resolution proof transformation for compression and interpolation
- On recursion-free Horn clauses and Craig interpolation
- Optimization techniques for Craig interpolant compaction in unbounded model checking
- Fast interpolating BMC
- OpenSMT2: An SMT Solver for Multi-core and Cloud Computing
- PeRIPLO: A Framework for Producing Effective Interpolants in SAT-Based Software Verification
- Whale: An Interpolation-Based Algorithm for Inter-procedural Verification
- From Under-Approximations to Over-Approximations and Back
- Three uses of the Herbrand-Gentzen theorem in relating model theory and proof theory
- Interpolant Strength
- Lower bounds for resolution and cutting plane proofs and monotone computations
- Interpolation Properties and SAT-Based Model Checking
- eVolCheck: Incremental Upgrade Checker for C
- An Efficient and Flexible Approach to Resolution Proof Reduction
- Theory and Applications of Satisfiability Testing
- Lazy Abstraction with Interpolants
- Computer Aided Verification
This page was built for publication: Exploiting partial variable assignment in interpolation-based model checking
