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

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

1 2 3 next

  1. Andrea Callia D’Iddio, Michael Huth: Manyopt: An Extensible Tool for Mixed, Non-Linear Optimization Through SMT Solving (2017) arXiv
  2. Ansótegui, Carlos; Gabàs, Joel; Levy, Jordi: Exploiting subproblem optimization in SAT-based maxsat algorithms (2016)
  3. Craciunas, Silviu S.; Oliver, Ramon Serna: Combined task- and network-level scheduling for distributed time-triggered systems (2016)
  4. Kovásznai, Gergely; Fröhlich, Andreas; Biere, Armin: Complexity of fixed-size bit-vector logics (2016)
  5. Liu, Shaoying: Testing-based formal verification for theorems and its application in software specification verification (2016)
  6. Tiwari, Ashish; Lincoln, Patrick: A search-based procedure for nonlinear real arithmetic (2016)
  7. Cimatti, Alessandro; Micheli, Andrea; Roveri, Marco: An SMT-based approach to weak controllability for disjunctive temporal problems with uncertainty (2015)
  8. Cimatti, Alessandro; Micheli, Andrea; Roveri, Marco: Solving strong controllability of temporal problems with uncertainty using SMT (2015)
  9. Michels, Steffen; Hommersom, Arjen; Lucas, Peter J.F.; Velikova, Marina: A new probabilistic constraint logic programming language based on a generalised distribution semantics (2015)
  10. Subramani, K.; Worthington, James: Feasibility checking in Horn constraint systems through a reduction based approach (2015)
  11. Tiwari, Ashish: Attacking a feedback controller (2015) ioport
  12. 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)
  13. Dixit, Manoj G.; Ramesh, S.; Dasgupta, Pallab: Time-budgeting: a component based development methodology for real-time embedded systems (2014)
  14. Ansótegui, Carlos; Bofill, Miquel; Palahí, Miquel; Suy, Josep; Villaret, Mateu: Solving weighted CSPs with meta-constraints by reformulation into satisfiability modulo theories (2013)
  15. Blanchette, Jasmin Christian; Böhme, Sascha; Paulson, Lawrence C.: Extending Sledgehammer with SMT solvers (2013)
  16. Chandrasekaran, R.; Subramani, K.: A combinatorial algorithm for Horn programs (2013)
  17. Jovanović, Dejan; Barrett, Clark: Being careful about theory combination (2013)
  18. Bofill, Miquel; Palahí, Miquel; Suy, Josep; Villaret, Mateu: Solving constraint satisfaction problems with SAT modulo theories (2012)
  19. Echenim, Mnacho; Peltier, Nicolas: An instantiation scheme for satisfiability modulo theories (2012)
  20. Gawlitza, Thomas Martin; Monniaux, David: Invariant generation through strategy iteration in succinctly represented control flow graphs (2012)

1 2 3 next