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

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

1 2 3 ... 18 19 20 next

  1. Bao, Yuyan; Leavens, Gary T.; Ernst, Gidon: Unifying separation logic and region logic to allow interoperability (2018)
  2. Barrett, Clark; Tinelli, Cesare: Satisfiability modulo theories (2018)
  3. Bart, Anicet; Delahaye, Beno^ıt; Fournier, Paulin; Lime, Didier; Monfroy, Éric; Truchet, Charlotte: Reachability in parametric interval Markov chains using constraints (2018)
  4. Blanchette, Jasmin Christian; Fleury, Mathias; Lammich, Peter; Weidenbach, Christoph: A verified SAT solver framework with learn, forget, restart, and incrementality (2018)
  5. Cheng, Xi; Zhou, Min; Song, Xiaoyu; Gu, Ming; Sun, Jiaguang: Parallelizing SMT solving: lazy decomposition and conciliation (2018)
  6. Chen, Hao; Wu, Xiongnan; Shao, Zhong; Lockerman, Joshua; Gu, Ronghui: Toward compositional verification of interruptible OS kernels and device drivers (2018)
  7. Cox, Christopher; Stolee, Derrick: Ramsey numbers for partially-ordered sets (2018)
  8. Czajka, Łukasz; Kaliszyk, Cezary: Hammer for Coq: automation for dependent type theory (2018)
  9. Dailler, Sylvain; Hauzar, David; Marché, Claude; Moy, Yannick: Instrumenting a weakest precondition calculus for counterexample generation (2018)
  10. De Angelis, Emanuele; Fioravanti, Fabio; Pettorossi, Alberto; Proietti, Maurizio: Solving Horn clauses on inductive data types without induction (2018)
  11. Demri, Stéphane; Dhar, Amit Kumar; Sangnier, Arnaud: Equivalence between model-checking flat counter systems and Presburger arithmetic (2018)
  12. Eisentraut, Christian; Hermanns, Holger; Schuster, Johann; Turrini, Andrea; Zhang, Lijun: The quest for minimal quotients for probabilistic and Markov automata (2018)
  13. Faghih, Fathiyeh; Bonakdarpour, Borzoo; Tixeuil, Sebastien; Kulkarni, Sandeep: Automated synthesis of distributed self-stabilizing protocols (2018)
  14. Ge, Cunjing; Ma, Feifei; Zhang, Peng; Zhang, Jian: Computing and estimating the volume of the solution space of SMT(LA) constraints (2018)
  15. Geffroy, Thomas; Leroux, Jér^ome; Sutre, Grégoire: Occam’s razor applied to the Petri net coverability problem (2018)
  16. Gnad, Daniel; Hoffmann, Jörg: Star-topology decoupled state space search (2018)
  17. Godefroid, Patrice; Sen, Koushik: Combining model checking and testing (2018)
  18. Hague, Matthew; Lin, Anthony W.: Decidable models of integer-manipulating programs with recursive parallelism (2018)
  19. Hensel, Jera; Giesl, Jürgen; Frohn, Florian; Ströder, Thomas: Termination and complexity analysis for programs with bitvector arithmetic by symbolic execution (2018)
  20. Hong, Hoon; Sturm, Thomas: Positive solutions of systems of signed parametric polynomial inequalities (2018)

1 2 3 ... 18 19 20 next