Decision procedures. An algorithmic point of view
From MaRDI portal
Introductory exposition (textbooks, tutorial papers, etc.) pertaining to computer science (68-01) Research exposition (monographs, survey articles) pertaining to computer science (68-02) Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.) (68T20) Logic in artificial intelligence (68T27)
Recommendations
Cited in
(42)- A note on Kirkwood's algebraic method for decision problems
- 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
- Solving bitvectors with MCSAT: explanations from bits and pieces
- CTL* model checking for data-aware dynamic systems with arithmetic
- MedleySolver: online SMT algorithm selection
- A symbolic programming approach to the rendezvous search problem
- Unified program generation and verification: a case study on number-theoretic transform
- 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
- Decision procedures. An algorithmic point of view. With foreword by Randal E. Bryant
- scientific article; zbMATH DE number 4055422 (Why is no real title available?)
- scientific article; zbMATH DE number 176085 (Why is no real title available?)
- scientific article; zbMATH DE number 7453200 (Why is no real title available?)
- Automated and sound synthesis of Lyapunov functions with SMT solvers
- Counterexample-Guided Prophecy for Model Checking Modulo the Theory of Arrays
- Automated repair for timed systems
- FOSSIL
- On algebraic array theories
- Trace Abstraction-Based Verification for Uninterpreted Programs
- Equivalence checking for orthocomplemented bisemilattices in log-linear time
- Formula normalizations in verification
- Conflict-free electric vehicle routing problem: an improved compositional algorithm
- Introducing asynchronicity to probabilistic hyperproperties
- Succinct ordering and aggregation constraints in algebraic array theories
- Block languages and their bitmap representations
- Transforming concurrent programs with semaphores into logically constrained term rewrite systems
- Shininess, strong politeness, and unicorns
- Computing inductive invariants of regular abstraction frameworks
- Relatively complete and efficient partial quantifier elimination
- Novel tree-search method for synthesizing SMT strategies
- A nesting-preserving transformation of SIMP programs into logically constrained term rewrite systems
- Combining combination properties: minimal models
- Universal truth of operator statements via ideal membership
- An introduction to the theory of linear integer arithmetic (invited paper)
- Multiple interdependent simple temporal networks with uncertainty: a semi-decentralized multi-agent model with shared control of activity durations
- CSB: a counting and sampling tool for bit-vectors
- ParSAT: parallel solving of floating-point satisfiability
- Learning union of integer hypercubes with queries (with applications to monadic decomposition)
Describes a project that uses
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)
