**Supervisors:** Viorel Preoteasa and Stavros Tripakis

**Contact information**: lastname.firstname@aalto.fi

**Job description**:

Invariant based programming is a technique for constructing correct programs. In invariant based programs the invariants (properties that the program should satisfy) are introduced first, and then the program transitions are introduced such that they preserve the invariants. For example a program that searches for an element x in some array a(0)...a(n-1) starts from a situation where some invariant (the precondition) is true, and if the element x is found then it ends in a situation (a post-condition) where i is the index in the array such that a(i) = x. If the element is not found in the array, then the program ends in a situation in which for all indexes i between 0 and n-1, x is not equal to a(i) . To be able to use invariant based programming in practice we need tool support. The purpose of this project is to build support for invariant based programs in Isabelle/HOL theorem prover. With this tool it will be possible to construct programs, verify (using Isabelle) that the transitions preserve the invariants, and generate executable code (SML, Scala, ...). The work on this project would involve SML (functional) programming and small theory development, as well as becoming familiar with the Isabelle theorem prover. Experience in programming is required for this project.

**Additional information**:
Verification and code
generation for invariant diagrams in Isabelle. Journal of
Logical and Algebraic Methods in Programming

**Supervisor**: Stavros Tripakis and Viorel Preoteasa

**Contact information**:firstname.lastname@aalto.fi

**Job description**:
The goal of this project is to build upon previous work in Prof. Tripakis' group on
compositional verification of Simulink models. Simulink is a modeling and simulation tool for
embedded control systems, widespread in several domains, in particular, automotive. We are building
a tool chain that checks Simulink models w.r.t. various correctness criteria, based on the refinement
calculus theory for reactive systems [EMSOFT 2014]. The goal of this project is to connect the existing
tool chain developed in Matlab and Python (parsing and code generation from Simulink models) to
external solvers and theorem provers such as dReal, Z3, and Isabelle, which will perform the actual
verification. The tool will be evaluated on real-life Simulink models provided by Toyota. Experience in
programming is required for this project. Experience in Matlab/Simulink is desirable, but not required.

**Additional information**: [EMSOFT 2014] Refinement
Calculus of Reactive Systems. EMSOFT 2014