Decision procedures. An algorithmic point of view. With foreword by Randal E. Bryant

zbMath1149.68071MaRDI QIDQ2473386

Ofer Strichman, Daniel Kroening

Publication date: 27 February 2008

Published in: Texts in Theoretical Computer Science. An EATCS Series (Search for Journal in Brave)

zbMATH Keywords

first-order theorypropositional logicdecision algorithms

Mathematics Subject Classification ID

Related Items (57)

A layered algorithm for quantifier elimination from linear modular constraints ⋮ Partial Order Reduction for Deep Bug Finding in Synchronous Hardware ⋮ Decision Procedures for Region Logic ⋮ Labelled interpolation systems for hyper-resolution, clausal, and local proofs ⋮ Semantically-guided goal-sensitive reasoning: model representation ⋮ Conflict-driven satisfiability for theory combination: lemmas, modules, and proofs ⋮ Targeted and contextual redescription set exploration ⋮ Mining Backbone Literals in Incremental SAT ⋮ Propositional SAT Solving ⋮ SAT-Based Model Checking ⋮ Satisfiability Modulo Theories ⋮ Integrating Simplex with Tableaux ⋮ Data abstraction: a general framework to handle program verification of data structures ⋮ Satisfiability Checking: Theory and Applications ⋮ Metalevel algorithms for variant satisfiability ⋮ An Impossible Asylum ⋮ Regular model checking revisited ⋮ Propagation based local search for bit-precise reasoning ⋮ Equality detection for linear arithmetic constraints ⋮ Experiments with automated reasoning in the class ⋮ Synthesising programs with non-trivial constants ⋮ Matching Multiplications in Bit-Vector Formulas ⋮ Some results on parametric temporal logic ⋮ A pearl on SAT and SMT solving in Prolog ⋮ Towards a notion of unsatisfiable and unrealizable cores for LTL ⋮ Unnamed Item ⋮ Superposition as a decision procedure for timed automata ⋮ Preface to the special issue ``SI: satisfiability modulo theories ⋮ Abstract interpretation of microcontroller code: intervals meet congruences ⋮ Satisfiability in composition-nominative logics ⋮ Region analysis for deductive verification of C programs ⋮ SLAP: specification logic of actions with probability ⋮ An approach to multicore parallelism using functional programming: a case study based on Presburger arithmetic ⋮ Runtime verification of embedded real-time systems ⋮ On logical bifurcation diagrams ⋮ Complexity of fixed-size bit-vector logics ⋮ Fixed points, Nash equilibria, and the existential theory of the reals ⋮ Symbolic trajectory evaluation for word-level verification: theory and implementation ⋮ Experience of improving the BLAST static verification tool ⋮ Loop invariants ⋮ Sharpening constraint programming approaches for bit-vector theory ⋮ Volume Computation for Boolean Combination of Linear Arithmetic Constraints ⋮ IPL: an integration property language for multi-model cyber-physical systems ⋮ Mutation-Based Test Case Generation for Simulink Models ⋮ Time-budgeting: a component based development methodology for real-time embedded systems ⋮ Transfer Function Synthesis without Quantifier Elimination ⋮ Predicate Generation for Learning-Based Quantifier-Free Loop Invariant Inference ⋮ Range and Set Abstraction using SAT ⋮ $$\mathsf {SC}^\mathsf{2} $$ : Satisfiability Checking Meets Symbolic Computation ⋮ Colors Make Theories Hard ⋮ On the Generation of Positivstellensatz Witnesses in Degenerate Cases ⋮ Virtual Substitution for SMT-Solving ⋮ Metalevel Algorithms for Variant Satisfiability ⋮ A Survey of Satisfiability Modulo Theory ⋮ Reconstruction of Z3’s Bit-Vector Proofs in HOL4 and Isabelle/HOL ⋮ Wombit: a portfolio bit-vector solver using word-level propagation ⋮ On neural network equivalence checking using SMT solvers

Uses Software

• Quaffle

This page was built for publication: Decision procedures. An algorithmic point of view. With foreword by Randal E. Bryant