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

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

1 2 3 ... 17 18 19 next

  1. Cheng, Xi; Zhou, Min; Song, Xiaoyu; Gu, Ming; Sun, Jiaguang: Parallelizing SMT solving: lazy decomposition and conciliation (2018)
  2. Dailler, Sylvain; Hauzar, David; Marché, Claude; Moy, Yannick: Instrumenting a weakest precondition calculus for counterexample generation (2018)
  3. Demri, Stéphane; Dhar, Amit Kumar; Sangnier, Arnaud: Equivalence between model-checking flat counter systems and Presburger arithmetic (2018)
  4. Faghih, Fathiyeh; Bonakdarpour, Borzoo; Tixeuil, Sebastien; Kulkarni, Sandeep: Automated synthesis of distributed self-stabilizing protocols (2018)
  5. Gnad, Daniel; Hoffmann, Jörg: Star-topology decoupled state space search (2018)
  6. Hensel, Jera; Giesl, Jürgen; Frohn, Florian; Ströder, Thomas: Termination and complexity analysis for programs with bitvector arithmetic by symbolic execution (2018)
  7. Lopez-Garcia, P.; Darmawan, L.; Klemen, M.; Liqat, U.; Bueno, F.; Hermenegildo, M. V.: Interval-based resource usage verification by translation into Horn clauses and an application to energy consumption (2018)
  8. Alberti, F.; Ghilardi, S.; Pagani, E.: Cardinality constraints for arrays (decidability results and applications) (2017)
  9. Alpuente, María; Pardo, Daniel; Villanueva, Alicia: Symbolic abstract contract synthesis in a rewriting framework (2017)
  10. Andrea Callia D’Iddio, Michael Huth: Manyopt: An Extensible Tool for Mixed, Non-Linear Optimization Through SMT Solving (2017) arXiv
  11. Bersani, Marcello M.; Rossi, Matteo; San Pietro, Pierluigi: A logical characterization of timed regular languages (2017)
  12. Bromberger, Martin; Weidenbach, Christoph: New techniques for linear arithmetic: cubes and equalities (2017)
  13. Chakraborty, Supratik; Gupta, Ashutosh; Jain, Rahul: Matching multiplications in bit-vector formulas (2017)
  14. Chaudhari, Dipak L.; Damani, Om: Assumption propagation through annotated programs (2017)
  15. 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)
  16. Chihani, Zakaria; Marre, Bruno; Bobot, François; Bardin, Sébastien: Sharpening constraint programming approaches for bit-vector theory (2017)
  17. Chistikov, Dmitry; Dimitrova, Rayna; Majumdar, Rupak: Approximate counting in SMT and value estimation for probabilistic programs (2017)
  18. Dan, Andrei; Meshman, Yuri; Vechev, Martin; Yahav, Eran: Effective abstractions for verification under relaxed memory models (2017)
  19. Demirović, Emir; Musliu, Nysret: Modeling high school timetabling with bitvectors (2017)
  20. Demri, Stéphane; Galmiche, Didier; Larchey-Wendling, Dominique; Méry, Daniel: Separation logic with one quantified variable (2017)

1 2 3 ... 17 18 19 next