Harnessing Disruptive Innovation in Formal Verification

	This Article
	Subscribers, please Login Purchase article: $19 PDF IEEE Xplore Subscribers RSS feed
	Share
	Email this Article to a friend
	Bibliographic References
	ASCII Text BibTex RefWorks Procite/RefMan/Endnote
	Add to:
	Digg Furl Spurl Blink Simpy Google Del.icio.us Y!MyWeb
	Search
	Similar Articles Articles by John Rushby

Fourth IEEE International Conference on Software Engineering and Formal Methods (SEFM'06)

Pune, India

September 11-September 15

ISBN: 0-7695-2678-0

	ASCII Text	x
	John Rushby, "Harnessing Disruptive Innovation in Formal Verification," Software Engineering and Formal Methods, International Conference on, pp. 21-30, Fourth IEEE International Conference on Software Engineering and Formal Methods (SEFM'06), 2006.

	BibTex	x
	@article{ 10.1109/SEFM.2006.24, author = {John Rushby}, title = {Harnessing Disruptive Innovation in Formal Verification}, journal ={Software Engineering and Formal Methods, International Conference on}, volume = {0}, year = {2006}, isbn = {0-7695-2678-0}, pages = {21-30}, doi = {http://doi.ieeecomputersociety.org/10.1109/SEFM.2006.24}, publisher = {IEEE Computer Society}, address = {Los Alamitos, CA, USA}, }

	RefWorks Procite/RefMan/Endnote	x
	TY - CONF JO - Software Engineering and Formal Methods, International Conference on TI - Harnessing Disruptive Innovation in Formal Verification SN - 0-7695-2678-0 SP21 EP30 A1 - John Rushby, PY - 2006 KW - null VL - 0 JA - Software Engineering and Formal Methods, International Conference on ER -

John Rushby, SRI International, USA

DOI Bookmark: http://doi.ieeecomputersociety.org/10.1109/SEFM.2006.24

Technological innovations are sweeping through the field of formal verification. These changes are disruptive to tools based on interactive theorem proving, which needs new

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.

Citation:

John Rushby, "Harnessing Disruptive Innovation in Formal Verification," sefm, pp.21-30, Fourth IEEE International Conference on Software Engineering and Formal Methods (SEFM'06), 2006

Peer Review Notice | Give Us Feedback

Usage of this product signifies your acceptance of the Terms of Use.