A.M. TURING AWARD WINNERS BY...

Joseph Sifakis

France – 2007
Short Annotated Bibliography
  1. Sifakis, J. “Use of Petri nets for Performance Evaluation,” 3rd Intl. Symposium on Modeling and Evaluation, IFIP, North Holland, pp. 75-93, 1977.  This paper introduces a method for computing maximal firing frequencies of the transitions of a timed Petri net.
  2. Queille, J-P. and J. Sifakis, “Specification and Verification of Concurrent Systems,” CESAR International Symposium on Programming, Lecture Notes in Computer Science, Vol. 137, 1982, pp. 337 -– 351.  This is a presentation of the principle of model-checking and its implementation in the CESAR verification tool.
  3. Sifakis, J., “A unified approach for studying the properties of transition systems,” Theoretical Computer Science, Vol. 18, 1982.  This discusses fixpoint characterization of modalities of branching-time temporal logic that provides a basis for algorithmic verification.
  4. Nicollin, X. and J.Sifakis, “The algebra of timed processes ATP: theory and application,” Information and Computation, Vol. 114, Num. 1, Oct. 1994, pp. 131-178.  The presents a fully-axiomatized process algebra for timed systems.
  5. Loiseaux, C., S. Graf, J. Sifakis, A. Bouajjani and S. Bensalem, “Property Preserving Abstractions for the Verification of Concurrent Systems,” Formal Methods in System Design, Volume 6, Num. 1, 1995.  This introduces a notion of abstraction based on Galois connections and its application to the verification of concurrent systems.
  6. Alur, R., C. Courcoubetis, N. Halbwachs, T. Henzinger, P. Ho, X. Nicollin, A. Olivero, J. Sifakis, and S. Yovine, “The algorithmic analysis of hybrid systems,” Theoretical Computer Science, Vol. 138, 1995, pp. 3-34.  This presents a general theory for the algorithmic analysis of systems exhibiting both continuous and discrete dynamic behavior.
  7. Henzinger, T.A., X. Nicollin, J. Sifakis and S. Yovine, “Symbolic model checking for real-time systems,” Proceedings of the 7th Symposium. on Logics in Computer Science (LICS'92) and Information and Computation Volume 111, Num. 2, 1994, pp.193-244.  The first symbolic model-checking method for timed-CTL.
  8. Maler, O., A. Pnueli, J. Sifakis, “On the Synthesis of Discrete Controllers for Timed Systems,”, in E.W. Mayr and C. Puech (Eds.). Proceedings of STACS '95, Lecture Notes in Computer Science, Vol. 900, pp. 229-242, Springer, 1995.
  9. Bornot, S., and J.Sifakis, “An Algebraic Framework for Urgency,” Information and Computation, Vol. 163, 2000, pp. 172-202.  This deals with an original synthesis technique based on a fixpoint characterization of maximal controllers meeting a given property.
  10. Bliudze, S. and J. Sifakis, “The Algebra of Connectors - Structuring Interaction in BIP,” IEEE Transactions on Computers, Vol. 57, Num. 10, pp. 1315-1330, October, 2008. This deals with connectors, studied as terms of a fully-aximatized algebra, expressed as coordination constraints in a component-based systems.
  11. Basu, A., S. Bensalem, M. Bozga, J. Combaz, M. Jaber, T.-H. Nguyen and J. Sifakis, “Rigorous Component-Based System Design Using the BIP Framework,” IEEE Software, Vol. 28, Num. 3, 2011, pp. 41-48. This introduces BIP,  a component framework consisting of a coordination language and supporting tools including a compiler, a dedicated runtime and a compositional deadlock-freedom checker.
  12. Bliudze, S. and J. Sifakis, “A Notion of Glue Expressiveness for Component-Based Systems,” Proceedings of the 19th International Conference on Concurrency Theory (CONCUR'08), Lecture Notes in Computer Science, Vol. 5201, pp. 508-522, Springer, 2008. This introduces a notion of expressiveness for coordination mechanisms in component-based systems and a comparison of existing formalisms based on this notion.
  13. Bliudze, S. and J. Sifakis, “Synthesizing Glue Operators from Glue Constraints for the Construction of Component-Based Systems,” Software Composition 2011, pp. 51-67. This gives a method for synthesizing connectors expressing coordination in a component-based system from synchronization constraints.