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

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

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.

Advisor: Kevin Kappelmann

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

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

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

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.

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