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

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

1 2 3 ... 22 23 24 next

  1. Barbosa, Haniel; Blanchette, Jasmin Christian; Fleury, Mathias; Fontaine, Pascal: Scalable fine-grained proofs for formula processing (2020)
  2. Bayless, Sam; Kodirov, Nodir; Iqbal, Syed M.; Beschastnikh, Ivan; Hoos, Holger H.; Hu, Alan J.: Scalable constraint-based virtual data center allocation (2020)
  3. Benzmüller, Christoph; Scott, Dana S.: Automating free logic in HOL, with an experimental application in category theory (2020)
  4. Bersani, Marcello M.; Rossi, Matteo; San Pietro, Pierluigi: On the initialization of clocks in timed formalisms (2020)
  5. Bohlender, Dimitri; Kowalewski, Stefan: Leveraging Horn clause solving for compositional verification of PLC software (2020)
  6. Bromberger, Martin; Sturm, Thomas; Weidenbach, Christoph: A complete and terminating approach to linear integer solving (2020)
  7. Finkbeiner, Bernd; Hahn, Christopher; Lukert, Philip; Stenger, Marvin; Tentrup, Leander: Synthesis from hyperproperties (2020)
  8. García Soto, Miriam; Prabhakar, Pavithra: Abstraction based verification of stability of polyhedral switched systems (2020)
  9. Huang, Cheng-Chao; Xu, Ming; Li, Zhi-Bin: A conflict-driven solving procedure for poly-power constraints (2020)
  10. Peña, Ricardo: An assertional proof of red-black trees using Dafny (2020)
  11. Qin, Xudong; Bliudze, Simon; Madelaine, Eric; Hou, Zechen; Deng, Yuxin; Zhang, Min: SMT-based generation of symbolic automata (2020)
  12. Sebastiani, Roberto; Trentin, Patrick: \textscOptiMathSAT: a tool for optimization modulo theories (2020)
  13. Semenov, Alexander; Otpuschennikov, Ilya; Gribanova, Irina; Zaikin, Oleg; Kochemazov, Stepan: Translation of algorithmic descriptions of discrete functions to SAT with applications to cryptanalysis problems (2020)
  14. Zhang, Nan; Duan, Zhenhua; Tian, Cong; Du, Hongwei: A novel approach to verifying context free properties of programs (2020)
  15. Allamigeon, Xavier; Katz, Ricardo D.: A formalization of convex polyhedra based on the simplex method (2019)
  16. Amadini, Roberto; Andrlon, Mak; Gange, Graeme; Schachte, Peter; Søndergaard, Harald; Stuckey, Peter J.: Constraint programming for dynamic symbolic execution of JavaScript (2019)
  17. Apt, Krzysztof R.; Olderog, Ernst-Rüdiger: Fifty years of Hoare’s logic (2019)
  18. Bentkamp, Alexander; Blanchette, Jasmin Christian; Klakow, Dietrich: A formal proof of the expressiveness of deep learning (2019)
  19. Besson, Frédéric; Blazy, Sandrine; Wilke, Pierre: A verified CompCert front-end for a memory model supporting pointer arithmetic and uninitialised data (2019)
  20. Borralleras, Cristina; Larraz, Daniel; Rodríguez-Carbonell, Enric; Oliveras, Albert; Rubio, Albert: Incomplete SMT techniques for solving non-linear formulas over the integers (2019)

1 2 3 ... 22 23 24 next