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

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

1 2 3 next

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

1 2 3 next