Publication 2007

article

Damian Barsotti, Leonor Prensa Nieto, Alwen Tiu. Verification of Clock Synchronization Algorithms: Experiments on a combination of deductive tools 2007 Formal Aspects of Computing 19 321-341 Ranko Lazic and Rajagopal Nagarajan 10.1007/s00165-007-0027-6 http://hal.inria.fr/inria-00097383/en/
Gilles Barthe, Leonor Prensa Nieto. Secure Information Flow for a Concurrent Language with Scheduling Formal Methods in Security Engineering Workshop (FMSE 04) 2007 Journal of Computer Security 16 647 - 689 IOS Press http://hal.inria.fr/inria-00097395/en/
Eunyoung Kang, Stephan Merz. Predicate Diagrams for the Verification of Real-Time Systems 2007 Formal Aspects of Computing 19 401-413 Springer London 10.1007/s00165-007-0030-y http://hal.inria.fr/inria-00112065/en/
Thierry Lecomte, Dominique Méry, Dominique Cansell. Patrons de conception prouvés Ingénierie dirigée par les modèles 2007 Génie Logiciel - Magazine de l'ingéniérie du logiciel et des systèmes 14-18 GL & IS - 8, rue du Parc - 92190 MEUDON http://hal.inria.fr/inria-00184827/en/
Dominique Méry, Stephan Merz. Specification and Refinement of Access Control 2007 Journal of Universal Computer Science 13 1073-1093 Institute for Information Processing and Computer Supported Media, Graz, Austria http://hal.inria.fr/inria-00147824/en/
Denis Roegel. A complex drawing in descriptive geometry 2007 Tugboat 28 218-228 TeX Users Group http://hal.inria.fr/inria-00172406/en/
Denis Roegel. Sphères, grands cercles et parallèles 2007 Cahiers Gutenberg Avril 2007 7-22 Association GUTenberg http://hal.inria.fr/inria-00111240/en/
Denis Roegel. Review of ``Mathematical Illustrations: A Manual of Geometry and PostScript'' 2007 Notices of the American Mathematical Society 54 38-42 American Mathematical Society http://hal.inria.fr/inria-00111243/en/

book

Michel Goossens, Frank Mittelbach, Sebastian Rahtz, Denis Roegel, Herbert Voss. The LaTeX Graphics Companion, Second Edition - Tools and Techniques for Computer Typesetting 2007 976 Addison-Wesley http://hal.inria.fr/inria-00172405/en/
Stephan Merz, Nicolas Navet. Modeling and Verification of Real-Time Systems - Formalisms and Software Tools 2008 Stephan Merz and Nicolas Navet 400 ISTE Publishing http://hal.inria.fr/inria-00187581/en/
Stephan Merz, Tobias Nipkow. Proceedings of the 6th International Workshop on Automated Verification of Critical Systems (AVoCS 2006) Electronic Notes in Theoretical Computer Science 2007 Michael Mislove 185 Electronic Notes in Theoretical Computer Science 151 Elsevier http://hal.inria.fr/inria-00187585/en/

incollection

Stephan Merz. An introduction to model checking Modeling and Verification of Real-Time Systems - Formalisms and Software Tools 2008 Stephan Merz and Nicolas Navet 81-116 ISTE Publishing http://hal.inria.fr/inria-00187577/en/
Dominique Cansell, Dominique Méry. Designing old and new distributed algorithms by replaying an incremental proof-based development Festschrift for Egon Börger LNCS 2007 Jean-Raymond Abrial and Uwe Glässer LNCS Springer-Verlag http://hal.inria.fr/inria-00174023/en/
Michael Leuschel, Dominique Cansell, Michael Butler. Validating and Animating Higher-Order Recursive Functions in B Festschrift for Egon Börger LNCS 2007 Jean-Raymond Abrial and Uwe Glässer LNCS Springer-Verlag http://hal.inria.fr/inria-00174013/en/

inproceedings

