Bounded model checking using satisfiability solving
From MaRDI portal
Publication:5946344
DOI10.1023/A:1011276507260zbMath0985.68038WikidataQ55889278 ScholiaQ55889278MaRDI QIDQ5946344
Armin Biere, Richard Raimi, Yunshan Zhu, Edmund M. Clarke
Publication date: 21 May 2002
Published in: Formal Methods in System Design (Search for Journal in Brave)
68Q45: Formal languages and automata
68Q60: Specification and verification (program logics, model checking, etc.)
68Q85: Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.)
Related Items
Engineering an Incremental ASP Solver, Solving parity games by a reduction to SAT, SAT-based verification for timed component connectors, Incremental preprocessing methods for use in BMC, First-order logical filtering, Verification of consensus algorithms using satisfiability solving, Unrestricted vs restricted cut in a tableau method for Boolean circuits, Design and results of the first satisfiability modulo theories competition (SMT-COMP 2005), CPBPV: a constraint-programming framework for bounded program verification, Stable models and difference logic, Hybrid systems: From verification to falsification by combining motion planning and discrete search, On the complexities of selected satisfiability and equivalence queries over Boolean formulas and inclusion queries over hulls, Effective use of Boolean satisfiability procedures in the formal verification of superscalar and VLIW microprocessors., Bounded model checking of infinite state systems, A SAT-based approach to unbounded model checking for alternating-time temporal epistemic logic, Design and results of the 2nd annual satisfiability modulo theories competition (SMT-COMP 2006), Visualizing SAT instances and runs of the DPLL algorithm, A sharp threshold for the renameable-Horn and the \(q\)-Horn properties, The state of SAT, versat: A Verified Modern SAT Solver, Gearing Up for Effective ASP Planning, Proving Stabilization of Biological Systems, Runtime Verification of Component-Based Systems, Decidable Fragments of Many-Sorted Logic, A View from the Engine Room: Computational Support for Symbolic Model Checking, Using Bounded Model Checking to Verify Consensus Algorithms, Extending Clause Learning of SAT Solvers with Boolean Gröbner Bases
Uses Software
