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

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

1 2 3 ... 5 6 7 next

  1. Bonacina, Maria Paola; Graham-Lengrand, Stéphane; Shankar, Natarajan: Conflict-driven satisfiability for theory combination: transition system and completeness (2020)
  2. Bromberger, Martin; Sturm, Thomas; Weidenbach, Christoph: A complete and terminating approach to linear integer solving (2020)
  3. Calvanese, Diego; Ghilardi, Silvio; Gianola, Alessandro; Montali, Marco; Rivkin, Andrey: SMT-based verification of data-aware processes: a model-theoretic approach (2020)
  4. Durán, Francisco; Eker, Steven; Escobar, Santiago; Martí-Oliet, Narciso; Meseguer, José; Rubio, Rubén; Talcott, Carolyn: Programming and symbolic computation in Maude (2020)
  5. Sebastiani, Roberto; Trentin, Patrick: \textscOptiMathSAT: a tool for optimization modulo theories (2020)
  6. Semenov, Alexander; Otpuschennikov, Ilya; Gribanova, Irina; Zaikin, Oleg; Kochemazov, Stepan: Translation of algorithmic descriptions of discrete functions to SAT with applications to cryptanalysis problems (2020)
  7. Wojciechowski, Piotr; Chandrasekaran, R.; Subramani, K.: Analyzing fractional Horn constraint systems (2020)
  8. Akgün, Özgür; Gent, Ian; Kitaev, Sergey; Zantema, Hans: Solving computational problems in the theory of word-representable graphs (2019)
  9. Bofill, Miquel; Manyà, Felip; Vidal, Amanda; Villaret, Mateu: New complexity results for Łukasiewicz logic (2019)
  10. Borralleras, Cristina; Larraz, Daniel; Rodríguez-Carbonell, Enric; Oliveras, Albert; Rubio, Albert: Incomplete SMT techniques for solving non-linear formulas over the integers (2019)
  11. Bright, Curtis; Đoković, Dragomir Ž.; Kotsireas, Ilias; Ganesh, Vijay: The SAT+CAS method for combinatorial search with applications to best matrices (2019)
  12. Bromberger, Martin; Fleury, Mathias; Schwarz, Simon; Weidenbach, Christoph: SPASS-SATT. A CDCL(LA) solver (2019)
  13. Calvanese, Diego; Ghilardi, Silvio; Gianola, Alessandro; Montali, Marco; Rivkin, Andrey: From model completeness to verification of data aware processes (2019)
  14. Gutiérrez, Raúl; Lucas, Salvador: Automatic generation of logical models with AGES (2019)
  15. Hirokawa, Nao; Nagele, Julian; van Oostrom, Vincent; Oyamaguchi, Michio: Confluence by critical pair analysis revisited (2019)
  16. Kobayashi, Koichi: Design of fixed points in Boolean networks using feedback vertex sets and model reduction (2019)
  17. Reynolds, Andrew; Kuncak, Viktor; Tinelli, Cesare; Barrett, Clark; Deters, Morgan: Refutation-based synthesis in SMT (2019)
  18. Wang, Wenxi; Søndergaard, Harald; Stuckey, Peter J.: Wombit: a portfolio bit-vector solver using word-level propagation (2019)
  19. Barrett, Clark; Tinelli, Cesare: Satisfiability modulo theories (2018)
  20. Cheng, Xi; Zhou, Min; Song, Xiaoyu; Gu, Ming; Sun, Jiaguang: Parallelizing SMT solving: lazy decomposition and conciliation (2018)

1 2 3 ... 5 6 7 next