Practical Course ‘Specification and Verification’

Overview

Module	Bachelor-Praktikum (Practical Course for BSc students), IN0012 Master-Praktikum (Practical Course for MSc students, IN2106
Prerequisites	Basic knowledge of Isabelle (e.g. through ‘Functional Data Structures’, IN2347, ‘Semantics’, IN2055)
Language	German, English
Organisation	Simon Roßkopf, Prof. Tobias Nipkow Contact Simon Roßkopf for all course matters, or your advisor (once you have been assigned one).

Content

Participants will work on a project by themselves using the interactive theorem prover Isabelle. The practical course will run throughout the semester.

Application

The application will be through the Matching Platform. There will be a kick-off meeting Friday January 29 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

Topics

Topics still subject to change!

Verification of an Interesting Algorithm or Data Structure

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), Hopcroft’s Minimization Algorithm, B-trees

Advisor: Simon Roßkopf, Lukas Stevens

NP Zoo

Polynomial Reductions

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).

Cook-Levin theorem

The Cook-Levin theorem is a fundamental result in Computational Complexity Theory. The student would join an ongoing effort to formalise the Cook-Levin theorem. This will involve the following steps:

Extending the existing refinement approaches in Isabelle/HOL to refine programs specified in Isabelle/HOL’s functional programming language to an already formalised simple While-language.
Extending an existing formalisation of a While-language to include the notion of a cost of computation steps, and thus a notion of running time.
Proving running time upper bounds on an already verified reduction from While-programs to SAT.

Approximation algorithms

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.
An example project is to 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

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

Advisor: Tobias Nipkow

Verification of an approximation algorithm for a graph theoretic problem

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..

Verified Translations of AI Planning Problems:

AI planning is a discipline aiming to build computer programs that act rationally to achieve a certain goal. One established way of solving planning problems is via translating them to SAT [1]. In this project you would extend a recent verification [2] of the forall-step SAT encoding of classical AI planning. Possible directions: translating first-order logic planning problems to propositional planning problems, adding symmetry breaking formulae [3], adding formulae that represent invariants in the state space [4].

Interval Analysis Based Verification of Neural Networks:

Deep neural networks are currently in heavy use in many applications, some of which are safety critical. One problem with them is that there are not theoretical foundations, let alone formal guarantees, on machine learning algorithms that train these deep neural networks. One approach to resolve that situation is by verifying that the trained neural networks themselves satisfy certain properties, e.g. that the outputs remain within certain bounds. One successful approach to perform this is via interval analysis [1,2]. In this project you would formally verify an interval analysis based method for verifying neural networks.

Graph Theory and Algorithms:

There is an ongoing effort to build a unified library of graph theory and algorithms in Isabelle 1. In this project you would participate in the development of this graph library by either porting results from other theorem provers, or by formalising new results into that library. Some interesting directions would be: algorithms for computing strongly connected components in a digraph, connecting graph theoretic concepts, like matchings and weighted matchings, to linear programming. You can also suggest an interesting graph theoretic concept or algorithm, if you have one.