An experiment with satisfiability modulo SAT. (English) Zbl 1356.68208
MSC:
68T15
03B05
Found 10 Documents (Results 1–10)
The TPTP typed first-order form with arithmetic. (English) Zbl 1352.68217
Bjørner, Nikolaj (ed.) et al., Logic for programming, artificial intelligence, and reasoning. 18th international conference, LPAR-18, Mérida, Venezuela, March 11–15, 2012. Proceedings. Berlin: Springer (ISBN 978-3-642-28716-9/pbk). Lecture Notes in Computer Science 7180, 406-419 (2012).
MSC:
68T15
03B35
Automatic verification of TLA\(^{ + }\) proof obligations with SMT solvers. (English) Zbl 1352.68159
Bjørner, Nikolaj (ed.) et al., Logic for programming, artificial intelligence, and reasoning. 18th international conference, LPAR-18, Mérida, Venezuela, March 11–15, 2012. Proceedings. Berlin: Springer (ISBN 978-3-642-28716-9/pbk). Lecture Notes in Computer Science 7180, 289-303 (2012).
Expressing polymorphic types in a many-sorted language. (English) Zbl 1348.68215
Tinelli, Cesare (ed.) et al., Frontiers of combining systems. 8th international symposium, FroCoS 2011, Saarbrücken, Germany, October 5–7, 2011. Proceedings. Berlin: Springer (ISBN 978-3-642-24363-9/pbk). Lecture Notes in Computer Science 6989. Lecture Notes in Artificial Intelligence, 87-102 (2011).
MSC:
68T15
03B70
Solving quantified verification conditions using satisfiability modulo theories. (English) Zbl 1184.68461
Model-based theory combination. (English) Zbl 1277.03007
Krstić, Sava (ed.) et al., Proceedings of the 5th international workshop on satisfiability modulo theories (SMT 2007), Berlin, Germany, July 1–2, 2007. Amsterdam: Elsevier. Electronic Notes in Theoretical Computer Science 198, No. 2, 37-49 (2008).
E-matching for fun and profit. (English) Zbl 1277.68142
Krstić, Sava (ed.) et al., Proceedings of the 5th international workshop on satisfiability modulo theories (SMT 2007), Berlin, Germany, July 1–2, 2007. Amsterdam: Elsevier. Electronic Notes in Theoretical Computer Science 198, No. 2, 19-35 (2008).
Filter Results by …
Document Type
- Journal Articles (5)
- Collection Articles (5)
all
top 5
Author
- de Moura, Leonardo (2)
- Tinelli, Cesare (2)
- Barrett, Clark W. (1)
- Baumgartner, Peter (1)
- Bjørner, Nikolaj S. (1)
- Bobot, François (1)
- Claessen, Koen (1)
- Ge, Yeting (1)
- Hadarean, Liana (1)
- Hamadi, Youssef (1)
- Kiniry, Joseph R. (1)
- Łopuszański, Jakub (1)
- Merz, Stephan (1)
- Moskal, Michał (1)
- Oe, Duckki (1)
- Paskevich, Andrei (1)
- Reynolds, Andrew (1)
- Schulz, Stephan (1)
- Sebastiani, Roberto (1)
- Stump, Aaron (1)
- Sutcliffe, Geoff (1)
- Vanzetto, Hernán (1)
- Wintersteiger, Christoph M. (1)
Serial
all
top 3
Software
- cvc3 (10)
- SMT-LIB (8)
- z3 (7)
- ESC/Java (3)
- SIMPLIFY (3)
- Yices (3)
- Coq (2)
- Isabelle/HOL (2)
- MathSAT (2)
- SPASS+T (2)
- TPTP (2)
- VAMPIRE (2)
- Why3 (2)
- Boogie (1)
- Boolector (1)
- CLSAT (1)
- Chaff (1)
- CirQit2 (1)
- E Theorem Prover (1)
- E-Darvin (1)
- Frama-C (1)
- Isabelle (1)
- Jessie (1)
- ML (1)
- Metis_ (1)
- Nemerle (1)
- QEPCAD (1)
- QUBE (1)
- QuBE++ (1)
- Quantor (1)
- SATO (1)
- SPASS (1)
- STP (1)
- Sledgehammer (1)
- Spec# (1)
- THF0 (1)
- TLAPS (1)
- UCLID (1)
- Zap (1)
- Zenon (1)
- seL4 (1)
- veriT (1)
