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 63 articles )

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

1 2 3 4 next

  1. Andrea Callia D’Iddio, Michael Huth: Manyopt: An Extensible Tool for Mixed, Non-Linear Optimization Through SMT Solving (2017) arXiv
  2. 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)
  3. 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)
  4. 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)
  5. Ansótegui, Carlos; Gabàs, Joel; Levy, Jordi: Exploiting subproblem optimization in SAT-based maxsat algorithms (2016)
  6. Banković, Milan: Extending SMT solvers with support for finite domain alldifferent constraint (2016)
  7. Craciunas, Silviu S.; Oliver, Ramon Serna: Combined task- and network-level scheduling for distributed time-triggered systems (2016)
  8. Echenim, Mnacho; Peltier, Nicolas: A superposition calculus for abductive reasoning (2016)
  9. Kovásznai, Gergely; Fröhlich, Andreas; Biere, Armin: Complexity of fixed-size bit-vector logics (2016)
  10. Liu, Shaoying: Testing-based formal verification for theorems and its application in software specification verification (2016)
  11. Tiwari, Ashish; Lincoln, Patrick: A search-based procedure for nonlinear real arithmetic (2016)
  12. Cimatti, Alessandro; Micheli, Andrea; Roveri, Marco: An SMT-based approach to weak controllability for disjunctive temporal problems with uncertainty (2015)
  13. Cimatti, Alessandro; Micheli, Andrea; Roveri, Marco: Solving strong controllability of temporal problems with uncertainty using SMT (2015)
  14. Michels, Steffen; Hommersom, Arjen; Lucas, Peter J.F.; Velikova, Marina: A new probabilistic constraint logic programming language based on a generalised distribution semantics (2015)
  15. Subramani, K.; Worthington, James: Feasibility checking in Horn constraint systems through a reduction based approach (2015)
  16. Tiwari, Ashish: Attacking a feedback controller (2015) ioport
  17. Zhou, Min; He, Fei; Song, Xiaoyu; He, Shi; Chen, Gangyi; Gu, Ming: Estimating the volume of solution space for satisfiability modulo linear real arithmetic (2015)
  18. Dixit, Manoj G.; Ramesh, S.; Dasgupta, Pallab: Time-budgeting: a component based development methodology for real-time embedded systems (2014)
  19. Ansótegui, Carlos; Bofill, Miquel; Palahí, Miquel; Suy, Josep; Villaret, Mateu: Solving weighted CSPs with meta-constraints by reformulation into satisfiability modulo theories (2013)
  20. Blanchette, Jasmin Christian; Böhme, Sascha; Paulson, Lawrence C.: Extending Sledgehammer with SMT solvers (2013)

1 2 3 4 next