Deprecated: The each() function is deprecated. This message will be suppressed on further calls in /home/zhenxiangba/zhenxiangba.com/public_html/phproxy-improved-master/index.php on line 456 HolCheck Project Home Page
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
Develop theory and implementations
to extend fully-expansive LCF-style theorem proving to
support model checking and symbolic execution.
Implement an experimental verification platform
to test and benchmark fully-expansive model checking and its integration with theorem
proving.
Search for new synergies between theorem proving and algorithmic
verification that exploit their tight integration in a programmable platform.
Conduct substantial verification experiments using
public domain examples.