Publications 2011
BackBooks / Journals / Conferences / PhD theses / Misc. / Reports
Books and book chapters
[2]  Sylvie Boldo and Thierry Viéville. Représentation numérique de l'information. In Gilles Dowek, editor, Introduction à la science informatique, Repères pour agir, pages 2372. CRDP Académie de Paris, July 2011. [ bib  http ] 
[1]  Sylvie Boldo and Thierry Viéville. Structuration et contrôle de l'information. In Gilles Dowek, editor, Introduction à la science informatique, Repères pour agir, pages 281308. CRDP Académie de Paris, July 2011. [ bib  http ] 
Journals
[5] 
JeanChristophe Filliâtre.
Deductive software verification.
International Journal on Software Tools for Technology Transfer
(STTT), 13(5):397403, August 2011.
[ bib 
DOI 
.pdf ]
Deductive software verification, also known as program proving, expresses the correctness of a program as a set of mathematical statements, called verification conditions. They are then discharged using either automated or interactive theorem provers. We briefly review this research area, with an emphasis on tools.

[4] 
Sylvie Boldo and JeanMichel Muller.
Exact and Approximated error of the FMA.
IEEE Transactions on Computers, 60(2):157164, February 2011.
[ bib 
full text on HAL ]
The fused multiply accumulateadd (FMA) instruction, specified by the IEEE 7542008 Standard for FloatingPoint Arithmetic, eases some calculations, and is already available on some current processors such as the Power PC or the Itanium. We first extend an earlier work on the computation of the exact error of an FMA (by giving more general conditions and providing a formal proof). Then, we present a new algorithm that computes an approximation to the error of an FMA, and provide error bounds and a formal proof for that algorithm.

[3]  Florent de Dinechin, Christoph Lauter, and Guillaume Melquiond. Certifying the floatingpoint implementation of an elementary function using Gappa. IEEE Transactions on Computers, 60(2):242253, 2011. [ bib  DOI  full text on HAL ] 
[2]  Sylvie Boldo and Thi Minh Tuyen Nguyen. Proofs of numerical programs when the compiler optimizes. Innovations in Systems and Software Engineering, 7:151160, 2011. [ bib  full text on HAL ] 
[1]  Sylvie Boldo and Claude Marché. Formal verification of numerical programs: from C annotated programs to mechanical proofs. Mathematics in Computer Science, 5:377393, 2011. [ bib  DOI  full text on HAL  .pdf ] 
Conferences
[17]  Thi Minh Tuyen Nguyen and Claude Marché. Hardwaredependent proofs of numerical programs. In JeanPierre Jouannaud and Zhong Shao, editors, Certified Programs and Proofs, Lecture Notes in Computer Science, pages 314329. Springer, December 2011. [ bib  full text on HAL ] 
[16] 
Louis Mandel, Florence Plateau, and Marc Pouzet.
Static scheduling of latency insensitive designs with Lucyn.
In Formal Methods in Computer Aided Design (FMCAD 2011),
Austin, TX, USA, October 2011.
[ bib 
full text on HAL 
.pdf ]
Lucyn is a dataflow programming language similar to Lustre extended with a buffer operator. This language is based on the nsynchronous model which was initially introduced for programming multimedia streaming applications. In this article, we show that Lucyn is also applicable to model Latency Insensitive Designs (LID). In order to model relay stations, we have to introduce a delay operator. Thanks to this new operator, a LID can be described by a Lucyn program. Then, the Lucyn compiler automatically provides static schedules for computation nodes and buffer sizes needed in the shell wrappers.

