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
- 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,
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
on the combination of decision procedures.
Back to the main ICS homepage
Last updated June 20 2002 by