Title | Spezifikation und Verifikation (Specification and Verification) |

Term | Winter 2020/2021 |

Module Type |
Bachelor-Praktikum (Practical Course for BSc students, IN0012) 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 | Simon Roßkopf, 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 a **kick-off meeting** **Monday July 13 at 15:00 ** in this BBB room; explaining some details about the Praktikum; in any case contact Simon Roßkopf via email in advance (i.e. before the matching starts) 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**.

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: Knuth-Morris-Pratt, A*, Kruskal, Finger Trees, Skew Binomial Queues, Dijkstra's Algorithm, Conversion Between Regular Expressions and Finite Automata.

Ideas: String Search Algorithms (Boyer-Moore), Graph Algorithms (Bellman-Ford), B-trees

Advisor: Simon Roßkopf, Lukas Stevens

The book "Concrete Semantics" [1] presents a simple abstract interpretation framework for the imperative toy language IMP. The most sophisticated abstract interpretation technique it provides is the interval domain. This domain suffers from a well-known shortcoming: dependencies between variables cannot be tracked. The goal of this project is to extend this abstract interpretation framework to some popular domains that can track variable inter-dependencies based on difference constraints. Concretely, this work would consist of the following steps:

- Extend the abstract interpretation interface such that variable inter-dependencies can be tracked. The classic reference is Cousot and Cousot [2].
- Instantiate the framework for the DBM domain [3]. DBMs have already been formalized in Isabelle/HOL [6] but some additional operations would have to be added.
- Instantiate the framework for the octagon domain [4]. This can be based on the formalization of the DBM domain.
- Possible extensions: polyhedra domain [5], certification of abstract interpretation results from external tools.

This project should be a perfect fit for any students that have just finished the Semantics course (or read the book)!

References:

[1] Nipkow, T., Gerwin, K.: Concrete Semantics

[2] Cousot, P., Cousot, R.: Abstract interpretation: A unified lattice model for static analysis of programs by construction or approximation of fixpoints

[3] Antoine Miné: A New Numerical Abstract Domain Based on Difference-Bound Matrices

[4] Antoine Miné: The Octagon Abstract Domain

[5] Cousot, P., Halbwachs, N.: Automatic Discovery of Linear Restraints Among Variables of a Program

[6] Simon Wimmer: Timed Automata

Advisor: Simon Wimmer, Simon Roßkopf

The Garsia-Wachs algorithm constructs an optimal binary search tree in time O(n log n) given fixed access frequencies for the items in the tree. The proof is intricate and has never been verified formally. There is a nicely abstract proof by Kingston and a recent derivation of the algorithm by Bird (Advisor has a copy). This is a challenging but also rewarding verification.

Advior: Tobias Nipkow

This topic aims to formalize some parts of the zoo of NP-complete problems and the polynomial-time reductions between them. See Figure 6 of [1] for an overview of a plethora of such problems and their interrelations. This could include one or more of the following subtasks:

- Formalizing classic Karp and Cook reductions between NP-hard problems in an abstract language.
- Complexity-preserving synthesis of WHILE programs from such abstract algorithms.
- Translation from WHILE-programs to Turing Machines (and vice versa).

Further reading: [1]

Advisor: Simon Roßkopf, Lukas Stevens

There are a number of simple approximation algorithms for NP-complete problems that can be shown to produce a result which is no worse than the optimal result within some factor. A typical example is the vertex cover problem which has a simple 2-approximation algorithm, i.e. the result is at most twice as bad as the optimal solution. We have verified this particular result. Here are two similar projects:

A description of the problem and the greedy approximation algorithm can be found here. Formalize and verify the center selection algorithm in [KT, Section 11.2], i.e. prove Theorem (11.8).

A description of the problem and the greedy approximation algorithm can be found here. Formalize and verify the Set Cover algorithm in [KT, Section 11.3], i.e. prove Theorem (11.11).

Reference: [KT] Jon Kleinberg and Eva Tardos. Algorithm Design. 2006.

Advisors: Mohammad Abdulaziz, Tobias Nipkow, Lukas Stevens

Edmond's blossom shrinking algorithm is one of the fundamental algorithms in combinatorial optimisation. It was recently verified in Isabelle/HOL. In this project the student will have the task of porting Edmond's algorithm to the Isabelle Refinement Framework and, if successful, show worst-case running time bounds on the algorithm.

Advisor: Mohammad Abdulaziz

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

Many basic graph theoretic problems are either NP-hard or cannot be solved in better than polynomial time. This makes solving those problems prohibitive if not impossible for real-world graphs. Approximation algorithms circumvent that by using less resources than exact algorithms, at the expense of providing only approximate solutions. In this project the student would formally verify that 1) the approximate solutions of those algorithms meet a certain quality citerion, 2) the upper bounds on their runtimes are correct. A particularly interesting algorithm is the algorithm described below for approximating the diameter of an undirected graph due to Aingworth et al..

Further Reading: [1]

Advisor: Mohammad Abdulaziz, Lukas Stevens

AI planning is the discipline that aims building computer programs that act rationally to achieve a certain goal, given a declarative description of the environment and the actions it has to change that environment. In many practical applications, like autonomous vehicles driving among others, it is not possible to model the exact effects of actions. Planning in such cases, known as planning under certainty, a planning problem is modelled as a (factored) Markov Decision Process (MDP), where the result of executing an action is one of many states, each with a different probability. Multiple methods to solve this kind of problems are in the AI and planning literature. In this project the student would specify and verify in Isabelle one of the basic algorithms that are used to solve planning problems that have uncertainty in them. Example algorithms are value iteration and policy iteration.

Advisors: Mohammad Abdulaziz