Workshop 23 November 2017 at DTU Meeting Center Building 101
Formal verification is the mathematical proof of the correctness of algorithms, protocols and computer systems. In the last decades proof assistants like Isabelle have verified a general-purpose operating system microkernel in the order of 10000 lines of C-code as well as a 300-pages textbook on programming language semantics. Journals like Archive of Formal Proofs have numerous verified articles covering both mathematics and computer science topics and many other verification projects have been successfully completed. The development and use of proof assistants and related tools, including model checking and advanced solvers, can be found in several sections at DTU Compute, for example in analysis of embedded systems, software specification and verification, security protocols, algorithms and meta-logic. The aim of the project is to strengthen the cross-sectional cooperation in formal verification research and teaching.
Program:
Thursday 23 November 2017 - DTU room 101/S14
- 13:00-14:00 Markus "Makarius" Wenzel (Sketis, Augsburg, Germany): Future Prospects of Isabelle Technology
- 14:30-15:30 Johannes Åman Pohjola (Chalmers University of Technology, Gothenburg, Sweden): How to Write End-to-End-Verified Software in CakeML
Abstract for the talk by Markus "Makarius" Wenzel: In the past 3 decades, Isabelle has made a long way from a modest LCF-style proof assistant (with copy-paste of proof scripts written in ML) to the current Isabelle/PIDE editor-environment (with its timeless and stateless processing of proof documents). In this presentation I will try to extrapolate this into the future: How far can we scale proof documents and libraries, e.g. via moving Isabelle into the "cloud"? How can we reduce system resource requirements on the client side? How can we upgrade interactive edits produced by a single author, towards versioned changesets by multiple or distributed authors? What are suitable frameworks for the next generation of Isabelle document preparation? What can we make out of Isabelle/ML as ultra-clean environment for functional programming? Etc. etc.
All are welcome. Registration is not necessary.
Organizers: Michael Reichhardt Hansen, Anne Elisabeth Haxthausen, Sebastian Alexander Mödersheim and Jørgen Villadsen (DTU Compute)
Supported by DTU Compute's Strategic Foundation