# Praktikum: Spezifikation und Verifikation, Winter 2018/2019

## Overview

 Title Spezifikation und Verifikation (Specification and Verification) Term Winter 2018/2019 Module Type Bachelor-Praktikum (Practical Course for BSc students, IN0012) Master-Praktikum (Practical Course for MSc students, IN2106) Preliminaries Basic knowledge of Isabelle (e.g. Functional Data Structures (IN2347), Semantics (IN2055), Interactive Software Verification (IN3350)) ECTS 10 Organisation Julian Brunner, Tobias Nipkow

## 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 Julian Brunner via email in advance 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

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

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

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

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

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

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

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

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