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

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

1 2 3 ... 6 7 8 next

  1. Bofill, Miquel; Coll, Jordi; Martín, Gerard; Suy, Josep; Villaret, Mateu: The sample analysis machine scheduling problem: definition and comparison of exact solving approaches (2022)
  2. Bonacina, Maria Paola; Graham-Lengrand, Stéphane; Shankar, Natarajan: Conflict-driven satisfiability for theory combination: lemmas, modules, and proofs (2022)
  3. Stehr, Mark-Oliver; Kim, Minyoung; Talcott, Carolyn L.: A probabilistic approximate logic for neuro-symbolic learning and reasoning (2022)
  4. Bjørner, Nikolaj; Levatich, Maxwell; Lopes, Nuno P.; Rybalchenko, Andrey; Vuppalapati, Chandrasekar: Supercharging plant configurations using Z3 (2021)
  5. Kwiatkowska, Marta; Norman, Gethin; Parker, David; Santos, Gabriel: Automatic verification of concurrent stochastic systems (2021)
  6. Luteberget, Bjørnar; Claessen, Koen; Johansen, Christian; Steffen, Martin: SAT modulo discrete event simulation applied to railway design capacity analysis (2021)
  7. Mann, Makai; Wilson, Amalee; Zohar, Yoni; Stuntz, Lindsey; Irfan, Ahmed; Brown, Kristopher; Donovick, Caleb; Guman, Allison; Tinelli, Cesare; Barrett, Clark: Smt-Switch: a solver-agnostic C++ API for SMT solving (2021)
  8. Niemetz, Aina; Preiner, Mathias; Reynolds, Andrew; Barrett, Clark; Tinelli, Cesare: On solving quantified bit-vector constraints using invertibility conditions (2021)
  9. Pimpalkhare, Nikhil; Mora, Federico; Polgreen, Elizabeth; Seshia, Sanjit A.: MedleySolver: online SMT algorithm selection (2021)
  10. Subramani, K.; Wojciechowski, P.: On the parametrized complexity of Read-once refutations in UTVPI+ constraint systems (2021)
  11. Winkler, Sarah; Moser, Georg: Runtime complexity analysis of logically constrained rewriting (2021)
  12. Bonacina, Maria Paola; Graham-Lengrand, Stéphane; Shankar, Natarajan: Conflict-driven satisfiability for theory combination: transition system and completeness (2020)
  13. Bromberger, Martin; Sturm, Thomas; Weidenbach, Christoph: A complete and terminating approach to linear integer solving (2020)
  14. Calvanese, Diego; Ghilardi, Silvio; Gianola, Alessandro; Montali, Marco; Rivkin, Andrey: SMT-based verification of data-aware processes: a model-theoretic approach (2020)
  15. Durán, Francisco; Eker, Steven; Escobar, Santiago; Martí-Oliet, Narciso; Meseguer, José; Rubio, Rubén; Talcott, Carolyn: Programming and symbolic computation in Maude (2020)
  16. Rümmer, Philipp: Competition report: CHC-COMP-20 (2020)
  17. Sebastiani, Roberto; Trentin, Patrick: \textscOptiMathSAT: a tool for optimization modulo theories (2020)
  18. 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)
  19. Wojciechowski, Piotr; Chandrasekaran, R.; Subramani, K.: Analyzing fractional Horn constraint systems (2020)
  20. Akgün, Özgür; Gent, Ian; Kitaev, Sergey; Zantema, Hans: Solving computational problems in the theory of word-representable graphs (2019)

1 2 3 ... 6 7 8 next