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

Showing results 1 to 20 of 385.
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. Demri, Stéphane; Dhar, Amit Kumar; Sangnier, Arnaud: Equivalence between model-checking flat counter systems and Presburger arithmetic (2018)
  11. Eisentraut, Christian; Hermanns, Holger; Schuster, Johann; Turrini, Andrea; Zhang, Lijun: The quest for minimal quotients for probabilistic and Markov automata (2018)
  12. Faghih, Fathiyeh; Bonakdarpour, Borzoo; Tixeuil, Sebastien; Kulkarni, Sandeep: Automated synthesis of distributed self-stabilizing protocols (2018)
  13. Ge, Cunjing; Ma, Feifei; Zhang, Peng; Zhang, Jian: Computing and estimating the volume of the solution space of SMT(LA) constraints (2018)
  14. Gnad, Daniel; Hoffmann, Jörg: Star-topology decoupled state space search (2018)
  15. Godefroid, Patrice; Sen, Koushik: Combining model checking and testing (2018)
  16. Hensel, Jera; Giesl, Jürgen; Frohn, Florian; Ströder, Thomas: Termination and complexity analysis for programs with bitvector arithmetic by symbolic execution (2018)
  17. Kojima, Kensuke; Kinoshita, Minoru; Suenaga, Kohei: Generalized homogeneous polynomials for efficient template-based nonlinear invariant synthesis (2018)
  18. Kotelnikov, Evgenii; Kovács, Laura; Voronkov, Andrei: A foolish encoding of the next state relations of imperative programs (2018)
  19. 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)
  20. Malik, Avinash; Walker, Cameron; O’Sullivan, Michael; Sinnen, Oliver: Satisfiability modulo theory (SMT) formulation for optimal scheduling of task graphs with communication delay (2018)

1 2 3 ... 18 19 20 next