SAT-Based Model Checking without Unrolling

DOI10.1007/978-3-642-18275-4_7zbMath1317.68109OpenAlexW3138459719MaRDI QIDQ3075471

Publication date: 15 February 2011

Published in: Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/978-3-642-18275-4_7

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60)

Related Items (72)

Configurable verification of timed automata with discrete variables ⋮ Improving Generalization in Software IC3 ⋮ Infinite-state invariant checking with IC3 and predicate abstraction ⋮ Software Verification with PDR: An Implementation of the State of the Art ⋮ Partial Order Reduction for Deep Bug Finding in Synchronous Hardware ⋮ Labelled interpolation systems for hyper-resolution, clausal, and local proofs ⋮ Counterexample-Guided Prophecy for Model Checking Modulo the Theory of Arrays ⋮ Latticed \(k\)-induction with an application to probabilistic programs ⋮ A Polyhedral Abstraction for Petri Nets and its Application to SMT-Based Model Checking ⋮ Mining Backbone Literals in Incremental SAT ⋮ Propositional SAT Solving ⋮ SAT-Based Model Checking ⋮ Combining Model Checking and Deduction ⋮ Transfer of Model Checking to Industrial Practice ⋮ Incremental design-space model checking via reusable reachable state approximations ⋮ Satisfiability and synthesis modulo oracles ⋮ LCTD: test-guided proofs for C programs on LLVM ⋮ Satisfiability Checking: Theory and Applications ⋮ When Is a Formula a Loop Invariant? ⋮ Horn Clause Solvers for Program Verification ⋮ Extracting counterexamples induced by safety violation in linear hybrid systems ⋮ Optimization techniques for Craig interpolant compaction in unbounded model checking ⋮ Symmetry in Gardens of Eden ⋮ Mining definitions in Kissat with Kittens ⋮ Verification Modulo theories ⋮ Analysis and Transformation of Constrained Horn Clauses for Program Verification ⋮ Unnamed Item ⋮ Interpolation with guided refinement: revisiting incrementality in SAT-based unbounded model checking ⋮ Level-up -- from bits to words ⋮ Intuitive modelling and formal analysis of collective behaviour in foraging ants ⋮ HRELTL: a temporal logic for hybrid systems ⋮ Process algebras and flocks of birds ⋮ Invariant inference with provable complexity from the monotone theory ⋮ Property Directed Reachability for Proving Absence of Concurrent Modification Errors ⋮ Dynamic Reductions for Model Checking Concurrent Software ⋮ IC3 - Flipping the E in ICE ⋮ Diversifying a parallel SAT solver with Bayesian moment matching ⋮ SAT-based invariant inference and its relation to concept learning ⋮ Solving constrained Horn clauses over algebraic data types ⋮ A unifying view on SMT-based software verification ⋮ An explicit transition system construction approach to LTL satisfiability checking ⋮ A learning-based approach to synthesizing invariants for incomplete verification engines ⋮ Automatic generation of inductive invariants from high-level microarchitectural models of communication fabrics ⋮ Unnamed Item ⋮ SMT-based verification of data-aware processes: a model-theoretic approach ⋮ Learning inductive invariants by sampling from frequency distributions ⋮ Resolution proof transformation for compression and interpolation ⋮ Quantifier elimination by dependency sequents ⋮ Model Checking Data Flows in Concurrent Network Updates ⋮ Counterexample- and simulation-guided floating-point loop invariant synthesis ⋮ Parametrized invariance for infinite state processes ⋮ Unbounded procedure summaries from bounded environments ⋮ Syntax-guided synthesis for lemma generation in hardware model checking ⋮ Complexity of fixed-size bit-vector logics ⋮ State space search nogood learning: online refinement of critical-path dead-end detectors in planning ⋮ SMT-based model checking for recursive programs ⋮ SAT solver management strategies in IC3: an experimental approach ⋮ Vacuity in practice: temporal antecedent failure ⋮ Model-based safety assessment of a triple modular generator with xSAP ⋮ Efficient suspect selection in unreachable state diagnosis ⋮ Counterexample-guided prophecy for model checking modulo the theory of arrays ⋮ SAT-based explicit \(\mathsf{LTL}_f\) satisfiability checking ⋮ ICE-based refinement type discovery for higher-order functional programs ⋮ Quantified data automata for linear data structures: a register automaton model with applications to learning invariants of programs manipulating arrays and lists ⋮ Deciding Bit-Vector Formulas with mcSAT ⋮ Certifying proofs for SAT-based model checking ⋮ Boolean satisfiability in quantum compilation ⋮ SAT-based explicit LTL reasoning and its application to satisfiability checking ⋮ Counterexample-preserving reduction for symbolic model checking ⋮ Zone-based verification of timed automata: extrapolations, simulations and what next? ⋮ On the combination of polyhedral abstraction and SMT-based model checking for Petri nets ⋮ Abstraction-based incremental inductive coverability for Petri nets

Uses Software

Cites Work

This page was built for publication: SAT-Based Model Checking without Unrolling