| Title | Spezifikation und Verifikation (Specification and Verification) |
| Term | Winter 2017/18 |
| Module type | Master-Praktikum (Practical Course for MSc students, IN2106) |
| Preliminaries | Basic knowledge of Isabelle (e.g. Functional Data Structures (IN2347), Semantics (IN2055), Interactive Software Verification (IN3350)) |
| ECTS | 10 |
| Organisation | Mohammad Abdulaziz, Manuel Eberl, Simon Wimmer, Tobias Nipkow |
Participants will work on a project by themselves using the interactive theorem prover Isabelle. The practical course will run throughout the semester.
The application will be through the Matching Platform. There will be no kick-off meeting; instead contact Manuel Eberl via email in advance and indicate what prior experience you have with Isabelle (e.g. through one of the above-mentioned lectures) and possibly what particular topics you are interested in.
Note that prior experience with Isabelle is mandatory.
Parser combinators are a very common technique in each functional programmer's toolbox to parse text. They are usually implemented as functions mapping input to an optional result, together with higher-order functions for sequential composition, alternatives, repetition and others. Implement parser combinators in Isabelle and if necessary, provide setup for other Isabelle packages.
Advisor: Lars Hupel
Implement a generic branch-and-bound method with a focus on global optimization problems (like e.g, [Narkawicz & Muñoz]). Unify existing approaches for numerical range bounding (interval arithmetic, affine arithmetic, Taylor models) and use them as instantiations of the generic method.
Advisor: Fabian Immler
Newton's method is a simple method for finding approximations of roots of non-linear real functions. The goal is to develop a generic framework for this that can be instantiated for particular functions and connecting it with Isabelle's existing packages for interval arithmetic and Taylor models.
Advisor: Fabian Immler
You are welcome to propose an algorithm or data structure and discuss the realizability with your advisor. Some examples of algorithms and data structures that were verified in past lab courses: Finger Trees, Skew Binomial Queues, Dijkstra's Algorithm, Conversion Between Regular Expressions and Finite Automata.
Ideas: String Search Algorithms (Boyer-Moore, Knuth-Morris-Pratt), Graph Algorithms (A*, Bellman-Ford, Kruskal)
Advisor: Peter Lammich
Formalize and verify the construction of the optimal binary search tree given probabilities for the keys in the tree. This is a dynamic programming problem that can be solved in cubic time; Knuth improved the algorithm such that it runs in quadratic time.
Further Reading: https://en.wikipedia.org/wiki/Optimal_binary_search_tree
Advisor: Tobias Nipkow
Isabelle's ‘approximation’ method uses interval arithmetic and various numeric techniques in order to prove estimates for real-valued expressions such as ‘arctan(2 ln(3))’ etc. It would be interesting to use this to also approximate definite integrals like ∫[0;1] x-x dx or possibly even unbounded integrals like the one appearing in the definition of the Gamma function.
There already exists some similar work in the theorem prover Coq that could be used as a basis.
Advisor: Manuel Eberl
Factored transition systems succinctly represent state spaces in applications such as Artificial Intelligence (AI) planning and model checking. Many problems defined on such systems are graph theoretic problems on their state space, such as computing reachability or the diameter of the state space. A problem with naively using state-of-the-art graph theoretic algorithms is that they would require the construction of the state space, which can be exponentially bigger than the input factored system, a problem referred to as the state space explosion problem. Compositional algorithms are one approach to alleviate state space explosion, where only state spaces of abstractions are constructed. This project concerns formalising some aspects of compositional algorithms from existing AI planning or model checking literature in Isabelle. Example from the literature discussing compositional algorithms are given below.
Advisor: Mohammad Abdulaziz
This project would formalize a number of simple program analyses on UPPAAL byte code. The goal is to establish a number of properties that are relevant for model checking (no knowledge on this part is needed). The project can start from an existing formalization of the semantics of the byte code. Ideally, the project would be carried out as a summer project, finishing in early October.
Advisor: Simon Wimmer
Starting from the experience from another student project, this project would study one or more of a number of aspects in the area of dynamic programming:
Advisor: Simon Wimmer
Auto2 is a recently developed proof automation tool in Isabelle. It is intended to emulate human reasoning when searching for a proof, and contains a mixture of ideas from existing approaches to automation: tactics and the use of automated theorem provers. It has been successfully applied to several case studies in mathematics and computer science, including the formalization of mathematics from the foundations up to the definition of the fundamental group (using set theory), and the verification of functional and imperative data structures (using higher-order logic).
The course consists of learning how to use the auto2 prover, and applying it in a small formalization project. The suggested topic is elementary number theory, based on existing formalization of basic mathematics in set theory. Through this project, the student can learn about some recent ideas on proof automation, and potentially contribute to the development of the still evolving auto2 prover.
Advisor: Bohua Zhan