Nazim Benaissa, Dominique Cansell, Dominique Mery. Integration of Security Policy into System Modeling The 7th International B Conference - B2007 01 2007 http://hal.inria.fr/inria-00155143/en/
Dominique Cansell, Paul Gibson, Dominique Méry. Formal verification of tamper-evident storage for e-voting 5th IEEE International Conference on Software Engineering and Formal Methods - SEFM 2007 Fifth IEEE International Conference on Software Engineering and Formal Methods, 2007. SEFM 2007 2007 Mike Hinchey and Tiziana Margaria 329-338 IEEE 10.1109/{SEFM}.2007.21 http://hal.inria.fr/inria-00184833/en/
Dominique Cansell, Dominique Méry. Proved-Patterns-Based Development for Structured Programs. Computer Science - Theory and Applications, Second International, Symposium on Computer Science in Russia - CSR 2007 Computer Science – Theory and Applications ; Second International Symposium on Computer Science in Russia, CSR 2007, Ekaterinburg, Russia, September 3-7, 2007. Proceedings Lecture Notes in Computer Science 2007 Volker Diekert and Mikhail V. Volkov and Andrei Voronkov 4649 Lecture Notes in Computer Science 104-114 Springer Berlin / Heidelberg 10.1007/978-3-540-74510-5_13 http://hal.inria.fr/inria-00168307/en/
Diego Caminha B De Oliveira, David Déharbe, Pascal Fontaine. haRVey : satisfaisabilité et théories Approches Formelles dans l'Assistance au Développement de Logiciels - AFADL'07 Actes de la 8e conférence - AFADL Approches Formelles dans l’Assistance au 2007 Marie-Laure Potet, Pierre-Yves Schobbens, Hubert Toussaint, Germain Saval 287-288 http://hal.inria.fr/inria-00186640/en/
Loïc Fejoz, Stephan Merz. Dérivation d’algorithmes sans verrou à partir d’une spécification atomique Approches Formelles dans l'Assistance au Développement de Logiciels - AFADL07 Actes de la 8e conférence AFADL Approches Formelles dans l’Assistance au Développement de Logiciels 06 2007 Marie-Laure Potet and Pierre-Yves Schobbens and Hubert Toussaint and Germain Saval 213-226 Presses universitaires de Namur, 2007 http://hal.inria.fr/inria-00162146/en/
Pascal Fontaine. Combinations of Theories and the Bernays-Schönfinkel-Ramsey Class 4th International Verification Workshop - VERIFY'07 Proceedings of 4th International Verification Workshop in connection with CADE-21 Bremen, Germany, July 15-16, 2007 CEUR Workshop Proceedings 2007 Bernhard Beckert 259 CEUR Workshop Proceedings 37-54 http://hal.inria.fr/inria-00186639/en/
Clément Hurlin, Amine Chaib, Pascal Fontaine, Stephan Merz, Tjark Weber. Practical Proof Reconstruction for First-order Logic and Set-Theoretical Constructions The Isabelle Workshop 2007 - Isabelle'07 The 21st Conference on Automated Deduction - CADE-21 2007 Lucas Dixon, Moa Johansson 2-13 http://hal.inria.fr/inria-00186638/en/
Olfa Mosbahi, Jacques Jaray, Samir Ben Ahmed. Spécification et vérification des propriétés de vivacité en B événementiel 6ème Colloque Francophone sur la Modélisation des Systèmes Réactifs - MSR 2007 2007 16 pages http://hal.inria.fr/inria-00172417/en/
Olfa Mosbahi, Leila Jemni, Jacques Jaray. A FORMAL APPROACH FOR THE DEVELOPMENT OF AUTOMATED SYSTEMS 2nd International Conference on Software and Data Technologies - ICSOFT 2007 07 2007 http://hal.inria.fr/inria-00158908/en/
Olfa Mosbahi, Jacques Jaray. SPECIFICATION AND PROOF OF LIVENESS PROPERTIES IN B EVENT SYSTEMS 2nd International Conference on Software and Data Technologies - ICSOFT 2007 07 2007 http://hal.inria.fr/inria-00158906/en/
Bill Stoddart, Dominique Cansell, Frank Zeyda. Modelling and Proof Analysis of Interrupt Driven Scheduling The 7th International B Conference - B 2007 B 2007: Formal Specification and Development in B LNCS 01 2007 Jacques Jullian et Olga Kouchnarenko 4355/2006 LNCS 155-170 Springer 10.1007/11955757_14 http://hal.inria.fr/inria-00156871/en/
Yann Zimmermann. Développement formel de circuits électroniques par la méthode B Approches Formelles dans l'Assistance au Développement de Logiciels - AFADL'07 Actes de la 8e conférence AFADL - Approches Formelles dans l’Assistance au Développement de Logiciels 2007 Marie-Laure Potet and Pierre-Yves Schobbens and Hubert Toussaint and Germain Saval 181-198 Presses universitaires de Namur http://hal.inria.fr/inria-00172745/en/

phdthesis

Eunyoung Kang. Abstractions booléennes pour la vérification des systèmes temps-réel 11 2007 http://tel.archives-ouvertes.fr/tel-00195096/en/

techreport

Denis Roegel. Three dials, and a few more: a practical introduction to accurate gnomonics Technical Report 2007 70 http://hal.inria.fr/inria-00172407/en/