Paper Info
Title
Harnessing Disruptive Innovation in Formal Verification
Abstract
Technological innovations are sweeping through the field of formal verification. These changes are disruptive to tools based on interactive theorem proving, which needs new ways to integrate the capabilities of novel technologies. 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
Year
DOI
Venue
2006
10.1109/SEFM.2006.24
SEFM
Keywords
Field
DocType
software systems,formal verification,theorem prover,theorem proving,formal specification,type system,higher order,interactive theorem proving,model checking,automated theorem proving,complex system,data structure
Architecture,Disruptive innovation,Programming language,Model checking,Computer science,Automated theorem proving,Theoretical computer science,Formal verification,Proof assistant
Conference
ISSN
ISBN
Citations 
1551-0255
0-7695-2678-0
20
PageRank 
References 
Authors
1.17
32
1
Name
Order
Citations
PageRank
John Rushby12459235.69