What is this Theory Good for?
This is the typical question we get from the students, and some of
our colleagues. Rather than answering it ourselves, we refer you to
the words of some of our most distinguished colleagues. You are
strongly encouraged to browse through the following papers and links
to relevant material. After reading some of it, we hope that you will
agree with us that this theory is not only beautiful, but also
useful and usable.
Methods: State of the Art and Future Directions, Edmund
M. Clarke and Jeannette M. Wing, report by the Working Group on Formal
Methods for the ACM Workshop on Strategic Directions in Computing Research,
ACM Computing Surveys, vol. 28, no. 4, December 1996,
pp. 626-643. Also CMU-CS-96-178. (This is strongly recommended
Verification Engineering: A Future Profession. (A. M. Turing Award
Lecture) 16th ACM Symp. on Principles of Distributed Computing (PODC 1998),
San Diego, August 1997
Mission Reliable by Patrick Regan and Scott Hamilton (IEEE
Computer). (See also Klaus
Havelund's page at NASA.)
can I be sure that my DVD player understands my TV? Wan Fokking, Izak
van Langevelde, Bas Luttik and Yaroslav Usenko, ERCIM News.
- Dawson Engler's page
has lots of very interesting papers on the use of software model
checking in analyzing file systems, large network protocol
implementations and more. He is also a founder of the company Coverity that offers the
technology for source code analysis developed by Englar and his
- Some Applications of Binary Decision Diagrams
- Software Accident Reports
- Gerard Holzmann of SPIN fame
CMU Model Checking home
page, where you can find information on some of the applications
of model checking carried out by E.M. Clarke and his group over the
UPPAAL web page, where you can read
about the examples that have been verified using this tool for real-time
systems. (These include Bang & Olufsen Audio/Video Protocol, a Gearbox
Controller and a Lip Synchronization Algorithm.)
The Risk Forum
This page will be actively modified over the next couple of
months. You are invited to check it regularly.
Luca Aceto, School
of Computer Science, Reykjavík University.
Last modified: 2 October 2008.