MOSEL - Publications 2009

[1] Nazim Benaissa and Dominique Méry. Cryptographic protocols analysis in event b. In Seventh International Andrei Ershov Memorial Conference «PERSPECTIVES OF SYSTEM INFORMATICS» - PSI 2009, Lectures Notes in Computer Science, Russian Federation Novosibisrk, November 2009. Springer-Verlag. [ bib ]
[2] Nazim Benaissa and Dominique Méry. Cryptologic protocols analysis using proof-based patterns. In Seventh International Andrei Ershov Memorial Conference «PERSPECTIVES OF SYSTEM INFORMATICS» - PSI 2009, Lecture Notes in Computer Science, Russian Federation Novosibirsk, June 2009. Springer-Verlag. [ bib ]
[3] Nazim Benaissa and Dominique Méry. Développement combiné et prouvé de systèmes transactionnels cryptologiques. In Approches Formelles dans l'Assistance au Développement de Logiciels - AFADL 2009, France Toulouse, January 2009. [ bib ]
[4] Thomas Bouton, Diego Caminha B. De Oliveira, David Déharbe, and Pascal Fontaine. verit: an open, trustable and efficient smt-solver. In Renate A. Schmidt, editor, 22nd International Conference on Automated Deduction - CADE 22, volume 5663 of Lecture Notes in Computer Science, pages 151-156, Canada Montreal, 2009. Springer Berlin / Heidelberg. The original publication is available at www.springerlink.com. [ bib | DOI ]
[5] Diego Caminha B. De Oliveira, David Déharbe, and Pascal Fontaine. Combining decision procedures by (model-)equality propagation. Electronic Notes in Theoretical Computer Science, 240(2):113-128, 2009. [ bib | DOI ]
[6] Dominique Cansell, Dominique Méry, and Cyril Proch. System-on-chip design by proof-based refinement. International Journal on Software Tools for Technology Transfer (STTT), 11(3):217-238, March 2009. [ bib | DOI ]
[7] Mouna Chaouch-Saad, Bernadette Charron-Bost, and Stephan Merz. A reduction theorem for the verification of round-based distributed algorithms. In Olivier Bournez and Igor Potapov, editors, Reachability Problems 2009, volume 5797 of Lecture Notes in Computer Science, pages 93-106, France Palaiseau, 2009. Springer Berlin / Heidelberg. [ bib | DOI ]
[8] Bernadette Charron-Bost and Stephan Merz. Formal verification of a consensus algorithm in the heard-of model. International Journal of Software and Informatics, 3(2-3):273-303, 2009. [ bib | http ]
[9] David Déharbe, Pascal Fontaine, Anamaria Martins Moreira, Stephan Merz, and Anderson Santana De Oliveira. Automating model-based software engineering. In Colloque d'Informatique: Brésil/INRIA (COLIBRI), pages 22-27, Brazil Bento Gonçalves, 2009. [ bib ]
[10] Didier Fass. Design et ingénierie des systèmes homme-dans-la boucle. La revue des Ingénieurs, (440):50-51, May 2009. [ bib ]
[11] Didier Fass and Romain Lieber. Rationale for human modelling in human in the loop systems design. In 3rd Annual IEEE International Systems Conference, SysCon 2009, pages 27-30, Canada Vancouver, March 2009. IEEE. ISBN : 978-1-4244-3463-3. [ bib ]
[12] Pascal Fontaine. Combinations of theories for decidable fragments of first-order logic. In Silvio Ghilardi and Roberto Sebastiani, editors, 7th International Symposium, FroCoS 2009, volume 5749 of Lecture Notes in Computer Science, pages 263-278, Italy Trento, 2009. Springer Verlag. The original publication is available at www.springerlink.com. [ bib | DOI ]
[13] Francisco López Fraguas, Stephan Merz, and Juan Rodríguez Hortalá. A formalization of the semantics of functional-logic programming in isabelle. In 22nd International Conference on Theorem Proving in Higher-Order Logics : emerging trends session - TPHOLs 2009, Germany Munich, 2009. Technische Universität München. [ bib ]
[14] Dominique Méry. Refinement-based guidelines for algorithmic systems. International Journal of Software and Informatics, 3(2-3):197-239, September 2009. [ bib | http ]
[15] Dominique Méry. A simple refinement-based method for constructing algorithms. ACM SIGCSE Bulletin, 41(2):51-59, June 2009. [ bib | DOI ]
[16] Dominique Méry and Neeraj Kumar Singh. Pacemaker's functional behaviors in event-b. Research report, 2009. [ bib ]
[17] Joris Rehm. Gestion du temps par le raffinement. PhD thesis, Université Henri Poincaré - Nancy I, December 2009. [ bib ]
[18] Joris Rehm. Pattern based integration of time applied to the 2-slots simpson algorithm. In Integration of Model-based Formal Methods and Tools - IM_FMT'2009 - in IFM'2009, Germany Düsseldorf, 2009. [ bib ]
[19] Joris Rehm. A rodin plugin for quantitative timed models. In Michael Butler, Stefan Hallerstede, and Laurent Voisin, editors, Rodin User and Developer Workshop, United Kingdom Southampton, July 2009. [ bib ]
[20] Denis Roegel. An introduction to nomography: Garrigues' nomogram for the computation of easter. Tugboat, 30(1):88-104, 2009. [ bib ]
[21] Denis Roegel. Metapost macros for drawing chinese and japanese abaci. Tugboat, 30(1):74-79, 2009. [ bib ]
[22] Denis Roegel. Prototype fragments from babbage's first difference engine. IEEE Annals of the History of Computing, 31(2):70-75, 2009. [ bib ]
[23] Denis Roegel. Spheres, great circles and parallels. Tugboat, 30(1):80-87, 2009. [ bib ]
[24] Cristian Rosa, Martin Quinson, and Stephan Merz. Model-checking distributed applications with gras. In Exploiting Concurrency Efficiently and Correctly - EC<sup>2</sup> workshop associated to CAV 2009, France Grenoble, 2009. [ bib ]
[25] Cristian Rosa, Martin Quinson, and Stephan Merz. Model-checking distributed applications with gras. Research Report RR-7052, INRIA, 2009. [ bib ]
[26] Alexander Schimpf, Stephan Merz, and Jan-Georg Smaus. Construction of büchi automata for ltl model checking verified in isabelle/hol. In Tobias Nipkow and Christian Urban, editors, 22nd International Conference Theorem Proving in Higher-Order Logics - TPHOLs 2009, volume 5674 of Lecture Notes in Computer Science, pages 424-439, Germany Munich, 2009. Springer Berlin / Heidelberg. [ bib | DOI ]
[27] Julien Siebert, Joris Rehm, Vincent Chevrier, Laurent Ciarletta, and Dominique Méry. Aa4mm coordination model and event-b specification. Research Report RR-7081, INRIA, 2009. [ bib ]
[28] Mohamed Tounsi, Ahmed Hadj Kacem, Mohamed Mosbah, and Dominique Méry. A refinement approach for proving distributed algorithms : Examples of spanning tree problems. In Integration of Model-based Formal Methods and Tools - IM_FMT'2009 - in IFM'2009, Germany Düsseldorf, February 2009. [ bib ]

This file has been generated by bibtex2html 1.87.