Joseph Sifakis (Greek: Ιωσήφ Σηφάκης; born December 26, 1946) is a scientist who works with computers and is from Greece and France. In 2007, he was given the Turing Award, along with Edmund M. Clarke and E. Allen Emerson, for his research on model checking.

Biography

Joseph Sifakis was born in Heraklion, Crete, in 1946 and currently lives in France. He studied Electrical Engineering at the National Technical University of Athens and Computer Science at the University of Grenoble, where he received a French scholarship. He earned his engineering doctorate in 1974 from the University of Grenoble and later received a state doctorate from the same university in 1979.

He is currently Research Director Emeritus for the National Center for Scientific Research at the VERIMAG laboratory near Grenoble, which he founded. Sifakis has been a leading figure in the fields of Model Checking and Embedded Systems. He co-founded the CAV conference with Edmund M. Clarke and Amir Pnueli. The first CAV conference was held in Grenoble in 1989. He coordinated the ARTIST European Network of Excellence for research on Embedded Systems from 2004 to 2012.

Sifakis held the INRIA-Schneider endowed industrial chair from 2008 to 2011. He was a full professor and Director of the «Rigorous System Design Laboratory» at the School of Computer and Communication Sciences of EPFL from 2011 to 2016. He also served as a visiting professor at Tsinghua University from 2011 to 2012 and at SUSTech in 2019.

Sifakis was President of the Greek National Council for Research and Technology from 2014 to 2016.

Work

Sifakis worked on system verification and the use of formal methods in system design. He earned his doctorate by studying the principles of an algorithmic verification method later known as model checking. In 1982, this technique was used in Jean-Pierre Queille's PhD research to create the CESAR verification tool.

Sifakis led VERIMAG for fourteen years. VERIMAG was originally established as a joint industrial laboratory between CNRS and Verilog SA. The organization has partnered with companies like Airbus and Schneider Electric to develop methods and tools for creating safety-critical systems, including the SCADE synchronous programming environment based on the Lustre Language. Sifakis collaborated with Thomas Henzinger on verifying timed and hybrid systems and with Amir Pnueli and Oded Maler on synthesizing timed systems. He contributed to the development of verification tools such as the IF toolset, Kronos, CADP, and TGV. He also created theories to address challenges like state explosion using abstraction techniques.

Over the past twenty years, his work has focused on rigorous component-based design using the BIP component framework. More recently, he has studied the design of trustworthy autonomous systems, including self-driving cars. He authored the book Understanding and Changing the World, published by Springer in May 2022.

Awards and honors

• Turing Award in 2007
• Leonardo da Vinci Medal in 2012
• Grand Officer of the National Order of Merit, France in 2008
• Member of the French Academy of Engineering in 2008
• Commander of the Legion of Honor, France in 2011
• Member of the French Academy of Sciences in 2010
• Member of Academia Europaea in 2008
• Member of the American Academy of Arts and Sciences in 2015
• Member of the National Academy of Engineering in 2017
• Foreign member of the Chinese Academy of Sciences in 2019
• Member of the National Academy of Sciences in 2024