SAT-Based Model Checking
From MaRDI portal
Publication:3176368
DOI10.1007/978-3-319-10575-8_10zbMath1392.68232OpenAlexW2803222079MaRDI QIDQ3176368
Publication date: 20 July 2018
Published in: Handbook of Model Checking (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1007/978-3-319-10575-8_10
Lua error in Module:PublicationMSCList at line 37: attempt to index local 'msc_result' (a nil value).
Related Items (4)
Satisfiability Modulo Theories ⋮ Abstraction and Abstraction Refinement ⋮ Interpolation and Model Checking ⋮ Combining Model Checking and Deduction
Uses Software
Cites Work
- Simulating circuit-level simplifications on CNF
- Planning as satisfiability: heuristics
- Exploiting step semantics for efficient bounded model checking of asynchronous systems
- Context-aware counter abstraction
- Reducing concurrent analysis under a context bound to sequential analysis
- Reasoning about infinite computations
- Predicate abstraction of ANSI-C programs using SAT
- Verification of SpecC using predicate abstraction
- Decision procedures. An algorithmic point of view. With foreword by Randal E. Bryant
- Understanding IC3
- Generalized Property Directed Reachability
- Numeric Bounds Analysis with Conflict-Driven Learning
- Abstract conflict driven learning
- SAT-Based Model Checking without Unrolling
- Beyond Quantifier-Free Interpolation in Extensions of Presburger Arithmetic
- Strengthening Induction-Based Race Checking with Lightweight Static Analysis
- Linear Completeness Thresholds for Bounded Model Checking
- Temporal Logic and Fair Discrete Systems
- Satisfiability Modulo Theories
- Interpolation and Model Checking
- Predicate Abstraction for Program Verification
- Model Checking Concurrent Programs
- Functional Specification of Hardware via Temporal Logic
- Abstractions from proofs
- Counterexample-guided abstraction refinement for symbolic model checking
- Solving SAT and SAT Modulo Theories
- Loop Summarization Using Abstract Transformers
- Simplify: a theorem prover for program checking
- Natural Domain SMT: A Preliminary Assessment
- Applying Logic Synthesis for Speeding Up SAT
- Symbolic Counter Abstraction for Concurrent Software
- Monotonic Partial Order Reduction: An Optimal Symbolic Partial Order Reduction Technique
- Graph-Based Algorithms for Boolean Function Manipulation
- Symbolic execution and program testing
- Interpolating Quantifier-Free Presburger Arithmetic
- Tools and Algorithms for the Construction and Analysis of Systems
- Tools and Algorithms for the Construction and Analysis of Systems
- Linear Encodings of Bounded LTL Model Checking
- Computer Aided Verification
- Computer Aided Verification
- Computer Aided Verification
- Computer Aided Verification
- Theory and Applications of Satisfiability Testing
- Regular canonical systems
- SAT-Based Scalable Formal Verification Solutions
- Delay-bounded scheduling
- On interference abstractions
- Invariant Synthesis for Combined Theories
- Formal Methods in Computer-Aided Design
- Formal Methods in Computer-Aided Design
- Tools and Algorithms for the Construction and Analysis of Systems
- Tools and Algorithms for the Construction and Analysis of Systems
- Computer Aided Verification
- Computer Aided Verification
- Computer Aided Verification
- An Interpolating Sequent Calculus for Quantifier-Free Presburger Arithmetic
- Bounded Model Checking for Weak Alternating Büchi Automata
- Deciding Bit-Vector Arithmetic with Abstraction
- Tools and Algorithms for the Construction and Analysis of Systems
- Tools and Algorithms for the Construction and Analysis of Systems
- Computer Aided Verification
- Reachability analysis of pushdown automata: Application to model-checking
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
This page was built for publication: SAT-Based Model Checking
