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

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

1 2 3 ... 14 15 16 next

  1. Alpuente, María; Pardo, Daniel; Villanueva, Alicia: Symbolic abstract contract synthesis in a rewriting framework (2017)
  2. Andrea Callia D’Iddio, Michael Huth: Manyopt: An Extensible Tool for Mixed, Non-Linear Optimization Through SMT Solving (2017) arXiv
  3. Bersani, Marcello M.; Rossi, Matteo; San Pietro, Pierluigi: A logical characterization of timed regular languages (2017)
  4. Chakraborty, Supratik; Gupta, Ashutosh; Jain, Rahul: Matching multiplications in bit-vector formulas (2017)
  5. Chaudhari, Dipak L.; Damani, Om: Assumption propagation through annotated programs (2017)
  6. 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)
  7. Chihani, Zakaria; Marre, Bruno; Bobot, François; Bardin, Sébastien: Sharpening constraint programming approaches for bit-vector theory (2017)
  8. Chistikov, Dmitry; Dimitrova, Rayna; Majumdar, Rupak: Approximate counting in SMT and value estimation for probabilistic programs (2017)
  9. Demirović, Emir; Musliu, Nysret: Modeling high school timetabling with bitvectors (2017)
  10. Demri, Stéphane; Galmiche, Didier; Larchey-Wendling, Dominique; Méry, Daniel: Separation logic with one quantified variable (2017)
  11. Dinsdale-Young, Thomas; da Rocha Pinto, Pedro; Andersen, Kristoffer Just; Birkedal, Lars: Caper - automatic verification for fine-grained concurrency (2017)
  12. Esparza, Javier: Advances in parameterized verification of population protocols (2017)
  13. Frohn, Florian; Giesl, Jürgen; Hensel, Jera; Aschermann, Cornelius; Ströder, Thomas: Lower bounds for runtime complexity of term rewriting (2017)
  14. 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)
  15. Fuhs, Carsten; Kop, Cynthia; Nishida, Naoki: Verifying procedural programs via constrained rewriting induction (2017)
  16. 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)
  17. 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)
  18. Grimmer, Andreas; Clemens, Joachim; Wille, Robert: Formal methods for reasoning and uncertainty reduction in evidential grid maps (2017)
  19. Jovanović, Dejan: Solving nonlinear integer arithmetic with MCSAT (2017)
  20. Konnov, Igor; Lazić, Marijana; Veith, Helmut; Widder, Josef: A short counterexample property for safety and liveness verification of fault-tolerant distributed algorithms (2017)

1 2 3 ... 14 15 16 next