The Laureates

Copyright © Klaus Tschira Stiftung / Peter Badge

Joseph Sifakis

Born 26 December 1946, Heraklion, Greece

ACM A.M. Turing Award (2007) together with Edmund Clarke and E. Allen Emerson “for their role in developing Model-Checking into a highly effective verification technology that is widely adopted in the hardware and software industries.”

Sifakis, who is Greek by birth, has had French citizenship since 1976. He studied Electrical Engineering at the National Technical University of Athens and Computer Science at the University of Grenoble. He received his Ph.D. in Computer Science in 1974 and his State Doctorate in 1979 from the University of Grenoble. He is a professor at EPFL, Lausanne and the director of the Center of Integrative Research in Grenoble.

Joseph Sifakis has been a CNRS researcher in Grenoble where he founded the Verimag laboratory in 1993. Verimag is a leading research laboratory in the area of critical embedded systems. It developed the underlying theory and technology for the SCADE tool, used by Airbus for the design and validation of its critical real-time systems, and is becoming a de facto standard for aeronautics. Verimag has a lasting and strategic collaboration with ST Microelectronics, France Telecom R&D, and Airbus, through which numerous results on validation and testing have been transferred.

Joseph Sifakis is a member of the French Academy of Sciences, a member of the French National Academy of Engineering and a member of Academia Europaea. He is a Grand Officer of the French National Order of Merit and a Commander of the French Legion of Honor. He has received the Leonardo da Vinci Medal in 2012.

Sifakis’ work is characterized by an unusual recurrent pattern: the problem is first studied from an abstract, foundational point of view, which leads to methods and techniques for its solution, which, in turn, leads to an effective implementation that is successfully used in multiple industrial applications.

From 1974 to 1977 Sifakis studied Petri nets and obtained original and fundamental results on their verification and performance evaluation. From 1977 to 1982 he switched his attention to verification of transition systems and developed original results on the algorithmic verification of concurrent systems based on a fixpoint characterization of the modalities of a branching time temporal logic. These results laid down the foundations of model checking – the most widely used verification method in industry – and have been implemented for the first time in the CESAR model checker. This work was expanded during 1982-1988 to deal with model checking and temporal logics for the description of concurrent system specifications.

In the period 1988-2000, Sifakis extended this work to deal with modeling and verification of real-time systems. His main contributions include: 1) the modeling and verification of hybrid systems – models combining discrete and continuous dynamics; 2) the development and implementation of the KRONOS model checker, the first symbolic model checker for timed automata; 3) the study of symbolic synthesis algorithms for timed automata.

From 1998, Sifakis has actively promoted the emergence of embedded systems and has contributed to the constitution of an international and lively research community in this area. He has been the Scientific Coordinator of the ARTIST European Network of Excellence on Embedded System Design for more than 10 years. He actively contributed to setting up the ARTEMISIA industrial association for embedded systems in
Europe and is a co-founder of the EmSoft Conference and Embedded Systems Week.

During this later period, the main focus of Sifakis’ work is on the formalization of system design as a process leading from given requirements to trustworthy, optimized and correct-by-construction implementations. His results led to the development of the BIP component framework for rigorous system design. The framework consists of a language and a set of tools including source-to-source transformers, a compiler and the D-Finder tool for compositional verification. BIP is unique for its expressiveness.

It can describe mixed hardware/software systems. It uses a small and powerful set of primitives encompassing a general concept of system architecture. BIP was successfully used in several industrial projects, in particular for the componentization of legacy software and the automatic generation of implementations for manycore platforms.