# Practical Course ‘Specification and Verification’

## Overview

 Module Bachelor-Praktikum (Practical Course for BSc students), IN0012Master-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 NipkowContact 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

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

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

Further reading: [1] [2] [3] [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.