Praktikum: Spezifikation und Verifikation, Summer 2019

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; instead contact Maximilian Haslbeck 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

Primality Testing

There are many different tests to determine if a natural number is prime. Most of these are *probabilistic* and always recognise a prime number as prime, but, with some probability, also mistakenly classify composites as primes. Some of these tests (Fermat, Miller–Rabin, Solovay–Strassen) are already formalised in Isabelle.

In this project, more primality tests are to be formalised, e.g.:

• Frobenius test (randomised)
• Lucas and Fibonacci pseudoprimes (randomised)
• Lucas–Lehmer test for Mersenne primes (deterministic)
• AKS test (deterministic)

Additionally, one could prove a better bound for the error probability in the Miller–Rabin test (1/4 instead of 1/2).

Advisor: Manuel Eberl

Analytic Number Theory

There is an ongoing effort to formalise Tom Apostol's classic textbook on Analytic Number Theory [1]. Most of the core content has already been formalised, but there are some chapters that have been left out completely, e.g.:

• Congruences
• Gauss Sums and Finite Fourier Series
• Quadratic Residues (partially)
• Number Partitions

The goal of the practical course work would be to formalise as much as possible of this material.

[1] https://www.springer.com/de/book/9780387901633

Advisor: Manuel Eberl

Group Theory

The purpose of this project is to add various missing bits of group theory to HOL-Algebra, with a particular focus on finite groups. Topics of interest include:

• Decomposition of a group into an interior direct product
• Indexed direct products
• The fundamental theorem of finite(ly generated) abelian groups
• Finite simple groups

Advisor: Manuel Eberl

Specialised Mathematical Tactics and Simprocs

The goal is to implement various additional tactics and/or simplification procedures (‘simprocs’) to simplify/expand certain mathematical terms that are difficult to simplify using simp rules, e.g.:

• proving/disproving/rewriting statements like "4/3 ∈ ℤ"
• expanding ln(n) = ∑ k_i ln(p_i) using the prime factorisation n = ∏ p_i^k
• pulling out perfect k-th powers from k-th roots, e.g. sqrt(12) = 3sqrt(2) (probably again using prime factorisation)

Some of these can be done using externally-computed certificates, e.g.:

• primality: Pratt certificate
• prime power: prime factor (with Pratt certificate) and multiplicity
• compositeness: two non-trivial factors
• non-prime-power: two non-trivial coprime factors
• prime factorisation: list of primes factors with multiplicity; Pratt certificate for each prime
• non-k-th-power-freeness: perfect k-th power factor

For the tactics (but not for the simprocs), these certificates could also be computed by an external tool (e.g. Maxima). This may require the student to write some code in Maxima as well. Otherwise, a ‘native’ certifier can be written in ML.

Proofs of concepts for some of these already exist (e.g. in the Pratt_Certificate and Bertrands_Postulate AFP entries). The goal would be to make a bigger collection of fast and robust tactics/simprocs.

Advisor: Manuel Eberl

Approximation algorithms

There are a number of simple approximation algorithms for NP-complete problems that can be shown to produce a result which is no worse than the optimal result within some factor. A typical example is the vertex cover problem which has a simple 2-approximation algorithm, i.e. the result is at most twice as bad as the optimal solution. We have verified this particular result. Here are two similar projects:

Load Balancing

Bin Packing

[CLRS] Cormen, Leiserson, Rivest and Stein. Introduction to Algorithms. 3rd edition, 2009.

[KT] Jon Kleinberg and Eva Tardos. Algorithm Design. 2006.

Advisors: Mohammad Abdulaziz, Tobias Nipkow

Parser Combinators

Parser combinators are a very common technique in each functional programmer's toolbox to parse text. They are usually implemented as functions mapping input to an optional result, together with higher-order functions for sequential composition, alternatives, repetition and others. Implement parser combinators in Isabelle and if necessary, provide setup for other Isabelle packages.

Advisor: Simon Wimmer

Newton Iteration

Newton's method is a simple method for finding approximations of roots of non-linear real functions. The goal is to develop a generic framework for this that can be instantiated for particular functions and connecting it with Isabelle's existing packages for interval arithmetic and Taylor models.

