EPSRC Project GR/R27105/01
Fully Expansive Proof and Algorithmic Verification

Mike Gordon (Principal Investigator) University of Cambridge    Mike.Gordon@cl.cam.ac.uk
Joe Hurd (Postdoctoral Research Associate) University of Cambridge Joe.Hurd@cl.cam.ac.uk
Hasan Amjad (Postdoctoral Research Associate)   University of Cambridge Hasan.Amjad@cl.cam.ac.uk
Anthony Fox (Postdoctoral Research Associate) University of Cambridge Anthony.Fox@cl.cam.ac.uk
Konrad Slind (Collaborator) University of Utah slind@cs.utah.edu

Objectives

  1. Develop theory and implementations to extend fully-expansive LCF-style theorem proving to support model checking and symbolic execution.

  2. Implement an experimental verification platform to test and benchmark fully-expansive model checking and its integration with theorem proving.

  3. Search for new synergies between theorem proving and algorithmic verification that exploit their tight integration in a programmable platform.

  4. Conduct substantial verification experiments using public domain examples.

Results

    HolCheck fully-expansive model checker website

    Original Proposal and Final Report

MICHAEL J. C. GORDON
Professor of Computer Assisted Reasoning
The University of Cambridge Computer Laboratory
Room FE19, William Gates Building
JJ Thomson Avenue, Cambridge CB3 0FD, United Kingdom
office: +441223334627, mobile: +447774017428, fax: +441223334678