[15]  François Bobot and Andrei Paskevich. Expressing Polymorphic Types in a ManySorted Language. In Cesare Tinelli and Viorica SofronieStokkermans, editors, Frontiers of Combining Systems, 8th International Symposium, Proceedings, volume 6989 of Lecture Notes in Computer Science, pages 87102, Saarbrücken, Germany, October 2011. [ bib  .pdf ] 
[14] 
François Bobot, JeanChristophe Filliâtre, Claude Marché, and Andrei
Paskevich.
Why3: Shepherd your herd of provers.
In Boogie 2011: First International Workshop on Intermediate
Verification Languages, pages 5364, Wroclaw, Poland, August 2011.
https://hal.inria.fr/hal00790310.
[ bib 
full text on HAL ]
Why3 is the next generation of the Why software verification platform. Why3 clearly separates the purely logical specification part from generation of verification conditions for programs. This article focuses on the former part. Why3 comes with a new enhanced language of logical specification. It features a rich library of proof task transformations that can be chained to produce a suitable input for a large set of theorem provers, including SMT solvers, TPTP provers, as well as interactive proof assistants. Keywords: Why3 
[13] 
Claire Dross, JeanChristophe Filliâtre, and Yannick Moy.
Correct Code Containing Containers.
In 5th International Conference on Tests and Proofs (TAP'11),
volume 6706 of Lecture Notes in Computer Science, pages 102118,
Zurich, June 2011. Springer.
[ bib 
full text on HAL 
.pdf ]
For critical software development, containers such as lists, vectors, sets or maps are an attractive alternative to adhoc data structures based on pointers. As standards like DO178C put formal verification and testing on an equal footing, it is important to give users the ability to apply both to the verification of code using containers. In this paper, we present a definition of containers whose aim is to facilitate their use in certified software, using modern proof technology and novel specification languages. Correct usage of containers and userprovided correctness properties can be checked either by execution during testing or by formal proof with an automatic prover. We present a formal semantics for containers and an axiomatization of this semantics targeted at automatic provers. We have proved in Coq that the formal semantics is consistent and that the axiomatization thereof is correct.

[12] 
JeanChristophe Filliâtre and Krishnamani Kalyanasundaram.
Functory: A distributed computing library for Objective Caml.
In Trends in Functional Programming, volume 7193 of
Lecture Notes in Computer Science, pages 6581, Madrid, Spain, May 2011.
[ bib 
.pdf ]
We present Functory, a distributed computing library for Objective Caml. The main features of this library include (1) a polymorphic API, (2) several implementations to adapt to different deployment scenarios such as sequential, multicore or network, and (3) a reliable faulttolerance mechanism. This paper describes the motivation behind this work, as well as the design and implementation of the library. It also demonstrates the potential of the library using realistic experiments.

[11]  Sylvain Conchon, Évelyne Contejean, and Mohamed Iguernelala. Canonized Rewriting and Ground AC Completion Modulo Shostak Theories. In Parosh A. Abdulla and K. Rustan M. Leino, editors, Tools and Algorithms for the Construction and Analysis of Systems, volume 6605 of Lecture Notes in Computer Science, pages 4559, Saarbrücken, Germany, April 2011. Springer. [ bib  DOI  full text on HAL  .pdf  Abstract ] 
[10] 
Albert Benveniste, Timothy Bourke, Benoit Caillaud, and Marc Pouzet.
Divide and recycle: types and compilation for a hybrid synchronous
language.
In ACM SIGPLAN/SIGBED Conference on Languages, Compilers, Tools
and Theory for Embedded Systems (LCTES'11), Chicago, USA, April 2011.
[ bib 
.pdf ]
Hybrid modelers such as Simulink have become corner stones of embedded systems development. They allow both discrete controllers and their continuous environments to be expressed in a single language. Despite the availability of such tools, there remain a number of issues related to the lack of reproducibility of simulations and to the separation of the continuous part, which has to be exercised by a numerical solver, from the discrete part, which must be guaranteed not to evolve during a step.

[9]  Véronique Benzaken, JeanDaniel Fekete, PierreLuc Hémery, Wael Khemiri, and Ioana Manolescu. EdiFlow: dataintensive interactive workflows for visual analytics. In Serge Abiteboul, Christoph Koch, and Tan Kian Lee, editors, International Conference on Data Engineering (ICDE). IEEE Comp. Soc. Press, April 2011. [ bib  full text on HAL ] 
[8]  Évelyne Contejean, Pierre Courtieu, Julien Forest, Olivier Pons, and Xavier Urbain. Automated Certified Proofs with CiME3. In Manfred SchmidtSchauß, editor, 22nd International Conference on Rewriting Techniques and Applications (RTA 11), volume 10 of Leibniz International Proceedings in Informatics (LIPIcs), pages 2130, Novi Sad, Serbia, 2011. Schloss DagstuhlLeibnizZentrum fuer Informatik. [ bib  DOI  full text on HAL  http  Abstract ] 
[7]  Asma Tafat, Sylvain Boulmé, and Claude Marché. A refinement methodology for objectoriented programs. In Bernhard Beckert and Claude Marché, editors, Formal Verification of ObjectOriented Software, Revised Selected Papers Presented at the International Conference, FoVeOOS 2010, volume 6528 of Lecture Notes in Computer Science, pages 153167. Springer, January 2011. [ bib  full text on HAL ] 
[6]  Romain Bardou and Claude Marché. Perle de preuve: les tableaux creux. In Sylvain Conchon, editor, Vingtdeuxièmes Journées Francophones des Langages Applicatifs, La Bresse, France, January 2011. INRIA. [ bib ] 
[5]  JeanChristophe Filliâtre and Krishnamani Kalyanasundaram. Une bibliothèque de calcul distribué pour Objective Caml. In Sylvain Conchon, editor, Vingtdeuxièmes Journées Francophones des Langages Applicatifs, La Bresse, France, January 2011. INRIA. [ bib  .pdf ] 
[4] 
Louis Mandel and Florence Plateau.
Typage des horloges périodiques en Lucyn.
In Sylvain Conchon, editor, Vingtdeuxièmes Journées
Francophones des Langages Applicatifs, La Bresse, France, January 2011.
INRIA.
[ bib 
.pdf ]
Lucyn est un langage permettant de programmer des réseaux de processus communiquant à travers des buffers de taille bornée. La taille des buffers et les rythmes d'exécution relatifs des processus sont calculés par une phase de typage appelée calcul d'horloge. Ce typage nécessite la résolution d'un ensemble de contraintes de soustypage. L'an dernier, nous avons proposé un algorithme de résolution de ces contraintes utilisant des méthodes issues de l'interprétation abstraite. Cette année nous présentons un algorithme tirant profit de toute l'information contenue dans les types.

[3]  Sylvie Boldo and Guillaume Melquiond. Flocq: A unified library for proving floatingpoint algorithms in Coq. In Elisardo Antelo, David Hough, and Paolo Ienne, editors, Proceedings of the 20th IEEE Symposium on Computer Arithmetic, pages 243252, Tübingen, Germany, 2011. [ bib  DOI  full text on HAL ] 
[2]  David Baelde, Romain Beauxis, and Samuel Mimram. Liquidsoap: A highlevel programming language for multimedia streaming. In Ivana Cerná, Tibor Gyimóthy, Juraj Hromkovic, Keith G. Jeffery, Rastislav Královic, Marko Vukolic, and Stefan Wolf, editors, 37th Conference on Current Trends in Theory and Practice of Computer Science (SOFSEM'11), volume 6543 of Lecture Notes in Computer Science, Nový Smokovec, Slovakia, January 2011. Springer. [ bib ] 
[1]  Véronique Benzaken, JeanDaniel Fekete, PierreLuc Hémery, Wael Khemiri, and Ioana Manolescu. EdiFlow: dataintensive interactive workflows for visual analytics. In Serge Abiteboul, Christoph Koch, and Tan Kian Lee, editors, International Conference on Data Engineering (ICDE). IEEE Comp. Soc. Press, April 2011. [ bib ] 
PhD theses
[4]  François Bobot. Logique de séparation et vérification déductive. Thèse de doctorat, Université ParisSud, December 2011. [ bib  full text on HAL  .pdf ] 
[3]  JeanChristophe Filliâtre. Deductive Program Verification. Thèse d'habilitation, Université ParisSud, December 2011. [ bib  .pdf ] 
[2]  Romain Bardou. Verification of Pointer Programs Using Regions and Permissions. Thèse de doctorat, Université ParisSud, October 2011. http://proval.lri.fr/publications/bardou11phd.pdf. [ bib  full text on HAL  .pdf ] 
[1]  Stéphane Lescuyer. Formalisation et développement d'une tactique réflexive pour la démonstration automatique en Coq. Thèse de doctorat, Université ParisSud, January 2011. [ bib  full text on HAL  .pdf ] 
Misc.
[4]  Nuno Gaspar. Mechanized semantics into concurrent program verification. http://www.lri.fr/~gaspar/rgcoq.html, September 2011. A documented Coq library, work in progress. [ bib ] 
[3]  Philippe Audebaud and Christine PaulinMohring, editors. Science of Computer Programming. Special issue on the Mathematics of Program Construction (MPC 2008), volume 76. Elsevier Science Publishers, 2011. [ bib  DOI  http ] 
[2]  François Bobot and Andrei Paskevich. Expressing Polymorphic Types in a ManySorted Language, 2011. Preliminary report. http://hal.inria.fr/inria00591414/. [ bib ] 
[1]  Bernhard Beckert and Claude Marché, editors. Formal Verification of ObjectOriented Software, Revised Selected Papers Presented at the International Conference, FoVeOOS 2010, volume 6528 of Lecture Notes in Computer Science. Springer, January 2011. [ bib ] 
Reports
[10] 
Sylvie Boldo, François Clément, JeanChristophe Filliâtre, Micaela
Mayero, Guillaume Melquiond, and Pierre Weis.
Wave equation numerical resolution: Mathematics and program.
Research Report 7826, INRIA, December 2011.
[ bib 
full text on HAL ]
We formally prove the C program that implements a simple numerical scheme for the resolution of the onedimensional acoustic wave equation. Such an implementation introduces errors at several levels: the numerical scheme introduces method errors, and the floatingpoint computation leads to roundoff errors. We formally specify in Coq the numerical scheme, prove both the method error and the roundoff error of the program, and derive an upper bound for the total error. This proves the adequacy of the C program to the numerical scheme and the convergence of the effective computation. To our knowledge, this is the first time a numerical analysis program is fully machinechecked. Keywords: Formal proof of numerical program; Convergence of numerical scheme; Proof of C program; Coq formal proof; Acoustic wave equation; Partial differential equation; Rounding error analysis 
[9] 
François Bobot, JeanChristophe Filliâtre, Claude Marché, and Andrei
Paskevich.
The Why3 platform, version 0.71.
LRI, CNRS & Univ. ParisSud & INRIA Saclay, version 0.71 edition,
October 2011.
https://gforge.inria.fr/docman/view.php/2990/7635/manual.pdf.
[ bib ]
Keywords: Why3 
[8] 
Asma Tafat and Claude Marché.
Binary heaps formally verified in Why3.
Research Report 7780, INRIA, October 2011.
http://hal.inria.fr/inria00636083/en/.
[ bib 
full text on HAL ]
Keywords: Why3 
[7]  Krishnamani Kalyanasundaram and Claude Marché. Automated generation of loop invariants using predicate abstraction. Research Report 7714, INRIA, August 2011. http://hal.inria.fr/inria00615623/en/. [ bib  full text on HAL ] 
[6] 
François Bobot, JeanChristophe Filliâtre, Claude Marché, Guillaume
Melquiond, and Andrei Paskevich.
The Why3 platform.
LRI, CNRS & Univ. ParisSud & INRIA Saclay, version 0.64 edition,
February 2011.
http://why3.lri.fr/.
[ bib ]
Keywords: Why3 
[5]  Yannick Moy and Claude Marché. The Jessie plugin for Deduction Verification in FramaC  Tutorial and Reference Manual. INRIA & LRI, 2011. http://krakatoa.lri.fr/. [ bib  PDF  http ] 
[4]  Évelyne Contejean, Pierre Courtieu, Julien Forest, Olivier Pons, and Xavier Urbain. Automated Certified Proofs with CiME3. Technical Report 2044, Cédric laboratory, CNAM Paris, France, 2011. [ bib  .pdf  Abstract ] 
[3]  Thi Minh Tuyen Nguyen and Claude Marché. Proving floatingpoint numerical programs by analysis of their assembly code. Research Report 7655, INRIA, 2011. http://hal.inria.fr/inria00602266/en/. [ bib  full text on HAL ] 
[2]  Paolo Herms, Claude Marché, and Benjamin Monate. A certified multiprover verification condition generator. Research Report 7793, INRIA, 2011. http://hal.inria.fr/hal00639977/en/. [ bib  full text on HAL ] 
[1]  Catherine Lelay. étude de la différentiabilité et de l'intégrabilité en Coq : Application à la formule de d'Alembert pour l'équation des ondes. Master's thesis, Université Paris 7, 2011. http://www.lri.fr/~lelay/Rapport.pdf. [ bib ] 
Back
Books / Journals / Conferences / PhD theses / Misc. / Reports
This page was generated by bibtex2html.