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

Showing results 1 to 20 of 55.
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. Craciunas, Silviu S.; Oliver, Ramon Serna: Combined task- and network-level scheduling for distributed time-triggered systems (2016)
  3. Kovásznai, Gergely; Fröhlich, Andreas; Biere, Armin: Complexity of fixed-size bit-vector logics (2016)
  4. Liu, Shaoying: Testing-based formal verification for theorems and its application in software specification verification (2016)
  5. Cimatti, Alessandro; Micheli, Andrea; Roveri, Marco: An SMT-based approach to weak controllability for disjunctive temporal problems with uncertainty (2015)
  6. Cimatti, Alessandro; Micheli, Andrea; Roveri, Marco: Solving strong controllability of temporal problems with uncertainty using SMT (2015)
  7. Michels, Steffen; Hommersom, Arjen; Lucas, Peter J.F.; Velikova, Marina: A new probabilistic constraint logic programming language based on a generalised distribution semantics (2015)
  8. Subramani, K.; Worthington, James: Feasibility checking in Horn constraint systems through a reduction based approach (2015)
  9. Tiwari, Ashish: Attacking a feedback controller (2015)
  10. 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)
  11. Dixit, Manoj G.; Ramesh, S.; Dasgupta, Pallab: Time-budgeting: a component based development methodology for real-time embedded systems (2014)
  12. Ansótegui, Carlos; Bofill, Miquel; Palahí, Miquel; Suy, Josep; Villaret, Mateu: Solving weighted CSPs with meta-constraints by reformulation into satisfiability modulo theories (2013)
  13. Blanchette, Jasmin Christian; Böhme, Sascha; Paulson, Lawrence C.: Extending Sledgehammer with SMT solvers (2013)
  14. Chandrasekaran, R.; Subramani, K.: A combinatorial algorithm for Horn programs (2013)
  15. Jovanović, Dejan; Barrett, Clark: Being careful about theory combination (2013)
  16. Bofill, Miquel; Palahí, Miquel; Suy, Josep; Villaret, Mateu: Solving constraint satisfaction problems with SAT modulo theories (2012)
  17. Echenim, Mnacho; Peltier, Nicolas: An instantiation scheme for satisfiability modulo theories (2012)
  18. Gawlitza, Thomas Martin; Monniaux, David: Invariant generation through strategy iteration in succinctly represented control flow graphs (2012)
  19. Köksal, Ali Sinan; Kuncak, Viktor; Suter, Philippe: Constraints as control (2012)
  20. Lee, Wonchan; Jung, Yungbum; Wang, Bow-Yaw; Yi, Kwangkuen: Predicate generation for learning-based quantifier-free loop invariant inference (2012)

1 2 3 next