Sixth International Conference on
   Formal Engineering Methods (ICFEM)
   Nov 8-12, 2004, Seattle

On the Adoption of Formal Methods by Industry: The ACL2 Experience

J Strother Moore
Department of Computer Sciences
University of Texas at Austin 

Formal methods is gradually being adopted by industry. The complexity of industrial designs -- often seen as an impediment to the use of formal methods -- is actually one of the main arguments in favor of mechanized formal methods. No other tool is as good as mechanized mathematical modeling at capturing the complexity and giving the human designers the facilities for explaining the reasons their designs are correct and controlling the revelation of the relevant complexity. In this talk I will describe the ongoing Boyer-Moore project, which for three decades has been concerned with the use of mechanized theorem proving to verify properties of hardware and software. The current theorem prover, ACL2, is the product of Matt Kaufmann and the speaker, and has been used to verify

•  the correspondence of a bit- and cycle-accurate micro-architectural model of a Motorola digital signal processor and the microcode engine it implemented,
• the verification of some microcode for that Motorola dsp,
• the correctness, with respect to the IEEE 754 floating point standard, of the AMD K5's FDIV and FSQRT instructions,
• the correctness of the RTL implementing the elementary floating point operations on the AMD Athlon and other AMD fpu designs,
•  process isolation properties of the microcode implementing a separation kernel on the Rockwell AAMP7 processor, and
• properties of JVM bytecode and of the JVM itself, including ongoing work on the bytecode verifier and class loader.

I will sketch how we got to this state of affairs and some of the key reasons ACL2 has been adopted for these and other projects.

When Can Formal Methods Make a Real Difference?

Peter G. Neumann
Principal Scientist
SRI International Computer Science Lab

ICFEM 2004 Banquet Talk

