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

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

### Automated Transport of Definitions and Theorems

Many times in formal verification, we set definitions and prove theorems about particular structures, only to discover later that our results should be applicable to similar, though definitionally different, structures. As an example, if we define addition on integers `Z` and prove it to be commutative, we would like to obtain an analogous operation on natural numbers `N` and its commutativity proof for free.

In Isabelle/HOL, the Lifting and Transfer package offers such automation for a limited fragment of structural equivalences (e.g. subtypes and quotients). Very recently, these equivalences have been generalised to a broader class (by this project’s advisor).

The aim of this project is to create automation support for this new class of equivalences in Isabelle/HOL. The project requires good functional programming skills. Acquaintance with Isabelle/ML is a plus.

### Higher-Order Unification Hints

Unification hints are a controlled mechanism to extend unification algorithms with new inference rules. They are particularly useful for interactive theorem provers. The goal of this project is to extend the existing framework of unification hints in Isabelle to full higher-order logic and prove its usefulness by means of new tactics and case studies. More information

### 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: 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.
• 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.

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

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

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 are to be published soon.

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

### Isabelle’s Metalogic

Isabelle is a generic theorem prover, that is it provides a simple metalogic in which different object-logics (e.g. HOL, FOL, ZF) can be encoded. To keep this metalogic trustworthy it is kept as minimal as possible (although some compromises must be made in the implementation for performance reasons). There exists a formalization of this meta logic in Isabelle/HOL, described in this paper. Possible topics for working with this formalization include:

#### Loose Variables

The formalization only allows working with closed terms, i.e. terms that do not contain loose variables. This can negatively affect the performance of extracted code, especially if one reasons under quantifiers, as one needs to convert the bound variables to free variables temporarily to allow working with them. For performance reasons it might be faster to allow loose variables during the derivations and only close them in a final step. The student’s task would be to develop such an alternative derivation system and prove it equivalent to the existing one.

### Theory extensions

Derivations in the formalization are performed with respect to a background theory, containing among others things like axioms, defined constants and type constructors. It should be possible to extend a theory by for example adding new axioms or defining new types. In this project the student would formalize some of those extension mechanisms and prove some basic correctness properties for them.