|
|
|
About
Founded in the 1980s, our research group initially focussed on hardware verification, and it gradually broadened to study various reasoning-related research areas.
One early achievement was the application of higher-order logic (HOL) to hardware verification. Higher-order logic is now one of the standard formalisms that is used to verify digital designs.
The group has built various tools. The HOL system was
intended primarily for hardware verification, while Isabelle
was designed around a generic reasoning mechanism in order to support a variety of logics. These two proof assistants are now two of the most
widely used systems worldwide, each with large and thriving research communities.
Isabelle has been used for both theoretical and practical
research. Among the latter kind are
type safety proofs for Java,
which were researched at T.U. Munich. At Cambridge, Isabelle has been
applied to the
verification of cryptographic protocols.
Several industrial-grade protocols, including Kerberos, have been analyzed to
a level of detail unmatched by other methods. In several cases the
analysis has uncovered design defects.
Current work on HOL concentrates on linking the theorem prover to
other programs. These include
industrial CAD and CASE tools
as well
as a variety of automatic proof procedures. A prerequisite for
combining formal verification with modern hardware design methods is
an accurate semantic understanding of hardware description languages
(HDLs). We are collaborating with Synopsys, the industry leader in
hardware synthesis, to develop a formal semantics of
Verilog HDL. Our long-term aim is to provide a flexible core proof engine that can be
embedded in other CAD/CASE systems to provide a programmable platform
for formal verification.
The Automated Reasoning Group has produced four BCS and one EAPLS Distinguished
Dissertations.
Andrew Gordon (supervised by Paulson) now works for Microsoft,
John Harrison (supervised by Gordon) works for Intel, and
Jacques Fleuriot (supervised by Paulson) is a lecturer at the University of Edinburgh.
More recently, Magnus Myreen (supervised by Gordon) and Alexey Gotsman (supervised by Gordon) have won awards.
|
