Publication:4804898
From MaRDI portal
zbMath1010.68168MaRDI QIDQ4804898
Randal E. Bryant, Ofer Strichman, Sanjit A. Seshia
Publication date: 1 May 2003
Full work available at URL: http://link.springer.de/link/service/series/0558/bibs/2404/24040209.htm
68Q60: Specification and verification (program logics, model checking, etc.)
03B25: Decidability of theories and sets of sentences
Related Items
A Term Rewriting Technique for Decision Graphs, Exploiting Symmetry in SMT Problems, Local Search For Satisfiability Modulo Integer Arithmetic Theories, The SAT-based approach to separation logic, M\textbf{ath}SAT: Tight integration of SAT and mathematical decision procedures, A framework for satisfiability modulo theories, Zero, successor and equality in BDDs, Decidable \({\exists}^*{\forall}^*\) first-order fragments of linear rational arithmetic with uninterpreted predicates, SMELS: satisfiability modulo equality with lazy superposition, The model evolution calculus as a first-order DPLL method, Efficient theory combination via Boolean search, Satisfiability Modulo Theories, Combining Instance Generation and Resolution