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

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

1 2 3 ... 29 30 31 next

  1. Akgün, Özgür; Frisch, Alan M.; Gent, Ian P.; Jefferson, Christopher; Miguel, Ian; Nightingale, Peter: \textscConjure: automatic generation of constraint models from problem specifications (2022)
  2. Bagnara, Roberto; Bagnara, Abramo; Biselli, Fabio; Chiari, Michele; Gori, Roberta: Correct approximation of IEEE 754 floating-point arithmetic for program verification (2022)
  3. Bonacina, Maria Paola; Graham-Lengrand, Stéphane; Shankar, Natarajan: Conflict-driven satisfiability for theory combination: lemmas, modules, and proofs (2022)
  4. Faisal Al Ameen, Mahmudul; Kobayashi, Naoki; Sato, Ryosuke: Asynchronous unfold/fold transformation for fixpoint logic (2022)
  5. Gregor Betz, Kyle Richardson: DeepA2: A Modular Framework for Deep Argument Analysis with Pretrained Neural Text2Text Language Models (2022) arXiv
  6. Käfer, Nikolai; Baier, Christel; Diller, Martin; Dubslaff, Clemens; Gaggl, Sarah Alice; Hermanns, Holger: Admissibility in probabilistic argumentation (2022)
  7. Lewis, Robert Y.; Wu, Minchao: A bi-directional extensible interface between Lean and Mathematica (2022)
  8. Safari, Mohsen; Huisman, Marieke: Formal verification of parallel prefix sum and stream compaction algorithms in CUDA (2022)
  9. Verdier, Cees Ferdinand; Kochdumper, Niklas; Althoff, Matthias; Mazo, Manuel: Formal synthesis of closed-form sampled-data controllers for nonlinear continuous-time systems under STL specifications (2022)
  10. Vlk, Marek; Brejchová, Kateřina; Hanzálek, Zdeněk; Tang, Siyu: Large-scale periodic scheduling in time-sensitive networks (2022)
  11. Xu, Ming; Fu, Jianling; Mei, Jingyi; Deng, Yuxin: Model checking QCTL plus on quantum Markov chains (2022)
  12. Abbasi, Rosa; Schiffl, Jonas; Darulova, Eva; Ulbrich, Mattias; Ahrendt, Wolfgang: Deductive verification of floating-point Java programs in KeY (2021)
  13. Amadini, Roberto; Gange, Graeme; Schachte, Peter; Søndergaard, Harald; Stuckey, Peter J.: Algorithm selection for dynamic symbolic execution: a preliminary study (2021)
  14. Amat, Nicolas; Berthomieu, Bernard; Dal Zilio, Silvano: On the combination of polyhedral abstraction and SMT-based model checking for Petri nets (2021)
  15. Ansótegui, Carlos; Ojeda, Jesús; Pacheco, Antonio; Pon, Josep; Salvia, Josep M.; Torres, Eduard: OptiLog: a framework for SAT-based systems (2021)
  16. Argyris, Georgios; Lluch Lafuente, Alberto; Tribastone, Mirco; Tschaikowski, Max; Vandin, Andrea: Reducing Boolean networks with backward Boolean equivalence (2021)
  17. Backeman, Peter; Rümmer, Philipp; Zeljić, Aleksandar: Interpolating bit-vector formulas using uninterpreted predicates and Presburger arithmetic (2021)
  18. Behrisch, Mike; Chavarri Villarello, Alain; Vargas-García, Edith: Representing partition lattices through FCA (2021)
  19. 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)
  20. Bigarella, Filippo; Cimatti, Alessandro; Griggio, Alberto; Irfan, Ahmed; Jonáš, Martin; Roveri, Marco; Sebastiani, Roberto; Trentin, Patrick: Optimization modulo non-linear arithmetic via incremental linearization (2021)

1 2 3 ... 29 30 31 next