• go to E. Allen Emerson's profile page
  • go to A J Milner 's profile page
  • go to Ronald L Rivest's profile page
  • go to Jeffrey D Ullman's profile page
  • go to Judea Pearl's profile page
  • go to Yoshua Bengio's profile page
  • go to Michael O. Rabin 's profile page
  • go to Edsger W. Dijkstra's profile page
  • go to Charles W Bachman's profile page
  • go to Kristen Nygaard 's profile page
  • go to A. J. Perlis 's profile page
  • go to Dennis M. Ritchie 's profile page
  • go to Juris Hartmanis's profile page
  • go to Niklaus E. Wirth's profile page
  • go to Raj Reddy's profile page
  • go to Silvio Micali's profile page
  • go to Andrew C Yao's profile page
  • go to Edgar F. Codd's profile page
  • go to Yann LeCun's profile page
  • go to Stephen A Cook's profile page
  • go to John E Hopcroft's profile page
  • go to Alfred V Aho's profile page
  • go to Michael Stonebraker's profile page
  • go to John Backus 's profile page
A.M. TURING AWARD LAUREATES BY...
BIRTH:

December 26, 1946

EDUCATION:

Doctorate (1974, Electrical Engineering, National Technical University of Athens, Greece); State Doctorate (1979, Computer Science, University of Grenoble, France).

EXPERIENCE:

Since 1975, CNRS and University Joseph Fourier researcher; founder of Verimag Laboratory in Grenoble (CNRS, UGA), France; Professor at EPFL, (École Polytechnique Fédérale de Lausanne), October 2011-October 2016); INRIA-Schneider endowed industrial chair (2008-2011); Coordinator of Artist Design, the European Network of Excellence for Research on Embedded Systems (2008-2012); in addition to these appointments he has had broad experience with industries such as Airbus, Astrium, Ericsson, the European Space Agency, France Telecom, Philips, ST Microelectronics, Thalès. 

HONORS AND AWARDS:

CNRS Silver Medal (2001), Honorary doctorates from École Polytechnique Fédérale de Lausanne, Switzerland (2009), University of Athens (2010) and the International Hellenic University (2011); Honorary Professor of the University of Patras (2008); Member of the Academia Europaea (2008), the French National Academy of Engineering (2008), the French Academy of Sciences (2011), the American Academy of Arts and Sciences (2015) and the National Academy of Engineering (2017); Grand Officer of the French National Order of Merit (2008); Commander of the Legion of Honor (2011); Leonardo da Vinci Medal (2012); Commander of the Order of the Phoenix, Greece (2013); Logic in Computing Science (LICS) 2012 Test-of-Time Award for the paper "Symbolic model checking for real-time systems."

Joseph Sifakis DL Author Profile link

France – 2007
CITATION

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’ 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. In what follows his main achievements are briefly presented from a historical perspective.

From 1974 to 1977 Sifakis studied Petri nets and other models for concurrent systems [1]. During this period Sifakis obtained original and fundamental results on the structural properties of Petri nets as well as on the performance evaluation of timed Petri nets. These results are extensively used today for scheduling data-flow systems.

From 1977 to 1982 he switched his attention to verification of transition systems. Once again his work yielded original results on the algorithmic verification of concurrent systems based on a fix-point 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 [2].

Sifakis explains his shift to model checking research.

This work was expanded during 1982-1988 to deal with model checking and temporal logics for the description of concurrent system specifications [3]. The development of the CESAR model checker was funded by France Telecom and was extensively used for the certification of communication protocols. He went on to development a theory and techniques for computing property-preserving abstractions, which  have been effectively used to verify complex systems.

Stearns explains the basic concepts behind model checking.

In a later episode (1988-2000) he extended this work to deal with modeling and verification of real-time systems [7, 8, 9]. This included:

  1. the study of hybrid models – models combining discrete and continuous dynamics;
  2. the development and implementation of the KRONOS model checker, and, in collaboration with T. Henzinger, the first symbolic model checker for timed automata (work);
  3. in collaboration with O. Maler and  A. Pnueli the development and implementation of an efficient symbolic synthesis algorithm for timed;
  4. the study of compositional modeling techniques for real-time scheduling by using priorities.

In 1993 Sifakis founded the Verimag industrial laboratory, a joint-venture between the Computer Science and Applied Mathematics laboratory (IMAG) and VERILOG SA. Verimag has been funded by Airbus and Schneider Electric to develop methods and tools based on results produced by Sifakis and his team, mainly:

  1. The SCADE synchronous programming environment based on the Lustre language, used by Airbus for more than 15 years to develop safety critical systems, a de facto standard for aeronautics. SCADE has been qualified as a development tool by the FAA, EASA, and Transport Canada under DO-178B up to Level A.
  2. The ObjectGeode specification and validation tool for real-time distributed applications, which includes functional testing and verification techniques. This tool  was commercialized by Telelogic SA until the company was acquired  by IBM in 2008.
Sifakis discusses Verimag and defines “correctness by construction”.

Since 1997, Verimag has been a public research laboratory, associated with CNRS and the University of Grenoble. It has played a prominent role in the area of embedded systems by producing cutting edge results and leading research initiatives and projects in Europe.

From 1998, Sifakis has actively promoted the emergence of embedded systems and has contributed to the constitution of an international and live research community in this area. He has been the Scientific Coordinator of the ARTIST European Network of Excellence on Embedded System Design which has coordinated research of leading European teams in embedded systems 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.

Sifakis explains his shift to embedded systems.

During this later period Sifakis has also played a major role in the development and implementation of the BIP component framework for rigorous system design [10,11]. The implementation 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 [12,13]. 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 many-core platforms.

Further information on Joseph Sifakis and his research can be found here.

Author: Cristian S. Calude