Yices

Yices is an efficient SMT solver that decides the satisfiability of arbitrary formulas containing uninterpreted function symbols with equality, linear real and integer arithmetic, scalar types, recursive datatypes, tuples, records, extensional arrays, fixed-size bit-vectors, quantifiers, and lambda expressions. Yices also does MaxSMT (and, dually, unsat cores) and is competitive as an ordinary SAT and MaxSAT solver.


References in zbMATH (referenced in 84 articles )

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

1 2 3 4 5 next

  1. Cheng, Xi; Zhou, Min; Song, Xiaoyu; Gu, Ming; Sun, Jiaguang: Parallelizing SMT solving: lazy decomposition and conciliation (2018)
  2. Orlin, James B.; Subramani, K.; Wojciechowki, Piotr: Randomized algorithms for finding the shortest negative cost cycle in networks (2018)
  3. Andrea Callia D’Iddio, Michael Huth: Manyopt: An Extensible Tool for Mixed, Non-Linear Optimization Through SMT Solving (2017) arXiv
  4. Chakraborty, Supratik; Khasidashvili, Zurab; Seger, Carl-Johan H.; Gajavelly, Rajkumar; Haldankar, Tanmay; Chhatani, Dinesh; Mistry, Rakesh: Symbolic trajectory evaluation for word-level verification: theory and implementation (2017)
  5. Don, Henk; Zantema, Hans: Finding DFAs with maximal shortest synchronizing word length (2017)
  6. 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)
  7. Gleiss, Bernhard; Kovács, Laura; Suda, Martin: Splitting proofs for interpolation (2017)
  8. Ströder, Thomas; Giesl, Jürgen; Brockschmidt, Marc; Frohn, Florian; Fuhs, Carsten; Hensel, Jera; Schneider-Kamp, Peter; Aschermann, Cornelius: Automatically proving termination and memory safety for programs with pointer arithmetic (2017)
  9. Ansótegui, Carlos; Bofill, Miquel; Manyà, Felip; Villaret, Mateu: Automated theorem provers for multiple-valued logics with satisfiability modulo theory solvers (2016)
  10. Ansótegui, Carlos; Gabàs, Joel; Levy, Jordi: Exploiting subproblem optimization in SAT-based maxsat algorithms (2016)
  11. Banković, Milan: Extending SMT solvers with support for finite domain alldifferent constraint (2016)
  12. Craciunas, Silviu S.; Oliver, Ramon Serna: Combined task- and network-level scheduling for distributed time-triggered systems (2016)
  13. Echenim, Mnacho; Peltier, Nicolas: A superposition calculus for abductive reasoning (2016)
  14. Kovásznai, Gergely; Fröhlich, Andreas; Biere, Armin: Complexity of fixed-size bit-vector logics (2016)
  15. Liu, Shaoying: Testing-based formal verification for theorems and its application in software specification verification (2016)
  16. Petrenko, Alexandre; Nguena Timo, Omer; Ramesh, S.: Multiple mutation testing from FSM (2016)
  17. Tiwari, Ashish; Lincoln, Patrick: A search-based procedure for nonlinear real arithmetic (2016)
  18. Cimatti, Alessandro; Micheli, Andrea; Roveri, Marco: Solving strong controllability of temporal problems with uncertainty using SMT (2015)
  19. Cimatti, Alessandro; Micheli, Andrea; Roveri, Marco: An SMT-based approach to weak controllability for disjunctive temporal problems with uncertainty (2015)
  20. Michels, Steffen; Hommersom, Arjen; Lucas, Peter J. F.; Velikova, Marina: A new probabilistic constraint logic programming language based on a generalised distribution semantics (2015)

1 2 3 4 5 next