SMT4ABS: Combining SMT-Solving with Type Checking for Real-Time ABS Programs

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 techniqu es 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 cu rrently 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 variab les. 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 decision procedures. 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 deve lop 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.