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

Showing results 1 to 20 of 228.
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. Chaudhari, Dipak L.; Damani, Om: Assumption propagation through annotated programs (2017)
  3. Dinsdale-Young, Thomas; da Rocha Pinto, Pedro; Andersen, Kristoffer Just; Birkedal, Lars: Caper - automatic verification for fine-grained concurrency (2017)
  4. Zheng, Yunhui; Ganesh, Vijay; Subramanian, Sanu; Tripp, Omer; Berzish, Murphy; Dolby, Julian; Zhang, Xiangyu: Z3str2: an efficient solver for strings, regular expressions, and length constraints (2017)
  5. Avigad, Jeremy; Lewis, Robert Y.; Roux, Cody: A heuristic prover for real inequalities (2016)
  6. Ballard, Grey; Benson, Austin R.; Druinsky, Alex; Lipshitz, Benjamin; Schwartz, Oded: Improving the numerical stability of fast matrix multiplication (2016)
  7. Bersani, Marcello M.; Rossi, Matteo; San Pietro, Pierluigi: A tool for deciding the satisfiability of continuous-time metric temporal logic (2016)
  8. Blanchette, Jasmin Christian; Böhme, Sascha; Fleury, Mathias; Smolka, Steffen Juilf; Steckermeier, Albert: Semi-intelligible Isar proofs from machine-generated proofs (2016)
  9. Blanchette, Jasmin Christian; Böhme, Sascha; Popescu, Andrei; Smallbone, Nicholas: Encoding monomorphic and polymorphic types (2016)
  10. Blanchette, Jasmin Christian; Greenaway, David; Kaliszyk, Cezary; Kühlwein, Daniel; Urban, Josef: A learning-based fact selector for Isabelle/HOL (2016)
  11. Cardelli, Luca; Tribastone, Mirco; Tschaikowski, Max; Vandin, Andrea: Symbolic computation of differential equivalences (2016)
  12. Cassel, Sofia; Howar, Falk; Jonsson, Bengt; Steffen, Bernhard: Active learning for extended finite state machines (2016)
  13. Christ, Jürgen; Hoenicke, Jochen: Proof tree preserving tree interpolation (2016)
  14. Craciunas, Silviu S.; Oliver, Ramon Serna: Combined task- and network-level scheduling for distributed time-triggered systems (2016)
  15. Dross, Claire; Conchon, Sylvain; Kanig, Johannes; Paskevich, Andrei: Adding decision procedures to SMT solvers using axioms with triggers (2016)
  16. Ferrer Fioriti, Luis María; Hashemi, Vahid; Hermanns, Holger; Turrini, Andrea: Deciding probabilistic automata weak bisimulation: theory and practice (2016)
  17. Hajdu, Ákos; Tóth, Tamás; Vörös, András; Majzik, István: A configurable CEGAR framework with interpolation-based refinements (2016)
  18. Keshishzadeh, Sarmen; Mooij, Arjan J.: Formalizing and testing the consistency of DSL transformations (2016)
  19. Komuravelli, Anvesh; Gurfinkel, Arie; Chaki, Sagar: SMT-based model checking for recursive programs (2016)
  20. Konnov, Igor; Veith, Helmut; Widder, Josef: What you always wanted to know about model checking of fault-tolerant distributed algorithms (2016)

1 2 3 ... 10 11 12 next