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

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

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

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