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

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

1 2 3 ... 9 10 11 next

  1. Avigad, Jeremy; Lewis, Robert Y.; Roux, Cody: A heuristic prover for real inequalities (2016)
  2. Ballard, Grey; Benson, Austin R.; Druinsky, Alex; Lipshitz, Benjamin; Schwartz, Oded: Improving the numerical stability of fast matrix multiplication (2016)
  3. Bersani, Marcello M.; Rossi, Matteo; San Pietro, Pierluigi: A tool for deciding the satisfiability of continuous-time metric temporal logic (2016)
  4. Blanchette, Jasmin Christian; Böhme, Sascha; Fleury, Mathias; Smolka, Steffen Juilf; Steckermeier, Albert: Semi-intelligible Isar proofs from machine-generated proofs (2016)
  5. Blanchette, Jasmin Christian; Greenaway, David; Kaliszyk, Cezary; Kühlwein, Daniel; Urban, Josef: A learning-based fact selector for Isabelle/HOL (2016)
  6. Cardelli, Luca; Tribastone, Mirco; Tschaikowski, Max; Vandin, Andrea: Symbolic computation of differential equivalences (2016)
  7. Cassel, Sofia; Howar, Falk; Jonsson, Bengt; Steffen, Bernhard: Active learning for extended finite state machines (2016)
  8. Christ, Jürgen; Hoenicke, Jochen: Proof tree preserving tree interpolation (2016)
  9. Craciunas, Silviu S.; Oliver, Ramon Serna: Combined task- and network-level scheduling for distributed time-triggered systems (2016)
  10. Dross, Claire; Conchon, Sylvain; Kanig, Johannes; Paskevich, Andrei: Adding decision procedures to SMT solvers using axioms with triggers (2016)
  11. Ferrer Fioriti, Luis María; Hashemi, Vahid; Hermanns, Holger; Turrini, Andrea: Deciding probabilistic automata weak bisimulation: theory and practice (2016)
  12. Hajdu, Ákos; Tóth, Tamás; Vörös, András; Majzik, István: A configurable CEGAR framework with interpolation-based refinements (2016)
  13. Keshishzadeh, Sarmen; Mooij, Arjan J.: Formalizing and testing the consistency of DSL transformations (2016)
  14. Wiik, Jonatan; Boström, Pontus: Contract-based verification of MATLAB-style matrix programs (2016)
  15. Xu, Ming; Zhang, Lijun; Jansen, David N.; Zhu, Huibiao; Yang, Zongyuan: Multiphase until formulas over Markov reward models: an algebraic approach (2016)
  16. Zhang, Hantao: An experiment with satisfiability modulo SAT (2016)
  17. Alberti, Francesco; Ghilardi, Silvio; Sharygina, Natasha: Decision procedures for flat array properties (2015)
  18. Baumgartner, Peter: SMTtoTPTP -- a converter for theorem proving formats (2015)
  19. Baumgartner, Peter; Bax, Joshua; Waldmann, Uwe: Beagle -- a hierarchic superposition theorem prover (2015)
  20. Bersani, Marcello M.; Rossi, Matteo; San Pietro, Pierluigi: An SMT-based approach to satisfiability checking of MITL (2015)

1 2 3 ... 9 10 11 next