Our group offers two summer internships for the Summer 2015.
Details about the application process, and the time table for
these are available from the
webpage.
of the Deapartment of Information and Computer Science.
IBP - Invariant Based Programming in Isabelle/HOL
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
CVS - Compositional Verification of Simulink Models
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
