SAT-Based Model Checking without Unrolling
From MaRDI portal
Publication:3075471
DOI10.1007/978-3-642-18275-4_7zbMath1317.68109MaRDI 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
68Q60: Specification and verification (program logics, model checking, etc.)
Related Items
Satisfiability Checking: Theory and Applications, Boolean satisfiability in quantum compilation, SMT-based verification of data-aware processes: a model-theoretic approach, ICE-based refinement type discovery for higher-order functional programs, Labelled interpolation systems for hyper-resolution, clausal, and local proofs, LCTD: test-guided proofs for C programs on LLVM, Symmetry in Gardens of Eden, Automatic generation of inductive invariants from high-level microarchitectural models of communication fabrics, Resolution proof transformation for compression and interpolation, Quantifier elimination by dependency sequents, Parametrized invariance for infinite state processes, 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, Efficient suspect selection in unreachable state diagnosis, Quantified data automata for linear data structures: a register automaton model with applications to learning invariants of programs manipulating arrays and lists, Optimization techniques for Craig interpolant compaction in unbounded model checking, HRELTL: a temporal logic for hybrid systems, A unifying view on SMT-based software verification, An explicit transition system construction approach to LTL satisfiability checking, Vacuity in practice: temporal antecedent failure, Model-based safety assessment of a triple modular generator with xSAP, Counterexample-guided prophecy for model checking modulo the theory of arrays, SAT-based explicit \(\mathsf{LTL}_f\) satisfiability checking, Certifying proofs for SAT-based model checking, Extracting counterexamples induced by safety violation in linear hybrid systems, A learning-based approach to synthesizing invariants for incomplete verification engines, Learning inductive invariants by sampling from frequency distributions, Counterexample- and simulation-guided floating-point loop invariant synthesis, Unbounded procedure summaries from bounded environments, Syntax-guided synthesis for lemma generation in hardware model checking, SAT-based explicit LTL reasoning and its application to satisfiability checking, Counterexample-preserving reduction for symbolic model checking, Infinite-state invariant checking with IC3 and predicate abstraction, Deciding Bit-Vector Formulas with mcSAT, When Is a Formula a Loop Invariant?, Horn Clause Solvers for Program Verification, Property Directed Reachability for Proving Absence of Concurrent Modification Errors, Dynamic Reductions for Model Checking Concurrent Software, IC3 - Flipping the E in ICE, Propositional SAT Solving, SAT-Based Model Checking, Combining Model Checking and Deduction, Transfer of Model Checking to Industrial Practice, Model Checking Data Flows in Concurrent Network Updates, Mining Backbone Literals in Incremental SAT
Uses Software
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Symbolic model checking: \(10^{20}\) states and beyond
- Counterexample-guided abstraction refinement for symbolic model checking
- Temporal Verification of Reactive Systems: Response
- Applying Logic Synthesis for Speeding Up SAT
- Theory and Applications of Satisfiability Testing
- An axiomatic basis for computer programming
- Theory and Applications of Satisfiability Testing
- Computer Aided Verification
- Computer Aided Verification
