



Trustworthy Tools


Home  About Us  Projects  HOLOmega  Publications  Dissertation  Divine Support


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 HOLOmega Logic and Theorem Prover
The HOLOmega 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 HOLOmega 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, HOLOmega 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.


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 semiautomatic
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.





