Practical Course ‘Specification and Verification’

Overview

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 no kick-off meeting; if you have questions or want to participate 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.

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.

Further reading: [1]

Advisor: Mohammad Abdulaziz, Simon Roßkopf, Lukas Stevens

Real-time double-ended queues

Hood and Melville showed how to implement functionally a queue with constant time enqueue and dequeue operations. A verification is described here and was covered in the FDS course 2021. Chuang and Goldberg generalised the work of Hood and Melville to double-ended queues. These are queues where you can enqueue and dequeue at both ends. The aim of this project is to verify the implementation by Chuang and Goldberg.

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

Further Reading: [1]

Advisor: Mohammad Abdulaziz, Lukas Stevens

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]

Advisor: Mohammad Abdulaziz

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.

Further reading: [1] [2]

Advisor: Mohammad Abdulaziz, Tobias Nipkow

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.

Further reading: [1]

Advisor: Mohammad Abdulaziz

Number Theoretic Transform

The number theoretic transform (NTT) is an extension of the classic discrete Fourier transform (DFT) to finite fields. Similar to the DFT, it is a convolution to quickly compute a multiplication eg. of large integers or large degree polynomials. This has applications in computer arithmetic and cryptography, especially in lattice-based cryptography. The goal of this project would be to define the number theoretic transform and verify its correctness (eg. along these lines).

Advisor: Katharina Kreuzer

Algebraic lattices

The goal of this project is to formalise some basic concepts from algebraic lattice theory. In algebra, lattices are discrete subgroups of \(\mathbb{R}^n\), for example \(\mathbb{Z}^n\) is a lattice (see for example). The application of algebraic lattices is huge: from chemistry where they describe the underlying structures of crystals to wallpaper groups and number theory in mathematics and lattice-based cryptography in computer science. The latter is of special interest, since the most known quantum-resistant cryptographic schemes rely on lattices. Example topics include the formalisation of lattices, their bases, transition between bases, the fundamental domain, Minkowski’s theorem or others. Another interesting topic is to formalise the basic lattice problems, such as the shortest vector problem (SVP), the closest vector problem (CVP) or similar

Advisor: Katharina Kreuzer

Unification Hints

Unification hints are a controlled mechanism to extend unification procedures with new inference rules: if the standard unification procedure fails, the set of collected unification hints is matched against the goal for an appropriate alternative.

This mechanism is particularly useful for interactive theorem provers such as Isabelle, where users can provide such hints to guide the unifier to find solutions for seemingly trivial equalities which might not hold by pure unification but by using special domain knowledge. Beyond extending the strength of the unifier, unification hints can be used to build mechanisms such as type classes and reification tactics.

The goal of this project is to extend the existing implementation of unification hints in Isabelle. Currently, the first-order unifier and higher-order pattern matcher are able to work with unification hints. The first step of the project is to extend the full higher-order unification procedure to work with unification hints as well.

The second step of the project is to prove the usefulness of unification hints in the Isabelle/HOL environment. First, a non-trivial reification tactic should be implemented. Finally, a mechanism to integrate type classes in the user space of Isabelle (that is outside the Isabelle kernel) should be designed and implemented.

The project requires good functional programming experience as the code must be written in Isabelle/ML as well as basic experience with Isabelle/HOL.

Advisor: Kevin Kappelmann