IMDEA Software

IMDEA initiative

Home > Events > Invited Talks > 2010 > Developing temporal abstract domains that prove the temporal specifications of reactive systems

Julien Bertrane

Monday, May 10, 2010

11:00am IMDEA conference room

Julien Bertrane, Researcher, Computer Science Departament, Carnegie Mellon University, USA

Developing temporal abstract domains that prove the temporal specifications of reactive systems

Abstract:

We consider the complex behaviors of embedded systems with several communicating imperfectly-clocked synchronous systems. In order to prove statically and automatically their properties, we introduced a “time-continuous” semantics and several ad hoc temporal abstract domains.

Then we show how to build new temporal domains from these simple basic domains, through the use of abstract transformers and of reduced products. The temporal aspects of this domains eases the automatisation of some of this optimizations and makes reductions more precise.