The SMT4ABS-project is funded as a bilateral Norwegian-German cooperation within the PPP-programme for collaborative research support scheme (``Projektbezogener Personenaustausch''). The cooperation is funded by the
The planned duration of the project is 24 months, the funding period spans the years 2015 and 2016.
In a nutshell
This project brings together researchers from the fields of program
analysis and SMT-solving, to exploit the power of modern SMT-solving
technologies for the analysis of real-time software systems.
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
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.
The above techniques involve the satisfiability check of real-arithmetic
constraint systems, i.e., Boolean combinations of constraints comparing
polynomial expressions over real-valued variables. Though there are pure
algebraic techniques, their heuristic embedding in SAT-modulo-theories
(SMT) solving shaped up as much more efficient in practice. SMT solvers for
real arithmetic use highly tuned SAT-solving techniques to find solutions
for the Boolean structure of a real-arithmetic problem. The Boolean
solutions are validated in the underlying theory using real-algebraic
We will work with the ABS programming language, co-developed by the
Norwegian partner, which supports the programming of resource management
strategies. The Norwegian partners are experts in type systems for program
analysis. The German partners are experts in the development of SMT solvers
for real arithmetic. In this project we join expertise to develop
innovative techniques for the analysis of real-time software systems. The
collaboration is centered around young researchers and has a significant
long-term potential beyond the project's scientific goals.