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

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

1 2 3 ... 24 25 26 next

  1. 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)
  2. Cassez, Franck; Jensen, Peter Gjøl; Guldstrand, Larsen Kim: Verification and parameter synthesis for real-time programs using refinement of trace abstraction (2021)
  3. Cheng, Siu-Wing; Cheong, Otfried; Lee, Taegyoung; Ren, Zhengtong: Fitting a graph to one-dimensional data (2021)
  4. Dutle, Aaron; Moscato, Mariano; Titolo, Laura; Muñoz, César; Anderson, Gregory; Bobot, François: Formal analysis of the compact position reporting algorithm (2021)
  5. Alpuente, María; Pardo, Daniel; Villanueva, Alicia: Abstract contract synthesis and verification in the symbolic (\mathbbK) framework (2020)
  6. Barbosa, Haniel; Blanchette, Jasmin Christian; Fleury, Mathias; Fontaine, Pascal: Scalable fine-grained proofs for formula processing (2020)
  7. Bayless, Sam; Kodirov, Nodir; Iqbal, Syed M.; Beschastnikh, Ivan; Hoos, Holger H.; Hu, Alan J.: Scalable constraint-based virtual data center allocation (2020)
  8. Benzmüller, Christoph; Scott, Dana S.: Automating free logic in HOL, with an experimental application in category theory (2020)
  9. Bersani, Marcello M.; Rossi, Matteo; San Pietro, Pierluigi: On the initialization of clocks in timed formalisms (2020)
  10. Bohlender, Dimitri; Kowalewski, Stefan: Leveraging Horn clause solving for compositional verification of PLC software (2020)
  11. Bromberger, Martin; Sturm, Thomas; Weidenbach, Christoph: A complete and terminating approach to linear integer solving (2020)
  12. Champion, Adrien; Chiba, Tomoya; Kobayashi, Naoki; Sato, Ryosuke: ICE-based refinement type discovery for higher-order functional programs (2020)
  13. Chen, Qian Matteo; Finzi, Alberto; Mancini, Toni; Melatti, Igor; Tronci, Enrico: MILP, pseudo-Boolean, and OMT solvers for optimal fault-tolerant placements of relay nodes in mission critical wireless networks (2020)
  14. Drechsler, Rolf (ed.); Soeken, Mathias (ed.): Advanced Boolean techniques. Selected papers from the 13th international workshop on Boolean problems, Bremen, Germany, September 19--21, 2018 (2020)
  15. Fedyukovich, Grigory; Kaufman, Samuel J.; Bodík, Rastislav: Learning inductive invariants by sampling from frequency distributions (2020)
  16. Finkbeiner, Bernd; Hahn, Christopher; Lukert, Philip; Stenger, Marvin; Tentrup, Leander: Synthesis from hyperproperties (2020)
  17. García Soto, Miriam; Prabhakar, Pavithra: Abstraction based verification of stability of polyhedral switched systems (2020)
  18. Garzella, Jack J.; Baranowski, Marek; He, Shaobo; Rakamarić, Zvonimir: Leveraging compiler intermediate representation for multi- and cross-language verification (2020)
  19. Grastien, Alban; Scala, Enrico: CPCES: a planning framework to solve conformant planning problems through a counterexample guided refinement (2020)
  20. Hajdu, Ákos; Micskei, Zoltán: Efficient strategies for CEGAR-based model checking (2020)

1 2 3 ... 24 25 26 next