Decision procedures. An algorithmic point of view. With foreword by Randal E. Bryant
From MaRDI portal
Publication:2473386
zbMATH Open1149.68071MaRDI QIDQ2473386FDOQ2473386
Authors: Daniel Kroening, Ofer Strichman 
Publication date: 27 February 2008
Published in: Texts in Theoretical Computer Science. An EATCS Series (Search for Journal in Brave)
Recommendations
- Decision procedures. An algorithmic point of view
- Book review of: Daniel Kroening and Ofer Strichman, Decision procedures: an algorithmic point of view
- Book review of: D. Kroening and O. Strichman, Decision procedures. An algorithmic point of view. 2nd ed.
- scientific article; zbMATH DE number 1071873
- Decision algorithms for some fragments of analysis and related areas
- scientific article; zbMATH DE number 1455133
- Axioms for a Class of Algorithms of Sequential Decision Making
- Optimal decision processes and algorithms
- On the Asymptotic Behavior of Decision Procedures
Research exposition (monographs, survey articles) pertaining to computer science (68-02) Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.) (68T20) Introductory exposition (textbooks, tutorial papers, etc.) pertaining to computer science (68-01) Logic in artificial intelligence (68T27)
Cited In (62)
- Title not available (Why is that?)
- Partial order reduction for deep bug finding in synchronous hardware
- An Impossible Asylum
- Reasoning on data words over numeric domains
- Mining backbone literals in incremental SAT. A new kind of incremental data
- Experiments with automated reasoning in the class
- Decision procedures for sequence theories
- Synthesising programs with non-trivial constants
- Conflict-driven satisfiability for theory combination: lemmas, modules, and proofs
- Virtual substitution for SMT-solving
- Preface to the special issue ``SI: satisfiability modulo theories
- Abstract interpretation of microcontroller code: intervals meet congruences
- Towards a notion of unsatisfiable and unrealizable cores for LTL
- On neural network equivalence checking using SMT solvers
- Wombit: a portfolio bit-vector solver using word-level propagation
- Metalevel algorithms for variant satisfiability
- SLAP: specification logic of actions with probability
- On logical bifurcation diagrams
- Volume Computation for Boolean Combination of Linear Arithmetic Constraints
- A pearl on SAT and SMT solving in Prolog
- Labelled interpolation systems for hyper-resolution, clausal, and local proofs
- Semantically-guided goal-sensitive reasoning: model representation
- Targeted and contextual redescription set exploration
- Matching multiplications in bit-vector formulas
- Propositional SAT solving
- IPL: an integration property language for multi-model cyber-physical systems
- Region analysis for deductive verification of C programs
- Experience of improving the BLAST static verification tool
- Loop invariants: analysis, classification, and examples
- Data abstraction: a general framework to handle program verification of data structures
- Range and set abstraction using SAT
- Predicate Generation for Learning-Based Quantifier-Free Loop Invariant Inference
- Regular model checking revisited
- Equality detection for linear arithmetic constraints
- Colors Make Theories Hard
- Satisfiability checking: theory and applications
- Reconstruction of Z3's bit-vector proofs in HOL4 and Isabelle/HOL
- SAT-Based Model Checking
- A survey of satisfiability modulo theory
- Satisfiability modulo theories
- An approach to multicore parallelism using functional programming: a case study based on Presburger arithmetic
- Runtime verification of embedded real-time systems
- Decision procedures for region logic
- Satisfiability in composition-nominative logics
- Time-budgeting: a component based development methodology for real-time embedded systems
- Some results on parametric temporal logic
- Transfer function synthesis without quantifier elimination
- Mutation-Based Test Case Generation for Simulink Models
- A layered algorithm for quantifier elimination from linear modular constraints
- Superposition as a decision procedure for timed automata
- Propagation based local search for bit-precise reasoning
- Computer Aided Verification
- Complexity of fixed-size bit-vector logics
- Metalevel algorithms for variant satisfiability
- Sharpening constraint programming approaches for bit-vector theory
- On the Generation of Positivstellensatz Witnesses in Degenerate Cases
- \textsf{SC}\(^2\): satisfiability checking meets symbolic computation. (Project paper)
- Title not available (Why is that?)
- Decision procedures. An algorithmic point of view
- Fixed points, Nash equilibria, and the existential theory of the reals
- Symbolic trajectory evaluation for word-level verification: theory and implementation
- Integrating simplex with tableaux
Uses Software
This page was built for publication: Decision procedures. An algorithmic point of view. With foreword by Randal E. Bryant
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2473386)
