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

Showing results 1 to 20 of 240.
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. Giesl, Jürgen; Aschermann, Cornelius; Brockschmidt, Marc; Emmes, Fabian; Frohn, Florian; Fuhs, Carsten; Hensel, Jera; Otto, Carsten; Plücker, Martin; Schneider-Kamp, Peter; Ströder, Thomas; Swiderski, Stephanie; Thiemann, René: Analyzing program termination and complexity automatically with \ssfAProVE (2017)
  5. Reynolds, Andrew; Blanchette, Jasmin Christian: A decision procedure for (co)datatypes in SMT solvers (2017)
  6. Ströder, Thomas; Giesl, Jürgen; Brockschmidt, Marc; Frohn, Florian; Fuhs, Carsten; Hensel, Jera; Schneider-Kamp, Peter; Aschermann, Cornelius: Automatically proving termination and memory safety for programs with pointer arithmetic (2017)
  7. Zeljić, Aleksandar; Wintersteiger, Christoph M.; Rümmer, Philipp: An approximation framework for solvers and decision procedures (2017)
  8. 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)
  9. Zulkoski, Edward; Bright, Curtis; Heinle, Albert; Kotsireas, Ilias; Czarnecki, Krzysztof; Ganesh, Vijay: Combining SAT solvers with computer algebra systems to verify combinatorial conjectures (2017)
  10. Avigad, Jeremy; Lewis, Robert Y.; Roux, Cody: A heuristic prover for real inequalities (2016)
  11. Ballard, Grey; Benson, Austin R.; Druinsky, Alex; Lipshitz, Benjamin; Schwartz, Oded: Improving the numerical stability of fast matrix multiplication (2016)
  12. Bersani, Marcello M.; Rossi, Matteo; San Pietro, Pierluigi: A tool for deciding the satisfiability of continuous-time metric temporal logic (2016)
  13. Blanchette, Jasmin Christian; Böhme, Sascha; Fleury, Mathias; Smolka, Steffen Juilf; Steckermeier, Albert: Semi-intelligible Isar proofs from machine-generated proofs (2016)
  14. Blanchette, Jasmin Christian; Böhme, Sascha; Popescu, Andrei; Smallbone, Nicholas: Encoding monomorphic and polymorphic types (2016)
  15. Blanchette, Jasmin Christian; Greenaway, David; Kaliszyk, Cezary; Kühlwein, Daniel; Urban, Josef: A learning-based fact selector for Isabelle/HOL (2016)
  16. Cardelli, Luca; Tribastone, Mirco; Tschaikowski, Max; Vandin, Andrea: Symbolic computation of differential equivalences (2016)
  17. Cassel, Sofia; Howar, Falk; Jonsson, Bengt; Steffen, Bernhard: Active learning for extended finite state machines (2016)
  18. Christ, Jürgen; Hoenicke, Jochen: Proof tree preserving tree interpolation (2016)
  19. Craciunas, Silviu S.; Oliver, Ramon Serna: Combined task- and network-level scheduling for distributed time-triggered systems (2016)
  20. Dross, Claire; Conchon, Sylvain; Kanig, Johannes; Paskevich, Andrei: Adding decision procedures to SMT solvers using axioms with triggers (2016)

1 2 3 ... 10 11 12 next