Blanchette Lab

Research focus

ERC Starting Grant · 2016

Fast Interactive Verification through Strong Higher-Order Automation

Proof assistants are increasingly used to verify hardware and software and to formalize mathematics. However, despite the success stories, they remain very laborious to use. The situation has improved with the integration of first-order automatic theorem provers -- superposition provers and SMT (satisfiability modulo theories) solvers -- through middleware such as Sledgehammer for Isabelle, codeveloped by the PI; but this research has now reached the point of diminishing returns. Only so much can be done when viewing automatic provers as black boxes. To make interactive verification more cost-effective, we propose to deliver very high levels of automation to users of proof assistants by…

From the public funding record at EU CORDIS. Describes the funded project, not the reviews below.