z3

Z3 is a high-performance theorem prover being developed at Microsoft Research.Z3 supports linear real and integer arithmetic, fixed-size bit-vectors, extensional arrays, uninterpreted functions, and quantifiers. Z3 is integrated with a number of program analysis, testing, and verification tools from Microsoft Research. These include: VCC, Spec#, Boogie, Pex, Yogi, Vigilante, SLAM, F7, F*, SAGE, VS3, FORMULA, and HAVOC.


References in zbMATH (referenced in 223 articles , 1 standard article )

Showing results 1 to 20 of 223.
Sorted by year (citations)

1 2 3 ... 10 11 12 next

  1. Andrea Callia D’Iddio, Michael Huth: Manyopt: An Extensible Tool for Mixed, Non-Linear Optimization Through SMT Solving (2017) arXiv
  2. Avigad, Jeremy; Lewis, Robert Y.; Roux, Cody: A heuristic prover for real inequalities (2016)
  3. Ballard, Grey; Benson, Austin R.; Druinsky, Alex; Lipshitz, Benjamin; Schwartz, Oded: Improving the numerical stability of fast matrix multiplication (2016)
  4. Bersani, Marcello M.; Rossi, Matteo; San Pietro, Pierluigi: A tool for deciding the satisfiability of continuous-time metric temporal logic (2016)
  5. Blanchette, Jasmin Christian; Böhme, Sascha; Fleury, Mathias; Smolka, Steffen Juilf; Steckermeier, Albert: Semi-intelligible Isar proofs from machine-generated proofs (2016)
  6. Blanchette, Jasmin Christian; Böhme, Sascha; Popescu, Andrei; Smallbone, Nicholas: Encoding monomorphic and polymorphic types (2016)
  7. Blanchette, Jasmin Christian; Greenaway, David; Kaliszyk, Cezary; Kühlwein, Daniel; Urban, Josef: A learning-based fact selector for Isabelle/HOL (2016)
  8. Cardelli, Luca; Tribastone, Mirco; Tschaikowski, Max; Vandin, Andrea: Symbolic computation of differential equivalences (2016)
  9. Cassel, Sofia; Howar, Falk; Jonsson, Bengt; Steffen, Bernhard: Active learning for extended finite state machines (2016)
  10. Christ, Jürgen; Hoenicke, Jochen: Proof tree preserving tree interpolation (2016)
  11. Craciunas, Silviu S.; Oliver, Ramon Serna: Combined task- and network-level scheduling for distributed time-triggered systems (2016)
  12. Dross, Claire; Conchon, Sylvain; Kanig, Johannes; Paskevich, Andrei: Adding decision procedures to SMT solvers using axioms with triggers (2016)
  13. Ferrer Fioriti, Luis María; Hashemi, Vahid; Hermanns, Holger; Turrini, Andrea: Deciding probabilistic automata weak bisimulation: theory and practice (2016)
  14. Hajdu, Ákos; Tóth, Tamás; Vörös, András; Majzik, István: A configurable CEGAR framework with interpolation-based refinements (2016)
  15. Keshishzadeh, Sarmen; Mooij, Arjan J.: Formalizing and testing the consistency of DSL transformations (2016)
  16. Komuravelli, Anvesh; Gurfinkel, Arie; Chaki, Sagar: SMT-based model checking for recursive programs (2016)
  17. Konnov, Igor; Veith, Helmut; Widder, Josef: What you always wanted to know about model checking of fault-tolerant distributed algorithms (2016)
  18. Kovásznai, Gergely; Fröhlich, Andreas; Biere, Armin: Complexity of fixed-size bit-vector logics (2016)
  19. Liang, Tianyi; Reynolds, Andrew; Tsiskaridze, Nestan; Tinelli, Cesare; Barrett, Clark; Deters, Morgan: An efficient SMT solver for string constraints (2016)
  20. Liu, Shaoying: Testing-based formal verification for theorems and its application in software specification verification (2016)

1 2 3 ... 10 11 12 next