[17] Thi Minh Tuyen Nguyen and Claude Marché. Hardware-dependent proofs of numerical programs. In Jean-Pierre Jouannaud and Zhong Shao, editors, Certified Programs and Proofs, Lecture Notes in Computer Science, pages 314--329. Springer, December 2011. [ bib | full text on HAL ]
[16] Louis Mandel, Florence Plateau, and Marc Pouzet. Static scheduling of latency insensitive designs with Lucy-n. In Formal Methods in Computer Aided Design (FMCAD 2011), Austin, TX, USA, October 2011. [ bib | full text on HAL | .pdf ]
Lucy-n is a dataflow programming language similar to Lustre extended with a buffer operator. This language is based on the n-synchronous model which was initially introduced for programming multimedia streaming applications. In this article, we show that Lucy-n 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 Lucy-n program. Then, the Lucy-n 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 Many-Sorted Language. In Cesare Tinelli and Viorica Sofronie-Stokkermans, editors, Frontiers of Combining Systems, 8th International Symposium, Proceedings, volume 6989 of Lecture Notes in Computer Science, pages 87--102, Saarbrücken, Germany, October 2011. [ bib | .pdf ]
[14] François Bobot, Jean-Christophe Filliâtre, Claude Marché, and Andrei Paskevich. Why3: Shepherd your herd of provers. In Boogie 2011: First International Workshop on Intermediate Verification Languages, pages 53--64, Wroclaw, Poland, August 2011. https://hal.inria.fr/hal-00790310. [ 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, Jean-Christophe 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 102--118, 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 ad-hoc data structures based on pointers. As standards like DO-178C 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 user-provided 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] Jean-Christophe 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 65--81, 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, multi-core or network, and (3) a reliable fault-tolerance 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 45--59, 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.

Starting from a minimal, yet full-featured, Lustre-like synchronous language, this paper presents a conservative extension where data-flow equations can be mixed with ordinary differential equations (ODEs) with possible reset. A type system is proposed to statically distinguish discrete computations from continuous ones and to ensure that signals are used in their proper domains. We propose a semantics based on non-standard analysis which gives a synchronous interpretation to the whole language, clarifies the discrete/continuous interaction and the treatment of zero-crossings, and also allows the correctness of the type system to be established.

The extended data-flow language is realized through a source-to-source transformation into a synchronous subset, which can then be compiled using existing tools into routines that are both efficient and bounded in their use of memory. These routines are orchestrated with a single off-the-shelf numerical solver using a simple but precise algorithm which treats causally-related cascades of zero-crossings. We have validated the viability of the approach through experiments with the SUNDIALS library.

[9] Véronique Benzaken, Jean-Daniel Fekete, Pierre-Luc Hémery, Wael Khemiri, and Ioana Manolescu. EdiFlow: data-intensive 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 Schmidt-Schauß, editor, 22nd International Conference on Rewriting Techniques and Applications (RTA 11), volume 10 of Leibniz International Proceedings in Informatics (LIPIcs), pages 21--30, Novi Sad, Serbia, 2011. Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik. [ bib | DOI | full text on HAL | http | Abstract ]
[7] 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, Revised Selected Papers Presented at the International Conference, FoVeOOS 2010, volume 6528 of Lecture Notes in Computer Science, pages 153--167. Springer, January 2011. [ bib | full text on HAL ]
[6] Romain Bardou and Claude Marché. Perle de preuve: les tableaux creux. In Sylvain Conchon, editor, Vingt-deuxièmes Journées Francophones des Langages Applicatifs, La Bresse, France, January 2011. INRIA. [ bib ]
[5] Jean-Christophe Filliâtre and Krishnamani Kalyanasundaram. Une bibliothèque de calcul distribué pour Objective Caml. In Sylvain Conchon, editor, Vingt-deuxiè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 Lucy-n. In Sylvain Conchon, editor, Vingt-deuxièmes Journées Francophones des Langages Applicatifs, La Bresse, France, January 2011. INRIA. [ bib | .pdf ]
Lucy-n 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 sous-typage. 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 floating-point algorithms in Coq. In Elisardo Antelo, David Hough, and Paolo Ienne, editors, Proceedings of the 20th IEEE Symposium on Computer Arithmetic, pages 243--252, Tübingen, Germany, 2011. [ bib | DOI | full text on HAL ]
[2] David Baelde, Romain Beauxis, and Samuel Mimram. Liquidsoap: A high-level 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, Jean-Daniel Fekete, Pierre-Luc Hémery, Wael Khemiri, and Ioana Manolescu. EdiFlow: data-intensive 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 ]