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 2010


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

Books and book chapters

[1] Jean-Michel Muller, Nicolas Brisebarre, Florent de Dinechin, Claude-Pierre Jeannerod, Vincent Lefèvre, Guillaume Melquiond, Nathalie Revol, Damien Stehlé, and Serge Torres. Handbook of Floating-Point Arithmetic. Birkhäuser, 2010. [ bib ]


[3] Marc Pouzet and Pascal Raymond. Modular Static Scheduling of Synchronous Data-flow Networks: An efficient symbolic representation. Journal of Design Automation for Embedded Systems, 2010. Special issue of selected papers from System Week. [ bib ]
[2] Marc Daumas and Guillaume Melquiond. Certification of bounds on expressions involving rounded operators. Transactions on Mathematical Software, 37(1), 2010. [ bib | DOI | full paper on HAL ]
[1] Yannick Moy and Claude Marché. Modular inference of subprogram contracts for safety checking. Journal of Symbolic Computation, 45:1184-1211, 2010. [ bib | DOI | full paper on HAL ]


[20] Albert Benveniste, Benoit Caillaud, and Marc Pouzet. The Fundamentals of Hybrid Systems Modelers. In 49th IEEE International Conference on Decision and Control (CDC), Atlanta, Georgia, USA, December 15-17 2010. [ bib ]
[19] Sylvain Conchon, Évelyne Contejean, and Mohamed Iguernelala. Ground Associative and Commutative Completion Modulo Shostak Theories. In Andrei Voronkov, editor, LPAR, 17th International Conference on Logic for Programming, Artificial Intelligence and Reasoning, EasyChair Proceedings, Yogyakarta, Indonesia, October 2010. (short paper). [ bib ]
[18] M. Barbosa, Jean-Christophe Filliâtre, J. Sousa Pinto, and B. Vieira. A Deductive Verification Platform for Cryptographic Software. In 4th International Workshop on Foundations and Techniques for Open Source Software Certification (OpenCert 2010), volume 33, Pisa, Italy, September 2010. Electronic Communications of the EASST. [ bib | http ]
[17] Ali Ayad and Claude Marché. Multi-prover verification of floating-point programs. In Jürgen Giesl and Reiner Hähnle, editors, Fifth International Joint Conference on Automated Reasoning, volume 6173 of Lecture Notes in Artificial Intelligence, pages 127-141, Edinburgh, Scotland, July 2010. Springer. [ bib | .pdf ]
[16] Sylvie Boldo, François Clément, Jean-Christophe Filliâtre, Micaela Mayero, Guillaume Melquiond, and Pierre Weis. Formal Proof of a Wave Equation Resolution Scheme: the Method Error. In Matt Kaufmann and Lawrence C. Paulson, editors, Proceedings of the first Interactive Theorem Proving Conference, volume 6172 of LNCS, pages 147-162, Edinburgh, Scotland, July 2010. Springer. (merge of TPHOLs and ACL2). [ bib | full paper on HAL ]
[15] Sylvie Boldo. Formal verification of numerical programs: from C annotated programs to Coq proofs. In Proceedings of the Third International Workshop on Numerical Software Verification, Edinburgh, Scotland, July 2010. NSV-8. [ bib | full paper on HAL ]
[14] Asma Tafat, Sylvain Boulmé, and Claude Marché. A refinement methodology for object-oriented programs. In Bernhard Beckert and Claude Marché, editors, Formal Verification of Object-Oriented Software, Papers Presented at the International Conference, Karlsruhe Reports in Informatics, pages 143-159, Paris, France, June 2010. [ bib ]
[13] Louis Mandel, Florence Plateau, and Marc Pouzet. Lucy-n: a n-synchronous extension of Lustre. In Tenth International Conference on Mathematics of Program Construction (MPC 2010), Québec, Canada, June 2010. [ bib | .pdf ]
Synchronous functional languages such as Lustre or Lucid Synchrone define a restricted class of Kahn Process Networks which can be executed with no buffer. Every expression is associated to a clock indicating the instants when a value is present. A dedicated type system, the clock calculus, checks that the actual clock of a stream equals its expected clock and thus does not need to be buffered. The n-synchrony relaxes synchrony by allowing the communication through bounded buffers whose size is computed at compile-time. It is obtained by extending the clock calculus with a subtyping rule which defines buffering points.

This paper presents the first implementation of the n-synchronous model inside a Lustre-like language called Lucy-n. The language extends Lustre with an explicit buffer construct whose size is automatically computed during the clock calculus. This clock calculus is defined as an inference type system and is parametrized by the clock language and the algorithm used to solve subtyping constraints. We detail here one algorithm based on the abstraction of clocks, an idea originally introduced in [?]. The paper presents a simpler, yet more precise, clock abstraction for which the main algebraic properties have been proved in Coq. Finally, we illustrate the language on various examples including a video application.

[12] Sylvie Boldo and Thi Minh Tuyen Nguyen. Hardware-independent proofs of numerical programs. In César Muñoz, editor, Proceedings of the Second NASA Formal Methods Symposium, NASA Conference Publication, pages 14-23, Washington D.C., USA, April 2010. [ bib | full paper on HAL | PDF ]
[11] Louis Mandel, Florence Plateau, and Marc Pouzet. Clock typing of n-synchronous programs. In Designing Correct