Contact Version française

The ProVal team was stopped at the end of August 2012, and reborn into a new team Toccata
These pages do not evolve anymore, please follow the link above for up-to-date informations about our team.

Publications 2006

Back

Books / Journals / Conferences / PhD theses / Misc. / Reports

Books and book chapters

[1] Paul Caspi, Grégoire Hamon, and Marc Pouzet. Systèmes Temps-réel : Techniques de Description et de Vérification - Théorie et Outils, volume 1, chapter Lucid Synchrone, un langage de programmation des systèmes réactifs, pages 217-260. Hermes, 2006. [ bib ]

Journals

[3] Sylvain Conchon and Sava Krstić. Strategies for combining decision procedures. Theoretical Computer Science, 354(2):187-210, 2006. Special Issue of TCS dedicated to a refereed selection of papers presented at TACAS'03. [ bib ]
[2] Jean-Christophe Filliâtre. Formal Proof of a Program: Find. Science of Computer Programming, 64:332-240, 2006. [ bib | DOI | PDF | .pdf ]
[1] Alain Girault, Xavier Nicollin, and Marc Pouzet. Automatic Rate Desynchronization of Embedded Reactive Programs. ACM Transactions on Embedded Computing Systems (TECS), 5(3), 2006. [ bib ]

Conferences

