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

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

1 2 3 ... 21 22 23 next

  1. Bayless, Sam; Kodirov, Nodir; Iqbal, Syed M.; Beschastnikh, Ivan; Hoos, Holger H.; Hu, Alan J.: Scalable constraint-based virtual data center allocation (2020)
  2. Benzmüller, Christoph; Scott, Dana S.: Automating free logic in HOL, with an experimental application in category theory (2020)
  3. Zhang, Nan; Duan, Zhenhua; Tian, Cong; Du, Hongwei: A novel approach to verifying context free properties of programs (2020)
  4. Allamigeon, Xavier; Katz, Ricardo D.: A formalization of convex polyhedra based on the simplex method (2019)
  5. Amadini, Roberto; Andrlon, Mak; Gange, Graeme; Schachte, Peter; Søndergaard, Harald; Stuckey, Peter J.: Constraint programming for dynamic symbolic execution of JavaScript (2019)
  6. Bentkamp, Alexander; Blanchette, Jasmin Christian; Klakow, Dietrich: A formal proof of the expressiveness of deep learning (2019)
  7. Besson, Frédéric; Blazy, Sandrine; Wilke, Pierre: A verified CompCert front-end for a memory model supporting pointer arithmetic and uninitialised data (2019)
  8. Bright, Curtis; Đoković, Dragomir Ž.; Kotsireas, Ilias; Ganesh, Vijay: The SAT+CAS method for combinatorial search with applications to best matrices (2019)
  9. Bueno, Denis; Sakallah, Karem A.: EUFORIA: complete software model checking with uninterpreted functions (2019)
  10. Camacho, Carlos; Llana, Luis; Núñez, Alberto; Bravetti, Mario: Probabilistic software product lines (2019)
  11. Cardelli, Luca; Tribastone, Mirco; Tschaikowski, Max; Vandin, Andrea: Symbolic computation of differential equivalences (2019)
  12. Drucker, Nir; Ho, Hsi-Ming; Ouaknine, Joël; Penn, Michal; Strichman, Ofer: Cyclic-routing of unmanned aerial vehicles (2019)
  13. Kobayashi, Tsutomu; Ishikawa, Fuyuki; Honiden, Shinichi: Consistency-preserving refactoring of refinement structures in Event-B models (2019)
  14. König, Barbara; Nederkorn, Maxime; Nolte, Dennis: CoReS: A tool for computing core graphs via SAT/SMT solvers (2019)
  15. Li, Wenda; Passmore, Grant Olney; Paulson, Lawrence C.: Deciding univariate polynomial problems using untrusted certificates in Isabelle/HOL (2019)
  16. Milicevic, Aleksandar; Near, Joseph P.; Kang, Eunsuk; Jackson, Daniel: Alloy*: a general-purpose higher-order relational constraint solver (2019)
  17. Ştefănescu, Andrei; Ciobâcă, Stefan; Mereuta, Radu; Moore, Brandon; Roşu, Grigore; Şerbănuṭă, Traian Florin: All-path reachability logic (2019)
  18. Stojanović-Ðurđević, Sana: From informal to formal proofs in Euclidean geometry (2019)
  19. Ta, Quang-Trung; Le, Ton Chanh; Khoo, Siau-Cheng; Chin, Wei-Ngan: Automated mutual induction proof in separation logic (2019)
  20. Wang, Wenxi; Søndergaard, Harald; Stuckey, Peter J.: Wombit: a portfolio bit-vector solver using word-level propagation (2019)

1 2 3 ... 21 22 23 next