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

Mostly topics from previous semester, still subject to change!

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

Advisor: Kevin Kappelmann

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

Verification of Combintorial Algorithms

The aim is to verify a library of algorithms for listing combinatorial objects: permutations, subsets, partitions, trees, … . There is a rich literature on the subject (see below). Part of the challenge is to find elegant functional programs instead of the universally imperative algorithms given in the literature (Nijenhuis and Wilf even give Fortran programs!). You can find a first Isabelle example here

Further reading:

[1] Knuth, The Art of Computer Programming, Volume 4A, Combinatorial Algorithms

[2] Nijenhuis and Wilf. Combinatorial Algorithms

[3] Stanton and White. Constructive Combinatorics

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.

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, Simon Roßkopf, Lukas Stevens

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

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

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:

Derived instantiation rules

The implementation provides constructs allowing instantiation of term and type variables anywhere in a proof. The formalization only provides a rule for instantiation of type variables in axioms. This single rule is enough logically, but the other versions are nice to have for efficiency and convenience reasons. The student’s task would be to derive such other instantiation rules and justify their admissibility. This would also help justifying their presence in the implementation.

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.

Advisor: Simon Roßkopf

Automatic construction of proof trees for inductive predicates

Inductive definitions are a common specification tool used in Isabelle/HOL. They are characterized by a set of introduction rules and specify the least predicate closed under these rules. However, knowing that such an inductive predicate holds, does not give information on how it was derived using the introduction rules. If one is interested in this information, one can explicitly record the proof tree created by the derivation. For this one needs to create a datatype of proof trees, as well as a modified version of the predicate which additionally records their construction. The goal of this project is to develop a tool which can automatically perform this construction. Further work could also include providing automatic equivalence proofs of the old and new specifications or the automatic generation and verification of (executable) proof checkers for the generated proof trees.

Advisor: Simon Roßkopf