SAT-Based Model Checking
From MaRDI portal
Recommendations
- Model checking with Boolean Satisfiability
- Bounded model checking using satisfiability solving
- Certifying proofs for SAT-based model checking
- SAT-Based Model Checking without Unrolling
- Efficient SAT-based bounded model checking for software verification
- Theory and Applications of Models of Computation
- SAT-based explicit \(\mathsf{LTL}_f\) satisfiability checking
Cites work
- Abstract conflict driven learning
- Abstractions from proofs
- An interpolating sequent calculus for quantifier-free Presburger arithmetic
- Applying Logic Synthesis for Speeding Up SAT
- Beyond quantifier-free interpolation in extensions of Presburger arithmetic
- BMC via on-the-fly determinization
- Bounded Model Checking for Weak Alternating Büchi Automata
- Computer Aided Verification
- Computer Aided Verification
- Computer Aided Verification
- Computer Aided Verification
- Computer Aided Verification
- Computer Aided Verification
- Computer Aided Verification
- Computing over-approximations with bounded model checking
- Context-aware counter abstraction
- Counterexample-guided abstraction refinement for symbolic model checking
- Deciding Bit-Vector Arithmetic with Abstraction
- Decision procedures. An algorithmic point of view. With foreword by Randal E. Bryant
- Delay-bounded scheduling
- Exploiting step semantics for efficient bounded model checking of asynchronous systems
- Formal Methods in Computer-Aided Design
- Formal Methods in Computer-Aided Design
- Functional specification of hardware via temporal logic
- Generalized property directed reachability
- Graph-Based Algorithms for Boolean Function Manipulation
- scientific article; zbMATH DE number 1629965 (Why is no real title available?)
- scientific article; zbMATH DE number 1670555 (Why is no real title available?)
- scientific article; zbMATH DE number 1701764 (Why is no real title available?)
- scientific article; zbMATH DE number 1799521 (Why is no real title available?)
- scientific article; zbMATH DE number 1232241 (Why is no real title available?)
- scientific article; zbMATH DE number 734956 (Why is no real title available?)
- scientific article; zbMATH DE number 1953038 (Why is no real title available?)
- scientific article; zbMATH DE number 1956569 (Why is no real title available?)
- scientific article; zbMATH DE number 1903351 (Why is no real title available?)
- scientific article; zbMATH DE number 1903357 (Why is no real title available?)
- scientific article; zbMATH DE number 5493266 (Why is no real title available?)
- scientific article; zbMATH DE number 3313427 (Why is no real title available?)
- Interpolating quantifier-free Presburger arithmetic
- Interpolation and model checking
- Interpolation and SAT-based model checking.
- Invariant Synthesis for Combined Theories
- Lazy satisfiability modulo theories
- Linear completeness thresholds for bounded model checking
- Linear Encodings of Bounded LTL Model Checking
- Loop Summarization Using Abstract Transformers
- Making the most of BMC counterexamples
- Model checking
- Model checking concurrent programs
- Monotonic Partial Order Reduction: An Optimal Symbolic Partial Order Reduction Technique
- Natural domain SMT: a preliminary assessment
- Numeric bounds analysis with conflict-driven learning
- On interference abstractions
- Planning as satisfiability: heuristics
- Predicate abstraction for program verification
- Predicate abstraction of ANSI-C programs using SAT
- Reachability analysis of pushdown automata: Application to model-checking
- Reasoning about infinite computations
- Reducing concurrent analysis under a context bound to sequential analysis
- Regular canonical systems
- SAT-Based Model Checking without Unrolling
- SAT-Based Scalable Formal Verification Solutions
- Satisfiability modulo theories
- Simplify: a theorem prover for program checking
- Simulating circuit-level simplifications on CNF
- Solving SAT and SAT modulo theories, from an abstract Davis-Putnam-Logemann-Loveland procedure to \(\operatorname{DPLL}(T)\)
- Strengthening induction-based race checking with lightweight static analysis
- Symbolic Counter Abstraction for Concurrent Software
- Symbolic execution and program testing
- Temporal logic and fair discrete systems
- Termination criteria for bounded model checking: extensions and comparison
- Theory and Applications of Satisfiability Testing
- Tools and Algorithms for the Construction and Analysis of Systems
- Tools and Algorithms for the Construction and Analysis of Systems
- Tools and Algorithms for the Construction and Analysis of Systems
- Tools and Algorithms for the Construction and Analysis of Systems
- Tools and Algorithms for the Construction and Analysis of Systems
- Tools and Algorithms for the Construction and Analysis of Systems
- Understanding IC3
- Verification of SpecC using predicate abstraction
Cited in
(35)- Accelerating bounded model checking of safety properties
- Optimized SAT encoding of conformance checking artefacts
- Model checking of concurrent software systems via heuristic-guided SAT solving
- scientific article; zbMATH DE number 1670796 (Why is no real title available?)
- A BMC-formulation for the scheduling problem in highly constrained hardware systems
- Supporting SAT based BMC on finite path models
- Computing over-approximations with bounded model checking
- An incremental algorithm to check satisfiability for bounded model checking
- Parallel SAT solving in bounded model checking
- SAT-Based Model Checking without Unrolling
- Satisfiability modulo theories
- Abstraction and abstraction refinement
- Interpolation and model checking
- Combining Model Checking and Deduction
- Formalization of Abstract State Transition Systems for SAT
- Model checking with Boolean Satisfiability
- COMPLETE SAT-BASED MODEL CHECKING FOR CONTEXT-FREE PROCESSES
- scientific article; zbMATH DE number 2087634 (Why is no real title available?)
- scientific article; zbMATH DE number 1852147 (Why is no real title available?)
- Computer Aided Verification
- SAT-BASED MODEL CHECKING FOR REGION AUTOMATA
- Formal Methods in Computer-Aided Design
- Tools and Algorithms for the Construction and Analysis of Systems
- ZB 2005: Formal Specification and Development in Z and B
- Theory and Applications of Models of Computation
- Model Checking Software
- Formal Methods for Hardware Verification
- Bounded model checking and induction: From refutation to verification (extended abstract, Category A)
- Of temporary coalitions in terms of concurrent game models, announcements, and temporal projection
- Using execution logs for improving pseudo-Boolean propagation
- Speeding up pseudo-Boolean propagation
- Improving and understanding the power of satisfaction-driven clause learning
- SAT-based bounded model checking for propositional projection temporal logic
- Certifying incremental SAT solving
- Looking for signs: reasoning about FOBNNs using SAT
Describes a project that uses
Uses Software
This page was built for publication: SAT-Based Model Checking
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3176368)
