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.

• Formal 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 reading.)
  • Related talk by Jeannette M. Wing,: Formal Methods: Past, Present, and Future,
• A. Pnueli: Verification Engineering: A Future Profession. (A. M. Turing Award Lecture) 16th ACM Symp. on Principles of Distributed Computing (PODC 1998), San Diego, August 1997
• NASA's Mission Reliable by Patrick Regan and Scott Hamilton (IEEE Computer). (See also Klaus Havelund's page at NASA.)
• How 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 co-workers.
• Some Applications of Binary Decision Diagrams
  • BDDs are the technology behind Configit Software.
  • Variants on BDDs can be used to represent the network filter of a firewall and to build a Network Access Verifier.
• Software Accident Reports
  • Therac-25 investigation
  • Ariane-5 investigation
• Formal Methods Publications
• Gerard Holzmann of SPIN fame
• Verification at IBM
• Verification at INTEL
• 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 years.
• 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 during the spring term. You are invited to check it regularly. The page is dormant in the autumn term.