Our new DAAD ppp project SMT4ABS will start in 2015.

The DAAD ppp project Combining SMT-Solving with Type Checking for Real-Time ABS Programs (SMT4ABS), in cooperation with the university of Oslo with a running time 01/2015-12/2016,  aims at the application of SMT solving for type checking.

We are interested in compositional verification techniques to prove a fundamental form of service-level agreement: that the response of a program or a program fragment is always delivered within a given deadline. We will study this problem in the context of dynamic deployment and resource management strategies which are relevant both for embedded devices and for virtualized programs and cloud computing, based on the notion of design by contract. Such techniques will allow the program developer to predict the behavior of a program before it is deployed, in contrast to the techniques currently in use, which assess timing behavior after deployment.