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 219 articles , 1 standard article )

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

1 2 3 ... 9 10 11 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; Greenaway, David; Kaliszyk, Cezary; Kühlwein, Daniel; Urban, Josef: A learning-based fact selector for Isabelle/HOL (2016)
  7. Cardelli, Luca; Tribastone, Mirco; Tschaikowski, Max; Vandin, Andrea: Symbolic computation of differential equivalences (2016)
  8. Cassel, Sofia; Howar, Falk; Jonsson, Bengt; Steffen, Bernhard: Active learning for extended finite state machines (2016)
  9. Christ, Jürgen; Hoenicke, Jochen: Proof tree preserving tree interpolation (2016)
  10. Craciunas, Silviu S.; Oliver, Ramon Serna: Combined task- and network-level scheduling for distributed time-triggered systems (2016)
  11. Dross, Claire; Conchon, Sylvain; Kanig, Johannes; Paskevich, Andrei: Adding decision procedures to SMT solvers using axioms with triggers (2016)
  12. Ferrer Fioriti, Luis María; Hashemi, Vahid; Hermanns, Holger; Turrini, Andrea: Deciding probabilistic automata weak bisimulation: theory and practice (2016)
  13. Hajdu, Ákos; Tóth, Tamás; Vörös, András; Majzik, István: A configurable CEGAR framework with interpolation-based refinements (2016)
  14. Keshishzadeh, Sarmen; Mooij, Arjan J.: Formalizing and testing the consistency of DSL transformations (2016)
  15. Konnov, Igor; Veith, Helmut; Widder, Josef: What you always wanted to know about model checking of fault-tolerant distributed algorithms (2016)
  16. Kovásznai, Gergely; Fröhlich, Andreas; Biere, Armin: Complexity of fixed-size bit-vector logics (2016)
  17. Liu, Shaoying: Testing-based formal verification for theorems and its application in software specification verification (2016)
  18. Wiik, Jonatan; Boström, Pontus: Contract-based verification of MATLAB-style matrix programs (2016)
  19. Xu, Ming; Zhang, Lijun; Jansen, David N.; Zhu, Huibiao; Yang, Zongyuan: Multiphase until formulas over Markov reward models: an algebraic approach (2016)
  20. Zhang, Hantao: An experiment with satisfiability modulo SAT (2016)

1 2 3 ... 9 10 11 next