Interpolation and SAT-based model checking.
From MaRDI portal
Recommendations
Cited in
(only showing first 100 items - show all)- Interpolation in computing science: The semantics of modularization
- Efficient Craig interpolation for linear Diophantine (dis)equations and linear modular equations
- Fast interpolating BMC
- A unifying view on SMT-based software verification
- An explicit transition system construction approach to LTL satisfiability checking
- Parallelizing SMT solving: lazy decomposition and conciliation
- Multicomponent proof-theoretic method for proving interpolation properties
- Exploiting partial variable assignment in interpolation-based model checking
- Configurable verification of timed automata with discrete variables
- Incremental design-space model checking via reusable reachable state approximations
- Loop verification with invariants and contracts
- A learning-based approach to synthesizing invariants for incomplete verification engines
- Learning inductive invariants by sampling from frequency distributions
- Interpolation and amalgamation for arrays with MaxDiff
- Unbounded procedure summaries from bounded environments
- Syntax-guided synthesis for lemma generation in hardware model checking
- NIL: learning nonlinear interpolants
- SAT-based explicit LTL reasoning and its application to satisfiability checking
- On interpolation in automated theorem proving
- SMT proof checking using a logical framework
- Planning as satisfiability: parallel plans and algorithms for plan search
- Visualizing SAT instances and runs of the DPLL algorithm
- An interpolating theorem prover
- Craig interpolation with clausal first-order tableaux
- A multiple-valued logic approach to the design and verification of hardware circuits
- Interpolant synthesis for quadratic polynomial inequalities and combination with EUF
- Deciding Bit-Vector Formulas with mcSAT
- Interpolant learning and reuse in SAT-based model checking
- Labelled interpolation systems for hyper-resolution, clausal, and local proofs
- Proof tree preserving tree interpolation
- PeRIPLO: a framework for producing effective interpolants in SAT-based software verification
- Interpolation systems for ground proofs in automated deduction: a survey
- Whale: an interpolation-based algorithm for inter-procedural verification
- Splitting via Interpolants
- Counterexample validation and interpolation-based refinement for forest automata
- IC3 -- flipping the E in ICE
- Generalized Craig interpolation for stochastic Boolean satisfiability problems
- Faster Extraction of High-Level Minimal Unsatisfiable Cores
- On interpolation in decision procedures
- Mutation-Based Test Case Generation for Simulink Models
- SAT-Based Model Checking without Unrolling
- ExplainHoudini: making Houdini inference transparent
- Linear completeness thresholds for bounded model checking
- Craig interpolation in the presence of non-linear constraints
- Propositional SAT solving
- SAT-Based Model Checking
- Satisfiability modulo theories
- Interpolation and model checking
- Transfer of model checking to industrial practice
- Temporal logic verification for delay differential equations
- Selfless interpolation for infinite-state model checking
- Invariant checking of NRA transition systems via incremental reduction to LRA with EUF
- Interpolation-based GR(1) assumptions refinement
- Refinement of Trace Abstraction
- Mining backbone literals in incremental SAT. A new kind of incremental data
- Complete SAT-Based Model Checking for Context-Free Processes
- A View from the Engine Room: Computational Support for Symbolic Model Checking
- Interpolants for Linear Arithmetic in SMT
- Survey on Directed Model Checking
- Computing Optimized Representations for Non-convex Polyhedra by Detection and Removal of Redundant Linear Constraints
- Ground Interpolation for the Theory of Equality
- Boundary Points and Resolution
- Exploiting step semantics for efficient bounded model checking of asynchronous systems
- Exact and fully symbolic verification of linear hybrid automata with large discrete state spaces
- SAT-solving in CSP trace refinement
- Cyclic Boolean circuits
- Benchmarking a model checker for algorithmic improvements and tuning for performance
- Incremental preprocessing methods for use in BMC
- Automatic verification of reduction techniques in higher order logic
- Resolution proof transformation for compression and interpolation
- Quantifier elimination by dependency sequents
- Quantifier-free encoding of invariants for hybrid systems
- Harald Ganzinger's legacy: contributions to logics and programming
- Encoding techniques, Craig interpolants and bounded model checking for incomplete designs
- Accelerated deletion-based extraction of minimal unsatisfiable cores
- Software verification with PDR: an implementation of the state of the art
- Partial order reduction for deep bug finding in synchronous hardware
- Sharper and Simpler Nonlinear Interpolants for Program Verification
- scientific article; zbMATH DE number 7559472 (Why is no real title available?)
- Component-wise incremental LTL model checking
- Interpolation Properties and SAT-Based Model Checking
- Interpolant Generation for UTVPI
- Ground Interpolation for Combined Theories
- Interpolation and Symbol Elimination
- Challenges in Constraint-Based Analysis of Hybrid Systems
- How to deal with unbelievable assertions
- SAT solver management strategies in IC3: an experimental approach
- Intertwined forward-backward reachability analysis using interpolants
- Rewriting interpolants
- Approximation Refinement for Interpolation-Based Model Checking
- Efficient Interpolant Generation in Satisfiability Modulo Theories
- Accelerating Interpolation-Based Model-Checking
- Interpolation and symbol elimination in Vampire
- Combining Abstraction Refinement and SAT-Based Model Checking
- Complete instantiation-based interpolation
- Constraint solving for interpolation
- SMT-based verification of program changes through summary repair
- Mining definitions in Kissat with Kittens
- Verification Modulo theories
- Interpolation Results for Arrays with Length and MaxDiff
This page was built for publication: Interpolation and SAT-based model checking.
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5900666)
