John Rushby

Invited paper, presented at the 4th IEEE International Conference on Software Engineering and Formal Methods (SEFM), Pune, India, September 2006. Appears in the proceedings, pp. 21--28, © IEEE Computer Society

Abstract

I describe two approaches. One is development and use of SMT solvers: these use techniques from theorem proving but apply them in ways that enable model checking, while also supporting highly automated theorem proving. The other is a proposal for an Evidential Tool Bus: a loosely coupled architecture that allows many different verification components to collaborate to solve problems beyond the capability of any single component.

gzipped postscript, or plain postscript or PDF or crude ascii (for your Palm Pilot)

And here's a link to Wikipedia's article on Disruptive Technology

Slides

gzipped postscript, or plain postscript or PDF or crude ascii (for your Palm Pilot)

BibTeX Entry

@INPROCEEDINGS{Rushby06:SEFM,
	AUTHOR = {John Rushby},
	TITLE = {Harnessing Disruptive Innovation in Formal Verification},
	EDITOR = {Dang Van Hung and Paritosh Pandya},
	BOOKTITLE = {Fourth International Conference on Software Engineering and Formal Methods ({SEFM})},
	ADDRESS = {Pune, India},
	ORGANIZATION = {IEEE Computer Society},
	MONTH = sep,
	YEAR = 2006
	PAGES = {21--28}
}