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

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

1 2 3 ... 16 17 18 next

  1. Faghih, Fathiyeh; Bonakdarpour, Borzoo; Tixeuil, Sebastien; Kulkarni, Sandeep: Automated synthesis of distributed self-stabilizing protocols (2018)
  2. Alberti, F.; Ghilardi, S.; Pagani, E.: Cardinality constraints for arrays (decidability results and applications) (2017)
  3. Alpuente, María; Pardo, Daniel; Villanueva, Alicia: Symbolic abstract contract synthesis in a rewriting framework (2017)
  4. Andrea Callia D’Iddio, Michael Huth: Manyopt: An Extensible Tool for Mixed, Non-Linear Optimization Through SMT Solving (2017) arXiv
  5. Bersani, Marcello M.; Rossi, Matteo; San Pietro, Pierluigi: A logical characterization of timed regular languages (2017)
  6. Chakraborty, Supratik; Gupta, Ashutosh; Jain, Rahul: Matching multiplications in bit-vector formulas (2017)
  7. Chaudhari, Dipak L.; Damani, Om: Assumption propagation through annotated programs (2017)
  8. Chen, Li; Lyu, Yinrun; Wang, Chong; Wu, Jingzheng; Zhang, Changyou; Min-Allah, Nasro; Alhiyafi, Jamal; Wang, Yongji: Solving linear optimization over arithmetic constraint formula (2017)
  9. Chihani, Zakaria; Marre, Bruno; Bobot, François; Bardin, Sébastien: Sharpening constraint programming approaches for bit-vector theory (2017)
  10. Chistikov, Dmitry; Dimitrova, Rayna; Majumdar, Rupak: Approximate counting in SMT and value estimation for probabilistic programs (2017)
  11. Dan, Andrei; Meshman, Yuri; Vechev, Martin; Yahav, Eran: Effective abstractions for verification under relaxed memory models (2017)
  12. Demirović, Emir; Musliu, Nysret: Modeling high school timetabling with bitvectors (2017)
  13. Demri, Stéphane; Galmiche, Didier; Larchey-Wendling, Dominique; Méry, Daniel: Separation logic with one quantified variable (2017)
  14. Dinsdale-Young, Thomas; da Rocha Pinto, Pedro; Andersen, Kristoffer Just; Birkedal, Lars: Caper - automatic verification for fine-grained concurrency (2017)
  15. Esparza, Javier: Advances in parameterized verification of population protocols (2017)
  16. Frohn, Florian; Giesl, Jürgen; Hensel, Jera; Aschermann, Cornelius; Ströder, Thomas: Lower bounds for runtime complexity of term rewriting (2017)
  17. Frumkin, Asya; Feldman, Yotam M.Y.; Lhoták, Ondřej; Padon, Oded; Sagiv, Mooly; Shoham, Sharon: Property directed reachability for proving absence of concurrent modification errors (2017)
  18. Fuhs, Carsten; Kop, Cynthia; Nishida, Naoki: Verifying procedural programs via constrained rewriting induction (2017)
  19. Giacobbe, Mirco; Guet, Călin C.; Gupta, Ashutosh; Henzinger, Thomas A.; Paixão, Tiago; Petrov, Tatjana: Model checking the evolution of gene regulatory networks (2017)
  20. Giesl, Jürgen; Aschermann, Cornelius; Brockschmidt, Marc; Emmes, Fabian; Frohn, Florian; Fuhs, Carsten; Hensel, Jera; Otto, Carsten; Plücker, Martin; Schneider-Kamp, Peter; Ströder, Thomas; Swiderski, Stephanie; Thiemann, René: Analyzing program termination and complexity automatically with \ssfAProVE (2017)

1 2 3 ... 16 17 18 next