SAT-Based Model Checking without Unrolling
From MaRDI portal
Recommendations
- SAT-Based Model Checking
- scientific article; zbMATH DE number 1903357
- SAT-based unbounded model checking of timed automata
- Bounded model checking using satisfiability solving
- scientific article; zbMATH DE number 1670796
- Formal Methods in Computer-Aided Design
- Efficient SAT-based bounded model checking for software verification
- Constraint LTL satisfiability checking without automata
- SAT-based explicit \(\mathsf{LTL}_f\) satisfiability checking
- Certifying proofs for SAT-based model checking
Cites work
- scientific article; zbMATH DE number 1903357 (Why is no real title available?)
- scientific article; zbMATH DE number 3302923 (Why is no real title available?)
- An axiomatic basis for computer programming
- Applying Logic Synthesis for Speeding Up SAT
- Bounded model checking and induction: From refutation to verification (extended abstract, Category A)
- Counterexample-guided abstraction refinement for symbolic model checking
- Interpolation and SAT-based model checking.
- Symbolic model checking: \(10^{20}\) states and beyond
- Temporal induction by incremental SAT solving
- Temporal verification of reactive systems: response
- Theory and Applications of Satisfiability Testing
- Theory and Applications of Satisfiability Testing
Cited in
(98)- A learning-based approach to synthesizing invariants for incomplete verification engines
- Correct Hardware Design and Verification Methods
- Boolean satisfiability in quantum compilation
- Symmetry in Gardens of Eden
- Hardware and Software, Verification and Testing
- Latticed \(k\)-induction with an application to probabilistic programs
- Process algebras and flocks of birds
- Partial order reduction for deep bug finding in synchronous hardware
- Resolution proof transformation for compression and interpolation
- Shared Certificates for Neural Network Verification
- Zone-based verification of timed automata: extrapolations, simulations and what next?
- Certified SAT solving with GPU accelerated inprocessing
- Model checking data flows in concurrent network updates
- scientific article; zbMATH DE number 7453201 (Why is no real title available?)
- scientific article; zbMATH DE number 7589540 (Why is no real title available?)
- Analysis and Transformation of Constrained Horn Clauses for Program Verification
- ICE-based refinement type discovery for higher-order functional programs
- An explicit transition system construction approach to LTL satisfiability checking
- Abstraction-based incremental inductive coverability for Petri nets
- Counterexample-preserving reduction for symbolic model checking
- Saturation-based incremental LTL model checking with inductive proofs
- Configurable verification of timed automata with discrete variables
- Syntax-guided synthesis for lemma generation in hardware model checking
- Unbounded procedure summaries from bounded environments
- SMT-based verification of data-aware processes: a model-theoretic approach
- IC3 -- flipping the E in ICE
- Labelled interpolation systems for hyper-resolution, clausal, and local proofs
- Dynamic reductions for model checking concurrent software
- Horn clause solvers for program verification
- Propositional SAT solving
- Efficient suspect selection in unreachable state diagnosis
- Interpolation and SAT-based model checking revisited: adoption to software verification
- Vacuity in practice: temporal antecedent failure
- Counterexample-guided prophecy for model checking modulo the theory of arrays
- Certifying proofs for SAT-based model checking
- The Lattice-Theoretic Essence of Property Directed Reachability Analysis
- On the combination of polyhedral abstraction and SMT-based model checking for Petri nets
- Diversifying a parallel SAT solver with Bayesian moment matching
- SAT-based invariant inference and its relation to concept learning
- RAT elimination
- Reasoning with propositional logic: from SAT solvers to knowledge compilation
- Counterexample- and simulation-guided floating-point loop invariant synthesis
- Model-based safety assessment of a triple modular generator with xSAP
- Automatic generation of inductive invariants from high-level microarchitectural models of communication fabrics
- Software verification with PDR: an implementation of the state of the art
- Solving constrained Horn clauses over algebraic data types
- Mining definitions in Kissat with Kittens
- Certifying phase abstraction
- Transfer of model checking to industrial practice
- Incremental design-space model checking via reusable reachable state approximations
- Optimization techniques for Craig interpolant compaction in unbounded model checking
- Satisfiability and synthesis modulo oracles
- Property Directed Reachability for Proving Absence of Concurrent Modification Errors
- Verification Modulo theories
- Interpolation with guided refinement: revisiting incrementality in SAT-based unbounded model checking
- Deciding Bit-Vector Formulas with mcSAT
- HRELTL: a temporal logic for hybrid systems
- LCTD: test-guided proofs for C programs on LLVM
- Invariant inference with provable complexity from the monotone theory
- Quantifier elimination by dependency sequents
- Satisfiability checking: theory and applications
- SAT-Based Model Checking
- COMPLETE SAT-BASED MODEL CHECKING FOR CONTEXT-FREE PROCESSES
- Invariant checking for SMT-based systems with quantifiers
- Counterexample-Guided Prophecy for Model Checking Modulo the Theory of Arrays
- A Polyhedral Abstraction for Petri Nets and its Application to SMT-Based Model Checking
- Data-driven Numerical Invariant Synthesis with Automatic Generation of Attributes
- Extracting counterexamples induced by safety violation in linear hybrid systems
- When is a formula a loop invariant?
- Learning inductive invariants by sampling from frequency distributions
- Parametrized invariance for infinite state processes
- Combining Model Checking and Deduction
- Mining backbone literals in incremental SAT. A new kind of incremental data
- Complexity of fixed-size bit-vector logics
- Infinite-state invariant checking with IC3 and predicate abstraction
- \textsc{Golem}: a flexible and efficient solver for constrained Horn clauses
- Global guidance for local generalization in model checking
- Improving Generalization in Software IC3
- Distributed bounded model checking
- A unifying view on SMT-based software verification
- SAT-based explicit \(\mathsf{LTL}_f\) satisfiability checking
- Level-up -- from bits to words
- Exploiting adjoints in property directed reachability analysis
- Inferring invariants with quantifier alternations: taming the search space explosion
- Partial quantifier elimination and property generation
- Property directed reachability for generalized Petri nets
- Towards an automatic proof of the bakery algorithm
- Searching for i-good lemmas to accelerate safety model checking
- Solving string constraints using SAT
- The \textsc{Golem} Horn solver
- Searching for ribbon-shaped paths in fair transition systems
- \textsc{Sorcar}: property-driven algorithms for learning conjunctive invariants
- State space search nogood learning: online refinement of critical-path dead-end detectors in planning
- SMT-based model checking for recursive programs
- Intuitive modelling and formal analysis of collective behaviour in foraging ants
- Quantified data automata for linear data structures: a register automaton model with applications to learning invariants of programs manipulating arrays and lists
- SAT-based explicit LTL reasoning and its application to satisfiability checking
- SAT solver management strategies in IC3: an experimental approach
This page was built for publication: SAT-Based Model Checking without Unrolling
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3075471)
