Practical Course ‘Specification and Verification’

Overview

Content

During the practical course students will work (guided by an advisior) on a practical problem involving the interactive theorem prover/proof assistant Isabelle. Most topics will involve using Isabelle to formalize some material, but there will also be some topics offered allowing for work on Isabelle itself and related tools. The goal of this course is providing an oppurtunity to experience actual, practical work involving proof assistants, not contrived examples from a classroom setting. Therefore previous experience with Isabelle is mandatory.

The practical course will run throughout the semester.

Application

If you want to participate in the practical course, please send an email to Katharina Heidler (before the start of the matching). In it, please list your prior experience with Isabelle. A formal letter of application or similar (beyond the mentionesd email) is not necessary.

Topics

Verification of Convex Hull Algorithms

Convex hull algorithms are important to solve computational geometry problems such as collision detection. The aim is to complete an existing formalisation of a convex hull algorithm called the Graham’s scan. After that, we would continue formalising other convex hull algorithms such as the Gift Wrapping Algorithm or Chan’s algorithm.

Advisor: Lukas Stevens

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

Advisor: Lukas Stevens

Earley’s Algorithm

There is already a proof of Earley’s parsing algorithm in Isabelle. Recently I have started on a much simplified “second generation” proof. The aim of this project is to complete this proof and extend it with a running time analysis.

Advisor: Tobias Nipkow

Running Time Analysis of Huffman’s Algorithm

Huffman’s algorithm has long been verified in Isabelle. The aim of the project is to

1. Prove that the verified algorithm has quadratic time complexity.
2. Modify the algorithm for the case of a sorted input list.
3. Verify correctness and linear-time complexity

Relevant literature: https://webspace.science.uu.nl/~leeuw112/huffman.pdf

Advisor: Tobias Nipkow

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.

Possible reductions include:

• Steiner-tree problem
• Job sequencing problem
• 3-dimensional matching
• Feedback arc problem
• an NP hard problem of your choice that is not formalized yet

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.
• Applying this refinement approach to concrete programs
• Proving running time upper bounds on an already verified reduction from While-programs to SAT.

Additionally a student could work on connecting the While-language to Turing machines or automating certain steps in the refinement.

Further reading: [1]

Advisor: Mohammad Abdulaziz, Lukas Stevens, Kevin Kappelmann

Certificate Checker for Probabilistic Model Checking

This project aims to extend a certificate checker for probabilistic model checking [1,2] to support a more expressive specification language.

Model Checking [3] is a formal method to determine whether a model of a system conforms to a specification. The probabilistic variant works on system models that are given as Markov Decision Processes (MDPs). Due to the complexity of probabilistic model checkers, a formal verification of an implementation is currently out of reach. Certificate checking offers a viable alternative: the model checker MoChiBA [4] can be extended to produce certificates that may then be used to verify its results. Checking these certificates is considerably less complex than the original problem, thus a certificate checker can be implemented and verified using Isabelle/HOL with reasonable effort.

Currently the certificate checker only supports LTL co-safety properties. The goal of the project is to extend it to full LTL [5]. Experience with model checking and MDPs can be helpful but not a prerequisite.

[1] Probabilistic Model Checking: Advances and Applications [2] [3] [4] [5]

Advisor: Maximilian Schäffeler

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: Maximilian Schäffeler

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: Maximilian Schäffeler, Tobias Nipkow

Convolution theorem for DFT/FFT and NTT/FNTT

The Discrete Fourier Transform (DFT) and Fast Fourier Transform (FFT) are used in signal theory to represent periodic functions and discrete signals. A very important theorem for calculating with signals is the convolution theorem, which states that a convolution of two sequences can be obtained as the inverse transform of the product of the individual transforms, ie. DFT(x*y) = DFT(x)DFT(y).

For finite fields, the analogue to the DFT is the number theoretic transform (NTT) with a fast variant FNTT. An analogue to the convolution theorem can be used for fast multiplication in cryptography.

The goal of this project is to formalize convolutions of discrete signals, properties thereof and the convolution theorem for DFT and FFT. The ultimate motive is to get the convolution theorem for the NTT and FNTT as well.

Formalizations of the FFT can be found here

Formalizations of the NTT can be found here.

Advisor: Katharina Heidler

Correctness of Crypto Systems

How can we ensure that cryptographic algorithms are really as secure as we hope they will be? Verification of cryptographic algorithms give insight in how cryptosystems work, one can show their correctness and even state security properties against certain attacks.

Your task: Define a crypto system (eg Cramer-Shoup, Paillier), show its correctness and analyze its security.

Advisor: Katharina Heidler

Galois fields and Number fields

Galois fields and number fields are an interesting topic in algebra. Your goal is to use existing formalizations of galois fields to prove small lemmas (tbd) or to formalize number fields and show essential properties.

Warning: Algebra knowledge essential!

Advisor: Manuel Eber, Katharina Heidler