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

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

1 2 3 ... 27 28 29 next

  1. Abbasi, Rosa; Schiffl, Jonas; Darulova, Eva; Ulbrich, Mattias; Ahrendt, Wolfgang: Deductive verification of floating-point Java programs in KeY (2021)
  2. Backeman, Peter; Rümmer, Philipp; Zeljić, Aleksandar: Interpolating bit-vector formulas using uninterpreted predicates and Presburger arithmetic (2021)
  3. Bhattacharyya, Arnab; Gupta, Ashutosh; Kuppusamy, Lakshmanan; Mani, Somya; Shukla, Ankit; Srivas, Mandayam; Thattai, Mukund: A formal methods approach to predicting new features of the eukaryotic vesicle traffic system (2021)
  4. Blondin, Michael; Esparza, Javier; Jaax, Stefan; Meyer, Philipp J.: Towards efficient verification of population protocols (2021)
  5. Cassez, Franck; Jensen, Peter Gjøl; Guldstrand, Larsen Kim: Verification and parameter synthesis for real-time programs using refinement of trace abstraction (2021)
  6. Češka, Milan; Hensel, Christian; Junges, Sebastian; Katoen, Joost-Pieter: Counterexample-guided inductive synthesis for probabilistic systems (2021)
  7. Cheng, Siu-Wing; Cheong, Otfried; Lee, Taegyoung; Ren, Zhengtong: Fitting a graph to one-dimensional data (2021)
  8. Cimatti, Alessandro; Griggio, Alberto; Redondi, Gianluca: Universal invariant checking of parametric systems with quantifier-free SMT reasoning (2021)
  9. Dutle, Aaron; Moscato, Mariano; Titolo, Laura; Muñoz, César; Anderson, Gregory; Bobot, François: Formal analysis of the compact position reporting algorithm (2021)
  10. Eraşcu, Mădălina; Micota, Flavia; Zaharie, Daniela: Scalable optimal deployment in the cloud of component-based applications using optimization modulo theory, mathematical programming and symmetry breaking (2021)
  11. Filliâtre, Jean-Christophe: Simpler proofs with decentralized invariants (2021)
  12. Garcia-Contreras, Isabel; Morales, José F.; Hermenegildo, Manuel V.: Incremental and modular context-sensitive analysis (2021)
  13. Hendriks, Martijn; Geilen, Marc; Goossens, Kees; de Jong, Rob; Basten, Twan: Interface modeling for quality and resource management (2021)
  14. Hossain, Akash; Laroussinie, François: (\mathsfQCTL) model-checking with (\mathsfQBF) solvers (2021)
  15. Kruff, Niclas; Lüders, Christoph; Radulescu, Ovidiu; Sturm, Thomas; Walcher, Sebastian: Algorithmic reduction of biological networks with multiple time scales (2021)
  16. Luteberget, Bjørnar; Claessen, Koen; Johansen, Christian; Steffen, Martin: SAT modulo discrete event simulation applied to railway design capacity analysis (2021)
  17. Meyer, Fabian; Hark, Marcel; Giesl, Jürgen: Inferring expected runtimes of probabilistic integer programs using expected sizes (2021)
  18. Namjoshi, Kedar S.; Xue, Anton: A self-certifying compilation framework for WebAssembly (2021)
  19. Niemetz, Aina; Preiner, Mathias; Reynolds, Andrew; Barrett, Clark; Tinelli, Cesare: On solving quantified bit-vector constraints using invertibility conditions (2021)
  20. Niemetz, Aina; Preiner, Mathias; Reynolds, Andrew; Zohar, Yoni; Barrett, Clark; Tinelli, Cesare: Towards satisfiability modulo parametric bit-vectors (2021)

1 2 3 ... 27 28 29 next