VERIMAG (UMR 5104)

Embedded systems

Verimag
Lab home-page : http://www-verimag.imag.fr/
Activity report : Verimag 2005-2009 (pdf, 1,78Mo)
AERES evaluation report : Report May 2010 (pdf, 161,29 ko)
Publications'URLs : Verimag's list of publications
Embedded systems, formal methods, model-checking, timed and hybrid systems, synchronous languages, provable security and cryptology, program verification, component-based design.
Themes Synchronous languages, modeling, design and validation of embedded systems
Design and validation of distributed and complex systems with extra-functional properties, such as soft and hard real-time, security, performance
Design and verification of systems involving real-time clocks and continuous variables
Highlights and distinctions Joseph Sifakis Turing award 2007
Member of the French academy of science, member of the French Academy of Technologies, member of the Academia Europaea
CNRS Silver Medal
Nicolas Halbwachs Member of the Academia Europaea
Saddek Bensalem Research Foundation for Avionics and Space prize, 2010
Paul Caspi and Nicolas Halbwachs French Academy of Science prize, 2004
AERES assessment A+ "Verimag is a jewel of the French research in computer science. Thematically focused on verification and security of computer systems, it acquired a very large international reputation. Its scientific production is excellent. The contractual activity as well as the scientific and industrial cooperations are outstanding."
Faculty 23
Researchers 9
Habilitation 14
"Produisants AERES" 88%
PhD students 30
Publications Journals : 10
Conferences: 68
Funding K€
Mean value per year
1 494

 

Verimag addresses issues and challenges on embedded systems. It is focused on the following themes:

  • Synchronous languages, modeling, design and validation of embedded systems
  • Distributed Complex Systems, Design and validation of distributed and complex systems with extra functional properties, like soft and hard real-time, security, performance Timed and hybrid systems, Design and verification of systems involving real-time clocks and continuous variables

Joseph Sifakis, the founder of Verimag, played a prominent role in the invention of "model-checking", a very successful approach for the automatic verification of software, systems and circuits. For this achievement, jointly with E. Clarke and A. Emerson, he received in 2008 the Turing Award, considered as the Nobel Prize in computer science. The approach was successfully extended to the modeling and verification of timed and hybrid systems, and to the verification of security protocols. Verimag develops also the BIP framework for embedded components, the success of which was awarded in 2010 by the Research Foundation for Avionics and Space. It has pioneered synchronous programming, developing the synchronous data-flow programming language Lustre. Lustre is today the core of the industrial tool SCADE (developed by Esterel Technologies), which is a worldwide de-facto standard for the development of critical control software. This success story motivated a prize from the French Academy of Science (P. Caspi and N. Halbwachs, 2004). The synchronous approach is currently extended towards modeling and validation of various kinds of systems, including distributed systems, systems on chip and sensor networks.
Verimag coordinates the series of European networks of excellence Artist, Artist2 and Artist-Design, which structures the community of research on embedded systems in Europe. Verimag has chaired and/or organized several major international conferences, such as ETAPS'02, HSCC'03, TACAS'05, CAV'09, EMSOFT'09, MEMOCODE'10.