Research projects related to proof engineering.
DeepSpec is an Expedition in Computing project funded by the National Science Foundation.
The DeepSpec consortium will develop new science, technology, and tools--for specifying what programs should do, for building programs that conform to those specifications, and for verifying that programs do behave exactly as specified.
REMS (Rigorous Engineering for Mainstream Systems), is a 6-year EPSRC-funded Programme Grant (2013-2019, £5.6M, Cambridge, Imperial, and Edinburgh) to explore how we can use rigorous mathematics to improve engineering practice for mainstream computer systems, to make them more robust and secure: broadly, to "create the intellectual and software tools to apply semantics and verification at the heart of mainstream system engineering".
http://www.cl.cam.ac.uk/~pes20/rems
Funded by the EPSRC (January 2004 to January 2007).
Interactive proof tools support rich, expressive formalisms. The user can express a complex model of, say, a CPU design, and develop its formal theory. Unfortunately, interactive proof construction is tedious. At the opposite extreme, resolution systems are automatic and powerful. However, they are restricted to first-order logic with equality. Can we combine the advantages of these two technologies?
This proposal aims to combine interactive proof tools with a leading resolution theorem prover. It also abandons the traditional mode of interaction, where the proof tool does nothing until the user types a command. Background processes should try to prove the outstanding subgoals. Better automation could make formal verification affordable.