This talk will consider a few cases from the ACM Risks Forum archives (http://www.risks.org) for which the sensible use of formal methods could have made a decisive difference in avoiding serious consequences -- with respect to requirements, specifications, human interfaces, implementation, and even operation, typically in systems that were supposedly safe, reliable, or secure. This will provide a view to the future in terms of things we can learn about the past.

Engineering Quality Software

Amitabh Srivastava
Corporate Vice-President, Core Windows
Microsoft Corporation

Producing high performing, reliable and secure software is a challenging problem in the software industry. An important element in achieving this goal lies in the automation of the software development process, which currently is primarily manual. However, progress in program specification, verification, and testing is more rapid today than ever before. At Microsoft, we have developed innovative techniques to address some of these challenges. Our techniques scale to meet the requirements of real production environments and span the whole development process from software architecture to sustained engineering. These methodologies are making huge impact in the development of Windows and other products at Microsoft. This talk focuses on the challenges in software development, describes our progress and experience, and outlines remaining problems.

A CLP Approach to Modelling Systems

Joxan Jaffar
Professor and Dean
School of Computing
National University of Singapore

We present a formal method for modelling the operational behavior of various kinds of systems of concurrent processes. A first objective is that the method be broadly applicable. A system can be described in terms of its processes written in a traditional syntax-based manner, or in some non-traditional form such as a timed automaton. The number of processes may be fixed, or parameterized, or, because of dynamic process creation, unbounded. The communication and synchronization between processes may be synchronous or not, and via shared variables or some form of channels. We may have a traditional interleaving of processes, or use a specific scheduling strategy. The observables modelled should not be restricted to just the values of the program variables, but possibly other attributes of the system such as its registers and cache, its clock and battery values, etc. An example application area which touches upon these characteristics is that of determining worst-case execution time.

We choose to model a generic system S in the form of a CLP program P. The model-theoretic semantics of P shall characterize the "collecting" semantics of S, that is, those states that are observable. The proof-theoretic semantics of P, on the other hand, further characterize the "trace" semantics of S. An advantage of this CLP approach is that intricate details of the system can be captured in a familiar logical framework.

We then present a specification language for an extensive class of system behaviors. In addition to the traditional safety and liveness properties which specify the universality or eventuality of certain predicates on states, we introduce the notions of relative safety and relative progress. The former extends traditional safety assertions to accommodate non-behavioral properties such as symmetry, serializability and commutativity between processes. The latter provides for specifying progress properties. Our specification method is not just for stating the property of interest, but also for the assertion of properties held at various program points.

Finally, we present an inference method, based upon a notion of inductive tabling, for proving an assertion A. This method can use assertions that have already been proven, use the assertion A itself, in a manner prescribed by induction principles, and dynamically generate new assertions. All these properties are shown to be useful in preventing redundant computations, which then can lead to efficient proofs. Our proof method thus combines the search characteristic of model-checking and abstract interpretation, and methods of inductive assertions.

We demonstrate a prototype implementation on some benchmark examples.

Amitabh Srivastava
Corporate Vice President Windows Core Operating System Development
Microsoft Corporation

Amitabh Srivastava is a Corporate Vice President of the Windows Core Operating System Development and a Microsoft Distinguished Engineer. Srivastava is responsible for the development of core operating system components like the kernel, operating system architecture, definition of development processes, and development of advanced tools to automate the development processes.

Srivastava joined Microsoft in 1997 as a Senior Researcher and led the Advanced Development Tools group in Microsoft Research that investigated new techniques to build innovative tools and technologies to improve performance and quality of Microsoft software. His vision and energy led to the creation of the Programmer Productivity Research Center (PPRC) in March 1999, which he has led since its inception. Srivastava's PPRC group has produced several tools and technologies that are critical to Microsoft product groups. In January 2001, he became one of a select few to be named a Distinguished Engineer. As part of the continued focus on engineering excellence, Srivastava joined a strong Windows team in December 2003 as Vice President of the Core OS development to redesign how Windows architects and engineers products.

Peter G. Neumann

(Neumann@CSL.sri.com) has doctorates from Harvard and Darmstadt. After 10 years at Bell Labs in Murray Hill, New Jersey, in the 1960s, during which he was heavily involved in the Multics development jointly with MIT and Honeywell, he has been in SRI's Computer Science Lab since September 1971. He is concerned with computer systems and networks, security, reliability, survivability, safety, and many risks-related issues such as voting-system integrity, crypto policy, social implications, and human needs including privacy. He moderates the ACM Risks Forum, edits CACM's monthly Inside Risks column, chairs the ACM Committee on Computers and Public Policy, co-chairs the ACM Advisory Committee on Security and Privacy, and chairs the National Committee for Voting Integrity (http://www.epic.org/privacy/voting).

He co-founded People For Internet Responsibility (PFIR, http://www.PFIR.org). His book, Computer-Related Risks, is in its fifth printing. He is a Fellow of the ACM, IEEE, and AAAS. He is a member of the U.S. General Accounting Office Executive Council on Information Management and Technology, and the California Office of Privacy Protection Advisory Council. He has taught at Stanford, U.C. Berkeley, and Maryland. For further background, see his Web site (http://www.csl.sri.com/neumann). 

J Strother Moore

J Strother Moore holds the Admiral B.R. Inman Centennial Chair in Computing Theory at the University of Texas at Austin. He is also chair of the department. He is the author of many books and papers on automated theorem proving and mechanical verification of computing systems. Along with Boyer he is a co-author of the Boyer-Moore theorem prover and the Boyer-Moore fast string searching algorithm. With Matt Kaufmann he is the co-author of the ACL2 theorem prover. Moore got his PhD from the University of Edinburgh in 1973 and his BS from MIT in 1970. Moore was a founder of Computational Logic, Inc., and served as its chief scientist for ten years. He and Bob Boyer were awarded the 1991 Current Prize in Automatic Theorem Proving by the American Mathematical Society. In 1999 they were awarded the Herbrand Award for their work in automatic theorem proving. Moore is a Fellow of the American Association for Artificial Intelligence.

Joxan Jaffar

Joxan Jaffar received his B.Sc.(Hons, 1st class) and M.Sc. from Melbourne University in 1979 and 1981, and his Ph.D. from Monash University in 1985. From 1982 through 1986, he was a Lecturer in Monash, and from 1986 through 1995, he was a Research Staff Member and Project Leader in the IBM. T.J. Watson Research Center, Yorktown Heights, New York. He joined NUS in 1995, where he is now a Professor and Dean of the School of Computing. His research interests are in programming languages and applications, with emphasis on the logic and constraint programming paradigms. Amongst his main contributions are the principles of constraint logic programming, and the widely-used CLP(R) system. His current interests center around program analysis and verification, and the design of concurrent programming languages. He is an Area Editor for the ACM Transactions on Programming Languages and Systems, a former editor of the Journal of Logic Programming, the Constraints Editor for the journal Theory and Practice of Logic Programming (CUP), and an editor for the electronic Journal of Functional and Logic Programming (MIT Press) since 1994. He holds an IBM Outstanding Innovation Award, and served on the program committee of and published in numerous international conferences on programming languages and theoretical computer science such as ICLP, ILPS, POPL, LICS, RTA, ICCL, CP, ICSE, IJCAI.