Papers

Some of the algorithms and data structures underlying ICS have been published.

• Combining Shostak Theories
  by: N. Shankar and Harald Rueß
  Invited paper for RTA'02.
• Lazy Theorem Proving for Bounded Model Checking over Infinite Domains
  by Leonardo de Moura, Harald Rueß, and Maria Sorea
  CADE'2002.
• ICS: Integrated Canonizer and Solver
  by: Jean-Christophe Filliatre and Sam Owre and Harald Rueß and N. Shankar,
  Published at CAV'2001.
• Deconstructing Shostak
  by: Harald Rueß and N. Shankar,
  Published at LICS'2001.
• Solving Bitvector Equations
  by: M. Oliver Möller and Harald Rueß
  In: Formal Methods in Computer-Aided Design (FMCAD'98), G. Gopalakrishnan, Ph. Windley (Eds.), pp. 36--48, ] Palo Alto, CA, November, 1998, volume 1522 of LNCS, Springer Verlag.
• An Efficient Decision Procedure for the Theory of Fixed-Sized Bitvectors
  by David Cyrluk, M. Oliver Möller, Harald Rueß
  In Orna Grumberg (Ed.), Proceedings of 9th International Conference on Computer Aided Verification, CAV'97, Haifa, Israel, June, 1997, volume 1254 of LNCS, Springer-Verlag.

There are also slides of a tutorial on the combination of decision procedures.

Back to the main ICS homepage

Last updated June 20 2002 by Harald Rueß