As software grows more complex, it tends to grow more unstable. For critical applications, this unreliability is unacceptable. The technology of formal methods aims at creating high assurance software through careful forethought, using the precision of mathematics. This site presents contributions to the computer science research in this field. The ultimate goal is to transfer this technology from the laboratory into practical use, thus making formal methods into normal methods.

Interest is growing in the field of formal methods. For a good overview of the current state of formal methods, see Formal Methods: State of the Art and Future Directions, by Ed Clarke and Jeannette Wing, August 1996. It is 22 pages long and has 124 references.

The Virtual Library of Formal Methods, maintained by Jonathan Bowen, is the premiere site for general and specific information about formal methods.

The Higher Order Logic theorem prover, available at SourceForge, has been used in many of the projects described here. Some older information is available at the Virtual Library.

Major Projects

	The HOL-Omega Logic and Theorem Prover The HOL-Omega or HOLω system presents a more powerful version of the widely used HOL theorem prover. This system implements a new logic, which is an extension of the existing higher order logic of HOL4. The logic is extended to three levels, adding kinds to the existing levels of types and terms. New types include type operator variables and universal types as in System F. Impredicativity is avoided through the stratification of types by ranks according to the depth of universal types. The HOL-Omega system is a merging of HOL4, HOL2P by Völker, and major aspects of System Fω from chapter 30 of Types and Programming Languages by Pierce. Like HOL4, HOL-Omega is constructed according to the design principles of the LCF approach, for the highest degree of soundness. (Details)

	Higher Order Quotients The quotient operation is a standard feature of set theory, where a set is partitioned into subsets by an equivalence relation. We reinterpret this idea for higher order logic, where types are divided by an equivalence relation to create new types, called quotient types. We present a design and an implementation to mechanically construct quotient types as new types in the logic, and to support the automatic lifting of constants and theorems about the original types to corresponding constants and theorems about the quotient types. This design exceeds the functionality of Harrison's package, creating quotients of multiple mutually recursive types simultaneously, and supporting the equivalence of aggregate types, such as lists and pairs. Most importantly, this design supports the creation of higher order quotients, which enable the automatic lifting of theorems with quantification over functions of any higher order. (Details)

	Sunrise Sunrise is a system for proving programs correct in a feasible way. It contains a deep embedding of a small programming language within the HOL theorem prover, and provides a tool, called a verification condition generator or VCG, for the semi-automatic creation of proofs of total correctness for Sunrise programs within HOL. The VCG is itself verified as sound, and that soundness proof is contained within and checked by the HOL system. This permits the significant simplification of proofs of total correctness of Sunrise programs while retaining complete security. (Details)

Last updated