Bounded model checking using satisfiability solving
From MaRDI portal
Publication:5946344
DOI10.1023/A:1011276507260zbMath0985.68038OpenAlexW1819209966WikidataQ55889278 ScholiaQ55889278MaRDI QIDQ5946344
Richard Raimi, Yunshan Zhu, Edmund M. Clarke, Armin Biere
Publication date: 21 May 2002
Published in: Formal Methods in System Design (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1023/a:1011276507260
Formal languages and automata (68Q45) Specification and verification (program logics, model checking, etc.) (68Q60) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85)
Related Items
On certifying the UNSAT result of dynamic symmetry-handling-based SAT solvers ⋮ Verifying Array Manipulating Programs with Full-Program Induction ⋮ versat: A Verified Modern SAT Solver ⋮ Latticed \(k\)-induction with an application to probabilistic programs ⋮ A Polyhedral Abstraction for Petri Nets and its Application to SMT-Based Model Checking ⋮ Bounded model checking of infinite state systems ⋮ Gearing Up for Effective ASP Planning ⋮ Satisfiability Modulo Theories ⋮ Combining Model Checking and Testing ⋮ Transfer of Model Checking to Industrial Practice ⋮ Checking EMTLK properties of timed interpreted systems via bounded model checking ⋮ Solving dependency quantified Boolean formulas using quantifier localization ⋮ A SAT-based approach to unbounded model checking for alternating-time temporal epistemic logic ⋮ Formal assessment of reliability specifications in embedded cyber-physical systems ⋮ The state of SAT ⋮ Design and results of the first satisfiability modulo theories competition (SMT-COMP 2005) ⋮ Incremental bounded model checking for embedded software ⋮ Decidable Fragments of Many-Sorted Logic ⋮ Mining definitions in Kissat with Kittens ⋮ Machine learning and logic: a new frontier in artificial intelligence ⋮ Towards better heuristics for solving bounded model checking problems ⋮ Solving parity games by a reduction to SAT ⋮ A View from the Engine Room: Computational Support for Symbolic Model Checking ⋮ SAT-based verification for timed component connectors ⋮ An explicit transition system construction approach to LTL satisfiability checking ⋮ SMT proof checking using a logical framework ⋮ Incremental preprocessing methods for use in BMC ⋮ Effective use of Boolean satisfiability procedures in the formal verification of superscalar and VLIW microprocessors. ⋮ Using Bounded Model Checking to Verify Consensus Algorithms ⋮ Verification of consensus algorithms using satisfiability solving ⋮ Truth Assignments as Conditional Autarkies ⋮ Approximate Automata for Omega-Regular Languages ⋮ Bounded semantics ⋮ Static analysis and stochastic search for reachability problem ⋮ Design and results of the 2nd annual satisfiability modulo theories competition (SMT-COMP 2006) ⋮ Decomposing SAT Instances with Pseudo Backbones ⋮ Visualizing SAT instances and runs of the DPLL algorithm ⋮ On relative and probabilistic finite counterability ⋮ The complexity of identifying characteristic formulae ⋮ Unnamed Item ⋮ Scalable and precise refinement of cache timing analysis via path-sensitive verification ⋮ CPBPV: a constraint-programming framework for bounded program verification ⋮ First-order logical filtering ⋮ Extending Clause Learning of SAT Solvers with Boolean Gröbner Bases ⋮ Proving Stabilization of Biological Systems ⋮ Efficient bounded model checking of heap-manipulating programs using tight field bounds ⋮ Bounded model checking for hyperproperties ⋮ Strong extension-free proof systems ⋮ Learning Rate Based Branching Heuristic for SAT Solvers ⋮ Dependency Schemes for DQBF ⋮ Non-clausal redundancy properties ⋮ Runtime Verification of Component-Based Systems ⋮ Stable models and difference logic ⋮ Computing properties of stable configurations of thermodynamic binding networks ⋮ Dynamic Exploration of Multi-agent Systems with Periodic Timed Tasks ⋮ 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 ⋮ An automata-theoretic approach to model-checking systems and specifications over infinite data domains ⋮ Engineering an Incremental ASP Solver ⋮ Terminal satisfiability in GSTE ⋮ Covered clauses are not propagation redundant ⋮ A sharp threshold for the renameable-Horn and the \(q\)-Horn properties ⋮ The (D)QBF Preprocessor HQSpre – Underlying Theory and Its Implementation1 ⋮ Unrestricted vs restricted cut in a tableau method for Boolean circuits ⋮ On the combination of polyhedral abstraction and SMT-based model checking for Petri nets ⋮ DiMo -- discrete modelling using propositional logic
Uses Software
