ERC Starting Grant · 2016
Strong Modular proof Assistance: Reasoning across Theories
Formal proof technology delivers an unparalleled level of certainty and security. Nevertheless, applying proof assistants to the verification of complex theories and designs is still extremely laborious. High profile certification projects, such as seL4, CompCert, and Flyspeck require tens of person-years. We recently demonstrated that this effort can be significantly reduced by combining reasoning and learning in so called hammer systems: 40% of the Flyspeck, HOL4, Isabelle/HOL, and Mizar top-level lemmas can be proved automatically. Today's early generation of hammers consists of individual systems limited to very few proof assistants. The accessible knowledge repositories are isolated,…
From the public funding record at EU CORDIS. Describes the funded project, not the reviews below.