Computer Aided Verification

DOI10.1007/b11831zbMath1278.68184OpenAlexW1571340194MaRDI QIDQ5900666

Publication date: 20 April 2010

Published in: Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/b11831

Mathematics Subject Classification ID

Symbolic computation and algebraic computation (68W30) Specification and verification (program logics, model checking, etc.) (68Q60) Interpolation, preservation, definability (03C40)

Related Items

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 ⋮ Living without Beth and Craig: Definitions and Interpolants in Description and Modal Logics with Nominals and Role Inclusions ⋮ Interpolation with guided refinement: revisiting incrementality in SAT-based unbounded model checking ⋮ Invariant inference with provable complexity from the monotone theory ⋮ SAT-based invariant inference and its relation to concept learning ⋮ Complete instantiation-based interpolation ⋮ A multiple-valued logic approach to the design and verification of hardware circuits ⋮ Configurable verification of timed automata with discrete variables ⋮ Software Verification with PDR: An Implementation of the State of the Art ⋮ Partial Order Reduction for Deep Bug Finding in Synchronous Hardware ⋮ Whale: An Interpolation-Based Algorithm for Inter-procedural Verification ⋮ Splitting via Interpolants ⋮ Labelled interpolation systems for hyper-resolution, clausal, and local proofs ⋮ Proof tree preserving tree interpolation ⋮ Interpolation systems for ground proofs in automated deduction: a survey ⋮ Latticed \(k\)-induction with an application to probabilistic programs ⋮ Craig Interpolation in the Presence of Non-linear Constraints ⋮ Mining Backbone Literals in Incremental SAT ⋮ Propositional SAT Solving ⋮ SAT-Based Model Checking ⋮ Satisfiability Modulo Theories ⋮ Interpolation and Model Checking ⋮ Transfer of Model Checking to Industrial Practice ⋮ SAT-solving in practice, with a tutorial example from supervisory control ⋮ Sharper and Simpler Nonlinear Interpolants for Program Verification ⋮ Temporal Logic Verification for Delay Differential Equations ⋮ Incremental design-space model checking via reusable reachable state approximations ⋮ Loop verification with invariants and contracts ⋮ An institution-independent proof of the Robinson consistency theorem ⋮ Constraint solving for interpolation ⋮ Craig interpolation with clausal first-order tableaux ⋮ Optimization techniques for Craig interpolant compaction in unbounded model checking ⋮ HRELTL: a temporal logic for hybrid systems ⋮ Complete SAT-Based Model Checking for Context-Free Processes ⋮ Counterexample Validation and Interpolation-Based Refinement for Forest Automata ⋮ IC3 - Flipping the E in ICE ⋮ A View from the Engine Room: Computational Support for Symbolic Model Checking ⋮ A unifying view on SMT-based software verification ⋮ 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 ⋮ An explicit transition system construction approach to LTL satisfiability checking ⋮ Cyclic Boolean circuits ⋮ A learning-based approach to synthesizing invariants for incomplete verification engines ⋮ SMT proof checking using a logical framework ⋮ Benchmarking a model checker for algorithmic improvements and tuning for performance ⋮ Incremental preprocessing methods for use in BMC ⋮ Interpolants for Linear Arithmetic in SMT ⋮ Automatic verification of reduction techniques in higher order logic ⋮ Learning inductive invariants by sampling from frequency distributions ⋮ Resolution proof transformation for compression and interpolation ⋮ Quantifier elimination by dependency sequents ⋮ Quantifier-free encoding of invariants for hybrid systems ⋮ Planning as satisfiability: parallel plans and algorithms for plan search ⋮ Generalized Craig Interpolation for Stochastic Boolean Satisfiability Problems ⋮ Property-directed incremental invariant generation ⋮ Model checking duration calculus: a practical approach ⋮ Interpolation and amalgamation for arrays with MaxDiff ⋮ Unbounded procedure summaries from bounded environments ⋮ Syntax-guided synthesis for lemma generation in hardware model checking ⋮ Invariant Checking of NRA Transition Systems via Incremental Reduction to LRA with EUF ⋮ Interpolation-Based GR(1) Assumptions Refinement ⋮ Visualizing SAT instances and runs of the DPLL algorithm ⋮ Faster Extraction of High-Level Minimal Unsatisfiable Cores ⋮ Efficient SAT-based bounded model checking for software verification ⋮ On Interpolation in Decision Procedures ⋮ Component-wise incremental LTL model checking ⋮ Parallelizing SMT solving: lazy decomposition and conciliation ⋮ How to deal with unbelievable assertions ⋮ Harald Ganzinger’s Legacy: Contributions to Logics and Programming ⋮ SAT solver management strategies in IC3: an experimental approach ⋮ Rewriting Interpolants ⋮ Exploiting partial variable assignment in interpolation-based model checking ⋮ Interpolation and Symbol Elimination in Vampire ⋮ Interpolant Generation for UTVPI ⋮ Ground Interpolation for Combined Theories ⋮ Interpolation and Symbol Elimination ⋮ Challenges in Constraint-Based Analysis of Hybrid Systems ⋮ Unnamed Item ⋮ Mutation-Based Test Case Generation for Simulink Models ⋮ Approximation Refinement for Interpolation-Based Model Checking ⋮ 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 ⋮ Multicomponent proof-theoretic method for proving interpolation properties ⋮ Efficient Interpolant Generation in Satisfiability Modulo Theories ⋮ Accelerating Interpolation-Based Model-Checking ⋮ SAT-Based Model Checking without Unrolling ⋮ ExplainHoudini: Making Houdini Inference Transparent ⋮ On recursion-free Horn clauses and Craig interpolation ⋮ Efficient generation of small interpolants in CNF ⋮ Quantified data automata for linear data structures: a register automaton model with applications to learning invariants of programs manipulating arrays and lists ⋮ Interpolant Synthesis for Quadratic Polynomial Inequalities and Combination with EUF ⋮ On Interpolation and Symbol Elimination in Theory Extensions ⋮ Deciding Bit-Vector Formulas with mcSAT ⋮ Linear Completeness Thresholds for Bounded Model Checking ⋮ NIL: learning nonlinear interpolants ⋮ Boundary Points and Resolution ⋮ Refinement of Trace Abstraction ⋮ Interpolation in computing science: The semantics of modularization ⋮ Efficient Craig interpolation for linear Diophantine (dis)equations and linear modular equations ⋮ SAT-based explicit LTL reasoning and its application to satisfiability checking ⋮ An interpolating theorem prover ⋮ Interpolant Learning and Reuse in SAT-Based Model Checking ⋮ Accelerated Deletion-based Extraction of Minimal Unsatisfiable Cores ⋮ On interpolation in automated theorem proving