On Shostak's Combination of Decision Procedures

Harald Ruess, N. Shankar, and Ashish Tiwari

Tutorial presentation at CADE 2002, which was held as part of FLoC 2002 in Copenhagen, Denmark, July 20--Aug 1, 2002.

Slides

postscript or pdf (preferred)

Errata : Definition of convexity (on Slide 32) should be: A theory is convex if whenever a conjunction of literals implies a disjunction of variable equalities, it also implies one of the disjuncts.

Pictures

BibTeX Entry


@misc{RuessShankarTiwari02:CADE,
	TITLE = {On Shostak's Combination of Decision Procedures},
	AUTHOR = {Ruess, H. and Shankar, N. and Tiwari, A.},
	howpublished = {Available at \url{http://www.csl.sri.com/~tiwari/}}
	YEAR = 2002
}


Return to the Formal Methods Program home page
Return to the Computer Science Laboratory home page