A.M. TURING AWARD WINNERS BY...

France – 2007

Short Annotated Bibliography

- 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.* - 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.* - 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.* - 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.* - 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.* - 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.* - 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.* - 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. - 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.* - 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.* - 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.* - 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.* - 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.*