Walid Taha - Mathematical Equations as Executable Models of Mechanical Systems

Increasingly, hardware and software systems are being developed for applications where they must interact directly with a physical environment.  This trend significantly complicates testing computational systems and necessitates modeling and simulation of physical environments.  While numerous tools provide differing types of assistance in simulating physical systems, there are surprising gaps in the support that these tools provide.  Focusing on mechanics as an important class of physical environment, we address two such gaps, namely, the poor integration between different existing tools and the performance limitations of mainstream symbolic computing engines. 


Accepted poster and best demo award

DiaSim: a Parameterized Simulator for Pervasive Computing Applications - Julien Bruneau, Alexandre Blanquart, Nicolas Loriant, Charles Consel. Alexandre Blanquart received the Best Demo Award at ICPS'09 Demo Track.



Accepted paper in GPCE'09

The paper "A Generative Programming Approach to Developing Pervasive Computing Systems" --
D. Cassou et al. has been accepted in GPCE 2009, Oct. 4,5, Denver, Colorado.

Developing pervasive computing applications is a difficult task because it requires to deal with a wide range of issues: heterogeneous devices, entity distribution, entity coordination, low-level hardware knowledge... Besides requiring various areas of expertise, programming such applications involves writing a lot of administrative code to glue technologies together and to interface with both hardware and software components.


Johann Bourcier - Auto-Home: A Framework for Autonomic Pervasive Applications

Recent developments in computing devices such as miniaturization, increased autonomy and capacity of communications open new perspectives for applications. The ubiquitous or pervasive computing uses these new equipments to offer new types of applications. However, the realisation of software running on these environments raises a new set of challenges, such as building applications that can adapt themselves to their environment. This PhD thesis focuses on the autonomic computing field and offers an infrastructure for the execution of such applications.


Sandrine Blazy, ENSIEE - Vérification formelle d'un compilateur du langage C

Dans cet exposé, Sandrine Blazy présente succinctement CompCert, un compilateur optimisant d'un vaste sous-ensemble de C, ayant été formellement vérifié avec l'assistant à la preuve Coq. Elle explique en particulier la propriété de préservation sémantique de ce compilateur. Ensuite, elle détaille les choix sémantiques ayant été faits pour modéliser les comportements des programmes écrits dans le langage source du compilateur, ainsi que le modèle mémoire du compilateur.

Travail réalisé en collaboration avec Xavier Leroy.


24 mars 2009 - 14h00 - 076, LaBRI



Page 9 of 9