Decision procedures. An algorithmic point of view
DOI10.1007/978-3-662-50497-0zbMATH Open1358.68002OpenAlexW4249885861MaRDI QIDQ518892FDOQ518892
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
Recommendations
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 (31)
- Book review of: E. M. Clarke (ed.) et al., Handbook of model checking
- CTL* model checking for data-aware dynamic systems with arithmetic
- Succinct ordering and aggregation constraints in algebraic array theories
- Learning union of integer hypercubes with queries (with applications to monadic decomposition)
- A symbolic programming approach to the rendezvous search problem
- Decidable \({\exists}^*{\forall}^*\) first-order fragments of linear rational arithmetic with uninterpreted predicates
- Title not available (Why is that?)
- A note on Kirkwood's algebraic method for decision problems
- Towards satisfiability modulo parametric bit-vectors
- Solving bitvectors with MCSAT: explanations from bits and pieces
- Title not available (Why is that?)
- 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
- Title not available (Why is that?)
- On algebraic array theories
- Automated and formal synthesis of neural barrier certificates for dynamical models
- 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
- Automated repair for timed systems
- Block languages and their bitmap representations
- Transforming concurrent programs with semaphores into logically constrained term rewrite systems
- A conflict-driven solving procedure for poly-power constraints
- Equivalence checking for orthocomplemented bisemilattices in log-linear time
- Formula normalizations in verification
- FOSSIL
- MedleySolver: online SMT algorithm selection
- Conflict-free electric vehicle routing problem: an improved compositional algorithm
- Introducing asynchronicity to probabilistic hyperproperties
Uses Software
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)