[15] Jean-Louis Colaço, Grégoire Hamon, and Marc Pouzet. Mixing Signals and Modes in Synchronous Data-flow Systems. In ACM International Conference on Embedded Software (EMSOFT'06), Seoul, South Korea, October 2006. [ bib ]
[14] Sylvain Conchon and Jean-Christophe Filliâtre. Type-Safe Modular Hash-Consing. In ACM SIGPLAN Workshop on ML, Portland, Oregon, September 2006. [ bib | PDF | .pdf ]
[13] Jean-Christophe Filliâtre. Backtracking iterators. In ACM SIGPLAN Workshop on ML, Portland, Oregon, September 2006. [ bib | PDF | .pdf ]
[12] Claude Marché and Nicolas Rousset. Verification of Java Card applets behavior with respect to transactions and card tears. In Dang Van Hung and Paritosh Pandya, editors, 4th IEEE International Conference on Software Engineering and Formal Methods (SEFM'06), Pune, India, September 2006. IEEE Comp. Soc. Press. [ bib | .ps ]
[11] Sylvie Boldo. Pitfalls of a full floating-point proof: example on the formal proof of the Veltkamp/Dekker algorithms. In Ulrich Furbach and Natarajan Shankar, editors, Third International Joint Conference on Automated Reasoning, volume 4130 of Lecture Notes in Computer Science, pages 52-66, Seattle, USA, August 2006. Springer. [ bib | PDF | .pdf ]
[10] Nicolas Halbwachs and Louis Mandel. Simulation and verification of asynchronous systems by means of a synchronous model. In Sixth International Conference on Application of Concurrency to System Design (ACSD'06), pages 3-14, Turku, Finland, June 2006. [ bib | PDF | .pdf ]
[9] Ludovic Samper, Florence Maraninchi, Laurent Mounier, and Louis Mandel. GLONEMO: Global and accurate formal models for the analysis of ad hoc sensor networks. In Proceedings of the First International Conference on Integrated Internet Ad hoc and Sensor Networks (InterSense'06), Nice, France, May 2006. ACM. [ bib | PDF | .pdf ]
[8] Sylvie Boldo and César Muñoz. Provably faithful evaluation of polynomials. In Proceedings of the 21st Annual ACM Symposium on Applied Computing, volume 2, pages 1328-1332, Dijon, France, April 2006. [ bib | full paper on HAL ]
[7] June Andronick and Boutheina Chetali. An Environment for Securing Smart Cards Embedded C Code. In International Conference on Research in Smart Cards (Esmart'06), 2006. [ bib | PDF | .pdf ]
[6] Philippe Audebaud and Christine Paulin-Mohring. Proofs of randomized algorithms in Coq. In Tarmo Uustalu, editor, Mathematics of Program Construction, MPC 2006, volume 4014 of Lecture Notes in Computer Science, Kuressaare, Estonia, July 2006. Springer. [ bib | PDF | .pdf ]
[5] Jean-Christophe Filliâtre. Itérer avec persistance. In Dix-septièmes Journées Francophones des Langages Applicatifs. INRIA, January 2006. [ bib | .ps.gz ]
[4] Claude Marché and Hans Zantema. The termination competition 2006. In Alfons Geser and Harald Sondergaard, editors, Extended Abstracts of the 8th International Workshop on Termination, WST'06, August 2006. http://www.lri.fr/~marche/termination-competition/. [ bib | http ]
[3] Albert Cohen, Marc Duranton, Christine Eisenbeis, Claire Pagetti, Florence Plateau, and Marc Pouzet. N-Synchronous Kahn Networks: a Relaxed Model of Synchrony for Real-Time Systems. In ACM International Conference on Principles of Programming Languages (POPL'06) [2]. [ bib ]
[2] Albert Cohen, Marc Duranton, Christine Eisenbeis, Claire Pagetti, Florence Plateau, and Marc Pouzet. N-Synchronous Kahn Networks: a Relaxed Model of Synchrony for Real-Time Systems. In ACM International Conference on Principles of Programming Languages (POPL'06), Charleston, South Carolina, USA, January 2006. [ bib ]
[1] Sylvie Boldo, Marc Daumas, William Kahan, and Guillaume Melquiond. Proof and certification for an accurate discriminant. In 12th IMACS-GAMM International Symposium on Scientific Computing, Computer Arithmetic and Validated Numerics, Duisburg,Germany, sep 2006. [ bib | http ]

PhD theses

[4] Nicolas Oury. Égalités et filtrages avec types dépendants dans le Calcul des Constructions Inductives. Thèse de doctorat, Université Paris-Sud, September 2006. [ bib ]
[3] Julien Signoles. Extension de ML avec raffinement : syntaxe, sémantiques et système de types. Thèse de doctorat, Université Paris-Sud, July 2006. [ bib ]
[2] June Andronick. Modélisation et vérification formelles de systèmes embarqués dans les cartes à microprocessur. Plateforme Java Card et Système d'exploitation. Thèse de doctorat, Université Paris-Sud, March 2006. [ bib | PDF | .pdf ]
[1] Louis Mandel. Conception, Sémantique et Implantation de ReactiveML : un langage à la ML pour la programmation réactive. PhD thesis, Université Paris 6, 2006. [ bib | PDF | .pdf ]

Misc.

Reports

[8] Louis Mandel. Prototype of AADL simulation in SCADE. ASSERT deliverable 4.3.2-2, ASSERT Project, November 2006. [ bib ]
[7] The Coq Development Team. The Coq Proof Assistant Reference Manual - Version V8.1, July 2006. http://coq.inria.fr. [ bib | http ]
[6] Marc Pouzet. Lucid Synchrone, version 3. Tutorial and reference manual. Université Paris-Sud, LRI, April 2006. [ bib | http ]
[5] Julien Signoles. Towards a ML extension with Refinement: a Semantic Issue. Technical Report 1440, LRI, University of Paris Sud, March 2006. [ bib | .pdf ]
[4] Louis Mandel. Report on modeling GALS in SCADE. ASSERT deliverable 4.3.2-1, ASSERT Project, February 2006. [ bib ]
[3] Jean-Christophe Filliâtre. Backtracking iterators. Research Report 1428, LRI, Université Paris Sud, January 2006. [ bib | .ps.gz ]
[2] Christine Paulin-Mohring. A library for reasoning on randomized algorithms in Coq. Description of a Coq contribution, Université Paris Sud, January 2006. http://www.lri.fr/~paulin/ALEA/library.pdf. [ bib | PDF | .pdf ]
[1] Stéphane Lescuyer. Codage de la logique du premier ordre polymorphe multi-sortée dans la logique sans sortes. Master's thesis, Master Parisien de Recherche en Informatique, 2006. [ bib ]

Back

Books / Journals / Conferences / PhD theses / Misc. / Reports


This page was generated by bibtex2html.