Decision procedures. An algorithmic point of view

DOI10.1007/978-3-662-50497-0MaRDI QIDQ518892zbMATH OpenOpenAlexFDO

Authors Daniel Kroening, Ofer Strichman

Publication date 30 March 2017

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

Full work available at URL https://doi.org/10.1007/978-3-662-50497-0

Mathematics Subject Classification ID

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)

Recommendations

• Decision procedures. An algorithmic point of view. With foreword by Randal E. Bryant
• Satisfiability modulo theories
• scientific article; zbMATH DE number 5194318
• Computer Aided Verification
• Computer Aided Verification

Cited in

(31)

• Book review of: E. M. Clarke (ed.) et al., Handbook of model checking
• CTL* model checking for data-aware dynamic systems with arithmetic
• Learning union of integer hypercubes with queries (with applications to monadic decomposition)
• Succinct ordering and aggregation constraints in algebraic array theories
• A symbolic programming approach to the rendezvous search problem
• Decidable \({\exists}^*{\forall}^*\) first-order fragments of linear rational arithmetic with uninterpreted predicates
• A note on Kirkwood's algebraic method for decision problems
• scientific article; zbMATH DE number 4055422 (Why is no real title available?)
• Towards satisfiability modulo parametric bit-vectors
• Solving bitvectors with MCSAT: explanations from bits and pieces
• scientific article; zbMATH DE number 176085 (Why is no real title available?)
• Book review of: J. F. Groote and M. R. Mousavi, Modeling and analysis of communicating systems
• Trace Abstraction-Based Verification for Uninterpreted Programs
• Automated and sound synthesis of Lyapunov functions with SMT solvers
• Automated and formal synthesis of neural barrier certificates for dynamical models
• scientific article; zbMATH DE number 7453200 (Why is no real title available?)
• On algebraic array theories
• Unified program generation and verification: a case study on number-theoretic transform
• Counterexample-Guided Prophecy for Model Checking Modulo the Theory of Arrays
• Towards bit-width-independent proofs in SMT solvers
• Decision procedures. An algorithmic point of view. With foreword by Randal E. Bryant
• A conflict-driven solving procedure for poly-power constraints
• Automated repair for timed systems
• Block languages and their bitmap representations
• Transforming concurrent programs with semaphores into logically constrained term rewrite systems
• Equivalence checking for orthocomplemented bisemilattices in log-linear time
• Formula normalizations in verification
• MedleySolver: online SMT algorithm selection
• FOSSIL
• Conflict-free electric vehicle routing problem: an improved compositional algorithm
• Introducing asynchronicity to probabilistic hyperproperties

Describes a project that uses

Uses Software

• Z34Bio
• C32SAT
• QAGen
• ICS
• RSat
• AMUSE
• FaCT++
• Smallfoot
• QBFLIB
• MathSAT5
• CVC4
• LLBMC
• CVC Lite
• DART
• PicoSAT
• Plingeling
• BerkMin
• SATzilla
• SIMPLIFY
• z3
• SATIRE
• SMT-LIB
• UnitWalk
• HaifaSat
• CUTE
• Boolector

This page was built for publication: Decision procedures. An algorithmic point of view

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q518892)