[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]

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 ]

[15]

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.

[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]

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 fullfeatured, Lustrelike synchronous
language, this paper presents a conservative extension
where dataflow 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 nonstandard analysis which gives a
synchronous interpretation to the whole language, clarifies the
discrete/continuous interaction and the treatment of zerocrossings, and
also allows the correctness of the type system to be established.
The extended dataflow language is realized through a sourcetosource
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 offtheshelf numerical
solver using a simple but precise algorithm which treats causallyrelated
cascades of zerocrossings.
We have validated the viability of the approach through experiments with
the SUNDIALS library.

[10]

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 ]

[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 ]

[8]

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 ]

[7]

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 ]

[6]

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.

[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]

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 ]

[3]

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 ]

[2]

É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, pages 2130, Novi
Sad, Serbia, 2011. Schloss DagstuhlLeibnizZentrum fuer Informatik.
[ bib 
DOI 
full text on HAL 
http 
Abstract ]

[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 
full text on HAL ]