Advisor: Manuel Eberl

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), Graph Algorithms (Bellman-Ford), B-trees

Advisor: Maximilian Haslbeck, Simon Wimmer

Verification of compositional algorithms for factored transition systems

Factored transition systems succinctly represent state spaces in applications such as Artificial Intelligence (AI) planning and model checking. Many problems defined on such systems are graph theoretic problems on their state space, such as computing reachability or the diameter of the state space. A problem with naively using state-of-the-art graph theoretic algorithms is that they would require the construction of the state space, which can be exponentially bigger than the input factored system, a problem referred to as the state space explosion problem. Compositional algorithms are one approach to alleviate state space explosion, where only state spaces of abstractions are constructed. This project concerns formalising some aspects of compositional algorithms from existing AI planning or model checking literature in Isabelle. Example from the literature discussing compositional algorithms are given below.

Further Reading: [1] [2] [3]

Advisor: Mohammad Abdulaziz

Verification of an approximation algorithm for a graph theoretic problem

Many basic graph theoretic problems are either NP-hard or cannot be solved in better than polynomial time. This makes solving those problems prohibitive if not impossible for real-world graphs. Approximation algorithms circumvent that by using less resources than exact algorithms, at the expense of providing only approximate solutions. In this project the student would formally verify that 1) the approximate solutions of those algorithms meet a certain quality citerion, 2) the upper bounds on their runtimes are correct. A particularly interesting algorithm is the algorithm described below for approximating the diameter of an undirected graph due to Aingworth et al..

Further Reading: [1]

Advisor: Mohammad Abdulaziz

Program Analysis for an Assembler-Style Language

This project would formalize a number of simple program analyses on UPPAAL byte code. The goal is to establish a number of properties that are relevant for model checking (no knowledge on this part is needed). The project can start from an existing formalization of the semantics of the byte code.

Advisor: Simon Wimmer

Understanding Machine Learning

Machine learning is one of the fastest growing areas of computer science. While it seems to perform well in a wide variety of information processing tasks, its foundations are far from understood and accurate guarantees can hardly be established. The idea of this topic is to explore the principles of machine learning and formalize basic results as a background for the analysis of various techniques (i.e. Least Squares, Kernel Methods, Neural Networks). [1,2] might serve as a starting point.

Further reading: [1] [2]

Advisor: Max Haslbeck

Formalization of (extended) Bayesian Networks

Bayesian networks (BNs) are probabilistic graphical models for describing complex joint probability distributions. This project‘s goal is to formalize BNs and possibly link them up with probabilistic programs in pGCL following recent work by Batz et al. [1].

Further reading: [1]

Advisor: Max Haslbeck

Verification of Data Structures with Sharing

Many efficient data structures use sharing of data in order to save space (e.g. CoDBMs) or to improve run time (e.g. Fibonnaci Heaps). Programs manipulating mutable data structures with intrinsic sharing present a challenge for verification.

A classic approach to modular verification of data structures is separation logic. As sharing and separation seem contradictory, separation logic alone does not suffice. There are at least two recent approaches to cope with that: Ramifications [1] and flow interfaces [2]. Understanding and formalizing one of these is the goal of this project.

One direct and hot application of this work would be the verification of efficient Compact Difference Bound Matrices (CoDBMs) (Paper from APLAS 2017: [3]) used in static program analysis and model checking.

Further reading: [1], [2], [3]

Advisors: Simon Wimmer, Max Haslbeck

Techniques for AI planning under uncertainty (MDPs)

AI planning is the discipline that aims building computer programs that act rationally to achieve a certain goal, given a declarative description of the environment and the actions it has to change that environment. In many practical applications, like autonomous vehicles driving among others, it is not possible to model the exact effects of actions. Planning in such cases, known as planning under certainty, a planning problem is modelled as a (factored) Markov Decision Process (MDP), where the result of executing an action is one of many states, each with a different probability. Multiple methods to solve this kind of problems are in the AI and planning literature. In this project the student would specify and verify in Isabelle one of the basic algorithms that are used to solve planning problems that have uncertainty in them. Example algorithms are value iteration and policy iteration.

Advisors: Mohammad Abdulaziz