Software verification is a problem with economic implications on a scale of billions of dollars. This prevalence of software flaws is exacerbated by the increasingly ubiquitous and connected environment in which software executes. Formal verification uses mathematical techniques to guarantee the correctness of a software program (or hardware design) for the specified behavior. Formal-verification tools have enjoyed a substantial and growing use over the last few years, showing ability to discover very subtle flaws.
Real advances have recently been made. For example:
* NASA is developing mathematics-based tools that verify the correctness of aerospace software.
* Intel and AMD use both human-guided and automatic proof engines to verify the correctness of their mathematics software libraries.
* Numerous companies and research groups have released powerful tools that verify the correctness of specialized software domains, such as railway switching software or device drivers.
The impact of such projects has encouraged computer scientists to search deeper into mathematical logic for techniques that will work for larger and more complex software. At the same time, researchers have been trying to come up with a theoretical understanding for the success of certain algorithms that have been particularly effective in practice. To extend the applicability of model checking, it is crucial to recognize that numerous problems in model checking are specific instances of constraint satisfaction, a canonical form of which is the satisfiability problem of propositional logic. Indeed, satisfiability is also a dramatic example of the symbiotic relationship between theory and practice in this field. Throughout the 1990s, applied researchers made dramatic improvements in the performance and scalability of satisfiability solvers, enabling the use of satisfiability as a viable alternative in increasingly non-trivial contexts. This, in turn, motivated renewed theoretical interest in propositional satisfiability and a plethora of new results. Satisfiability-based program verification has emerged as a rapidly advancing area.
For more details: http://research.microsoft.com/~bycook/sspv06/
(University of California, Santa Cruz (UC Santa Cruz))
Byron Cook (Microsoft Research)
Moshe Vardi (Rice University)