Viorel Preoteasa

Summer 2015 Internships

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:

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


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