Lattice-based refinement in bounded model checking
From MaRDI portal
Publication:1629959
DOI10.1007/978-3-030-03592-1_4zbMath1403.68123OpenAlexW2901895042MaRDI QIDQ1629959
Karine Even-Mendoza, Natasha Sharygina, Sepideh Asadi, Antti E. J. Hyvärinen, Hana Chockler
Publication date: 7 December 2018
Full work available at URL: https://doi.org/10.1007/978-3-030-03592-1_4
Cites Work
- Theory refinement for program verification
- SMTCoq: a plug-in for integrating SMT solvers into Coq
- Satisfiability modulo transcendental functions via incremental linearization
- OpenSMT2: An SMT Solver for Multi-core and Cloud Computing
- PeRIPLO: A Framework for Producing Effective Interpolants in SAT-Based Software Verification
- Three uses of the Herbrand-Gentzen theorem in relating model theory and proof theory
- Invariant Checking of NRA Transition Systems via Incremental Reduction to LRA with EUF
- Counterexample-guided abstraction refinement for symbolic model checking
- Simplify: a theorem prover for program checking
- Interpolant Strength
- Systematic design of program transformation frameworks by abstract interpretation
- Tools and Algorithms for the Construction and Analysis of Systems
- Making abstract interpretations complete
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
This page was built for publication: Lattice-based refinement in bounded model checking
