Isabelle/HOL- Interaction and Automation

25.10.2013 | 14:00 c.t.

Jasmin Christian Blanchette
J. Blanchette

Isabelle/HOL is a popular proof assistant based on higher-order logic. It owes its success to its ease of use and powerful automation. Much of the automation is performed by external tools: The metaprover Sledgehammer relies on automatic theorem provers for its proof search, and the counterexample generator Nitpick relies on SAT solvers. Together with the Isar structured proof format and a new asynchronous user interface, these tools have radically transformed the Isabelle user experience. Recently, Isabelle has been used to verify the seL4 microkernel, to formalize the Java and C++ memory models, and even to prove the existence of God.

Homepage J. Blanchette

Zeit & Ort

25.10.2013 | 14:00 c.t.

Takustr. 9, SR049 - Kaffee ab 13:45 Uhr im Konferenzraum 137