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

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

1 2 3 ... 17 18 19 next

  1. Barrett, Clark; Tinelli, Cesare: Satisfiability modulo theories (2018)
  2. Blanchette, Jasmin Christian; Fleury, Mathias; Lammich, Peter; Weidenbach, Christoph: A verified SAT solver framework with learn, forget, restart, and incrementality (2018)
  3. Cheng, Xi; Zhou, Min; Song, Xiaoyu; Gu, Ming; Sun, Jiaguang: Parallelizing SMT solving: lazy decomposition and conciliation (2018)
  4. Chen, Hao; Wu, Xiongnan; Shao, Zhong; Lockerman, Joshua; Gu, Ronghui: Toward compositional verification of interruptible OS kernels and device drivers (2018)
  5. Czajka, Łukasz; Kaliszyk, Cezary: Hammer for Coq: automation for dependent type theory (2018)
  6. Dailler, Sylvain; Hauzar, David; Marché, Claude; Moy, Yannick: Instrumenting a weakest precondition calculus for counterexample generation (2018)
  7. Demri, Stéphane; Dhar, Amit Kumar; Sangnier, Arnaud: Equivalence between model-checking flat counter systems and Presburger arithmetic (2018)
  8. Faghih, Fathiyeh; Bonakdarpour, Borzoo; Tixeuil, Sebastien; Kulkarni, Sandeep: Automated synthesis of distributed self-stabilizing protocols (2018)
  9. Ge, Cunjing; Ma, Feifei; Zhang, Peng; Zhang, Jian: Computing and estimating the volume of the solution space of SMT(LA) constraints (2018)
  10. Gnad, Daniel; Hoffmann, Jörg: Star-topology decoupled state space search (2018)
  11. Godefroid, Patrice; Sen, Koushik: Combining model checking and testing (2018)
  12. Hensel, Jera; Giesl, Jürgen; Frohn, Florian; Ströder, Thomas: Termination and complexity analysis for programs with bitvector arithmetic by symbolic execution (2018)
  13. 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)
  14. Malik, Avinash; Walker, Cameron; O’Sullivan, Michael; Sinnen, Oliver: Satisfiability modulo theory (SMT) formulation for optimal scheduling of task graphs with communication delay (2018)
  15. McMillan, Kenneth L.: Interpolation and model checking (2018)
  16. Alberti, F.; Ghilardi, S.; Pagani, E.: Cardinality constraints for arrays (decidability results and applications) (2017)
  17. Alpuente, María; Pardo, Daniel; Villanueva, Alicia: Symbolic abstract contract synthesis in a rewriting framework (2017)
  18. Andrea Callia D’Iddio, Michael Huth: Manyopt: An Extensible Tool for Mixed, Non-Linear Optimization Through SMT Solving (2017) arXiv
  19. Bersani, Marcello M.; Rossi, Matteo; San Pietro, Pierluigi: A logical characterization of timed regular languages (2017)
  20. Bromberger, Martin; Weidenbach, Christoph: New techniques for linear arithmetic: cubes and equalities (2017)

1 2 3 ... 17 18 19 next