For a complete listing of papers to be presented, please see the advance program.
Model checking is a technique of verifying automatically that a finite state system satisfies a formal specification about its behavior over time. It has been successfully applied in numerous instances to find errors in commercial hardware designs that escaped simulation, from low-level control logic, to the cache coherence protocols of multiprocessors. Nonetheless, there is still a great deal of uncertainty as to how and whether model checking can be made into a workable tool for the engineer.
This tutorial will introduce the basics of model checking and related methods of verifying finite-state (and sometimes non-finite-state) systems -- how to formally specify and verify a design, and techiques such as abstraction, decomposition, and "symbolic methods" that are used to avoid the exponential explosion of state space size as system size increases. We will also discuss the practicalities of using model checking as a verification aid in a commercial environment, using examples from commercial design practice, how to make the best use of the particular advantages of model checking to find difficult bugs, and why "formal" verification in practice is not always as formal as you might think.
We present the principles of synchronous languages, a family of programming languages devoted to the design of reactive systems. These principles are illustrated by two examples, the data-flow language Lustre, and the imperative language Esterel. Specific features related to the compilation and the verification of synchronous programs are described, together with a survey of current trends in this domain.
Checking the properties of concurrent systems is an ever growing challenge. Along with the development of improved verification methods, some critical systems that require careful attention have become highly concurrent and intricate. Partial order reduction methods were proposed for reducing the time and memory required to automatically verify concurrent asynchronous systems. We describe partial order reduction for various logical formalisms, such as LTL, CTL and process algebras. We show how one can combine partial order reduction with other efficient model checking techniques.
General purpose mechanical theorem provers can be of use in the verification of commercial hardware and software. We briefly describe such applications of the ACL2 theorem proving system. ACL2, which stands for ``A Computational Logic for Applicative Common Lisp,'' allows the user to model computational systems with Lisp programs. Such models can often be executed efficiently, allowing the formal model to serve as a prototype of the specified part. ACL2 supports direct reasoning about such models. ACL2's rule-driven simplifier can be used to provide a ``symbolic execution'' capability. Finally, conjectures relating input and output can be formalized within the logic and either tested with examples or proved as theorems. While simple conjectures can often be proved automatically, the user is more commonly required to ``explain'' his or her design to the system by formulating key properties as lemmas and then composing those lemmas in the appropriate way. This process is not automatic but it scales arbitrarily. Furthermore, it allows the user to describe more or less arbitrary properties of the system and to move smoothly from testing to formal proof. Ongoing industrial applications of ACL2 include the formal verification of floating point algorithms and hardware for the AMD K7 microprocessor, the modeling of several microprocessors, including the Rockwell-Collins JEM1 Java Virtual Machine, and the verification of some of the year 2000 conversion rules used in software developed by EDS.
Several approaches have been developed for analyzing security protocols. These include specialized logics that formalize notions such as secrecy and belief, special-purpose automated tools for cryptographic protocol analysis, and methods that apply general theorem-proving or model-checking tools to security protocols. This talk will describe some of the challenges in applying formal methods to problems in security and summarize work on finite-state methods that use standard model-checking tools. One of the main limitations in current approaches is the abstract treatment of cryptographic primitives. Some ideas for future work in this direction will be aired.