ICS is deprecated and no longer supported (since August 2006). Please use Yices instead; Yices is much faster, handles more theories, and has several other advantages. ICS: Integrated canonizer and solver. ICS (Integrated Canonizer and Solver) is an efficient decision procedure for a fragment of first-order logic. Terms are built from uninterpreted function symbols and operators from a rich combination of datatypes including arithmetic, functional arrays, tuples, cotuples, and fixed-sized bitvectors. It incorporates a state-of-the-art SAT solver. ICS can be used as a standalone application that reads formulas interactively, and may also be included as a library in any application that requires embedded deduction.

References in zbMATH (referenced in 20 articles , 1 standard article )

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

  1. Kroening, Daniel; Strichman, Ofer: Decision procedures. An algorithmic point of view (2016)
  2. Meseguer, José: Variant-based satisfiability in initial algebras (2016)
  3. Barrett, Clark; Deters, Morgan; de Moura, Leonardo; Oliveras, Albert; Stump, Aaron: 6 years of SMT-COMP (2013) ioport
  4. Konur, Savas: A survey on temporal logics for specifying and verifying real-time systems (2013)
  5. Strichman, Ofer (ed.); Kroening, Daniel (ed.): Preface to the special issue “SI: satisfiability modulo theories” (2013)
  6. Bruttomesso, Roberto; Cimatti, Alessandro; Franzen, Anders; Griggio, Alberto; Sebastiani, Roberto: Delayed theory combination vs. Nelson-Oppen for satisfiability modulo theories: a comparative analysis (2009)
  7. Kroening, Daniel; Strichman, Ofer: A framework for satisfiability modulo theories (2009)
  8. Badban, Bahareh; Van De Pol, Jaco; Tveretina, Olga; Zantema, Hans: Generalizing DPLL and satisfiability for equalities (2007)
  9. Basin, David; Kuruma, Hironobu; Miyazaki, Kunihiko; Takaragi, Kazuo; Wolff, Burkhart: Verifying a signature architecture: a comparative case study (2007)
  10. Bozzano, Marco; Bruttomesso, Roberto; Cimatti, Alessandro; Junttila, Tommi; Ranise, Silvio; Van Rossum, Peter; Sebastiani, Roberto: Efficient theory combination via Boolean search (2006)
  11. Currie, David; Feng, Xiushan; Fujita, Masahiro; Hu, Alan J.; Kwan, Mark; Rajan, Sreeranga: Embedded software verification using symbolic execution and uninterpreted functions (2006)
  12. Ireland, Andrew; Ellis, Bill J.; Cook, Andrew; Chapman, Roderick; Barnes, Janet: An integrated approach to high integrity software verification (2006)
  13. Rodeh, Yoav; Strichman, Ofer: Building small equality graphs for deciding equality logic with uninterpreted functions (2006)
  14. Barrett, Clark; de Moura, Leonardo; Stump, Aaron: Design and results of the first satisfiability modulo theories competition (SMT-COMP 2005) (2005)
  15. Bozzano, Marco; Bruttomesso, Roberto; Cimatti, Alessandro; Junttila, Tommi; van Rossum, Peter; Schulz, Stephan; Sebastiani, Roberto: M\textbfathSAT: Tight integration of SAT and mathematical decision procedures (2005)
  16. Yorsh, Greta; Musuvathi, Madanlal: A combination method for generating interpolants (2005)
  17. Zuck, Lenore; Pnueli, Amir; Goldberg, Benjamin; Barrett, Clark; Fang, Yi; Hu, Ying: Translation and run-time validation of loop transformations (2005)
  18. Sorea, Maria: Bounded model checking for timed automata (2003)
  19. Filliâtre, Jean-Christophe; Owre, Sam; Rueß, Harald; Shankar, Natarajan: ICS: Integrated canonizer and solver (2001)
  20. Rusu, Vlad; Zinovieva, Elena: Analyzing automata with Presburger arithmetic and uninterpreted function symbols (2001)