Decision procedures. An algorithmic point of view
From MaRDI portal
Publication:518892
DOI10.1007/978-3-662-50497-0zbMath1358.68002OpenAlexW4249885861MaRDI QIDQ518892
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
Introductory exposition (textbooks, tutorial papers, etc.) pertaining to computer science (68-01) Logic in artificial intelligence (68T27) Research exposition (monographs, survey articles) pertaining to computer science (68-02) Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.) (68T20)
Related Items
A symbolic programming approach to the rendezvous search problem ⋮ Automated and Sound Synthesis of Lyapunov Functions with SMT Solvers ⋮ Counterexample-Guided Prophecy for Model Checking Modulo the Theory of Arrays ⋮ Learning union of integer hypercubes with queries (with applications to monadic decomposition) ⋮ Unified program generation and verification: a case study on number-theoretic transform ⋮ Automated repair for timed systems ⋮ FOSSIL ⋮ On algebraic array theories ⋮ Unnamed Item ⋮ Book review of: J. F. Groote and M. R. Mousavi, Modeling and analysis of communicating systems ⋮ Decidable \({\exists}^*{\forall}^*\) first-order fragments of linear rational arithmetic with uninterpreted predicates ⋮ Automated and formal synthesis of neural barrier certificates for dynamical models ⋮ Towards satisfiability modulo parametric bit-vectors ⋮ A conflict-driven solving procedure for poly-power constraints ⋮ Towards bit-width-independent proofs in SMT solvers ⋮ Book review of: E. M. Clarke (ed.) et al., Handbook of model checking ⋮ Solving bitvectors with MCSAT: explanations from bits and pieces ⋮ CTL* model checking for data-aware dynamic systems with arithmetic ⋮ MedleySolver: online SMT algorithm selection
Uses Software
