CAV 2009

The CAV 20th anniversary edition is over now. For a week, people from the DCS team have been quite busy helping with the organisation, attending lectures and talking about science and French cuisine. More pictures to come on the CAV website.

DCS Day

The first 2009 DCS day took place at Autrans in Vercors. Besides, while permanent members of the group were talking seriously, PhD and Master students spent the first afternoon crosscountry-skiing, some of them for the first time. The detailed program and the abstracts of the talks are available here, the slides are given below.

• CORBINEAU Pierre : Equality and equivalence relations in formal proofs
• BLECH Jan Olaf : Certifying deadlock-freedom of BIP models -- a case study for the certifcation of safety critical software
• GALLIEN Matthieu : Toward a more dependable software architecture for autonomous robots
• NGUYEN Thanh-Hung : D-Finder: a tool for compositional deadlock detection and verification
• FALCONE Ylies : Enforcement monitoring wrt. the safety-progress classification of properties

Morning session

• GARNIER Florent: Termination of fair execution v.s. positive almost sure termination of infinite state programs under probabilistic fair schedulers. Application to the verification of randomized distributed concurrent communication protocols
• DAUBIGNARD Marion: Towards a proof system for computational indistinguishability
• SFAXI Lilia: Construction de composants surs : Le modèle CIF (Component Information Flow)
• GALLIEN Matthieu: Data flow embedded systems: DOL to BIP translation
• SAMPAIO ELESBAO MAZZA Eduardo: Formal methods and software liability
• PRATIKAKIS Polyvios: Extending L2CA for the verification of multi-threaded programs

Afternoon session

• PIETREK Artur: Use of the LLVM framework for the MSIL code generation
• KONECNY Filip: Software verification using counter automata
• SIMACEK Jiri: Symbolic verification of pointer programs using tree automata
• PROCHNOW Steffen: Modeling systems based on semi-formal graphical formalism
• ABDELLATIF Tesnim: Real-time implementation of BIP
• COMBAZ Jacques: Real-time implementation of BIP : clocks and real-time constraints

DCS Day

The second 2008 DCS day has taken place at Col de Porte. We enjoyed ten presentations by team members, and an extra one by our guest Doron Peled. Slides are available below. Some brave ones also climbed the mountaintop of Chamechaude and (almost) everybody watched France and Romania tie -- a good score for peace within the DCS team.

Lundi

• Thanh-Hung NGUYEN, Compositional verification for component-based systems and application
• Simon BLIUDZE, A notion of expressiveness for component-based systems
• Laurent MOUNIER, Modelling and analysis of WSNs
• Sylvain BOULME, Vérification modulaire d'invariants
• Radu IOSIF, What else is decidable about integer arrays?

Mardi

• Judicaël COURANT, Partage de secret
• Pascal LAFOURCADE, Neighbourhood problems in wireless communication
• Jean-François MONIN, F91 en Coq
• Doron PELED, Discriminative model-checking and its application for genetic programming
• Florent GARNIER, Terminaison en temps moyen fini de systèmes de règles probabilistes
• Jacques COMBAZ and Mohamad JABER, Fine grain quality management

Prof. Joseph SIFAKIS receives Turing Award

ACM, the Association for Computing Machinery, has named Edmund M. Clarke, E. Allen Emerson, and Joseph Sifakis the winners of the 2007 A.M. Turing Award, widely considered the most prestigious award in computing, for their original and continuing research in a quality assurance process known as Model Checking. Their innovations transformed this approach from a theoretical technique to a highly effective verification technology that enables computer hardware and software engineers to find errors efficiently in complex system designs. This transformation has resulted in increased assurance that the systems perform as intended by the designers.

Dr. Sifakis is the founder of Verimag Laboratory, a leading research center for embedded systems in Grenoble, France, where he was director from 1993-2006. He is Research Director of Centre National de la Recherche Scientifique, and Director of the CARNOT Institute on Intelligent Software and Systems in Grenoble. Dr. Sifakis is a member of the editorial board of several journals, and the scientific coordinator of the Artist2 and ArtistDesign European Networks of Excellence on Embedded Systems Design. He is co-founder with Edmund Clarke, Robert Kurshan, and Amir Pnueli of the International Conference on Computer Aided Verification (CAV). He earned a degree in electrical engineering from the Technical University of Athens and a Ph.D. in computer science from the University of Grenoble.

DCS Day

The first 2008 DCS day has taken place at La Veyrie, Bernin. We had talks from:

• Yassin CHKOURI
• Imen BENHFAIEDH
• Mohamad JABER
• Thanh-Hung NGUYEN
• Vassiliki SFYRLA
• Chaouki ZERRARI

We are welcoming Prof. SONG Fangmin (Nanjing University)

Within the project Types, Processes and Applications to Security and Biological Systems we are welcoming Professor SONG Fangmin from the Nanjing University. Professor SONG will visit us from 3 to 18 December.

DCS new web site online

The web site is now online

Please, feel free to send us any remark.

DCS Green day

The DCS Green day will take place September 6th 2007.

Program

• 9h00-11h00: 4 exposes
• 11h00-11h30: Pause
• 11h30-12h30: 2 exposes
• 12h30-14h00: lunch
• 14h00-15h30 Discussion between permanents
• 15h30-16h00: Pause
• 16h00-18h00: 4 exposes