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

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

1 2 3 ... 19 20 21 next

  1. Li, Wenda; Passmore, Grant Olney; Paulson, Lawrence C.: Deciding univariate polynomial problems using untrusted certificates in Isabelle/HOL (2019)
  2. Bao, Yuyan; Leavens, Gary T.; Ernst, Gidon: Unifying separation logic and region logic to allow interoperability (2018)
  3. Barrett, Clark; Tinelli, Cesare: Satisfiability modulo theories (2018)
  4. Bart, Anicet; Delahaye, Benoît; Fournier, Paulin; Lime, Didier; Monfroy, Éric; Truchet, Charlotte: Reachability in parametric interval Markov chains using constraints (2018)
  5. Bendík, Jaroslav; Černá, Ivana: Evaluation of domain agnostic approaches for enumeration of minimal unsatisfiable subsets (2018)
  6. Blanchette, Jasmin Christian; Fleury, Mathias; Lammich, Peter; Weidenbach, Christoph: A verified SAT solver framework with learn, forget, restart, and incrementality (2018)
  7. Blanchette, Jasmin Christian; Peltier, Nicolas; Robillard, Simon: Superposition with datatypes and codatatypes (2018)
  8. Bromberger, Martin: A reduction from unbounded linear mixed arithmetic problems into bounded problems (2018)
  9. Cheng, Xi; Zhou, Min; Song, Xiaoyu; Gu, Ming; Sun, Jiaguang: Parallelizing SMT solving: lazy decomposition and conciliation (2018)
  10. Chen, Hao; Wu, Xiongnan; Shao, Zhong; Lockerman, Joshua; Gu, Ronghui: Toward compositional verification of interruptible OS kernels and device drivers (2018)
  11. Cox, Christopher; Stolee, Derrick: Ramsey numbers for partially-ordered sets (2018)
  12. Czajka, Łukasz; Kaliszyk, Cezary: Hammer for Coq: automation for dependent type theory (2018)
  13. Dailler, Sylvain; Hauzar, David; Marché, Claude; Moy, Yannick: Instrumenting a weakest precondition calculus for counterexample generation (2018)
  14. De Angelis, Emanuele; Fioravanti, Fabio; Pettorossi, Alberto; Proietti, Maurizio: Solving Horn clauses on inductive data types without induction (2018)
  15. Demri, Stéphane; Dhar, Amit Kumar; Sangnier, Arnaud: Equivalence between model-checking flat counter systems and Presburger arithmetic (2018)
  16. Echenim, Mnacho; Peltier, Nicolas; Sellami, Yanis: A generic framework for implicate generation modulo theories (2018)
  17. Eisentraut, Christian; Hermanns, Holger; Schuster, Johann; Turrini, Andrea; Zhang, Lijun: The quest for minimal quotients for probabilistic and Markov automata (2018)
  18. Faghih, Fathiyeh; Bonakdarpour, Borzoo; Tixeuil, Sebastien; Kulkarni, Sandeep: Automated synthesis of distributed self-stabilizing protocols (2018)
  19. Farinier, Benjamin; David, Robin; Bardin, Sébastien; Lemerre, Matthieu: Arrays made simpler: an efficient, scalable and thorough preprocessing (2018)
  20. Ge, Cunjing; Ma, Feifei; Zhang, Peng; Zhang, Jian: Computing and estimating the volume of the solution space of SMT(LA) constraints (2018)

1 2 3 ... 19 20 21 next