[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]
|
Manuel Barbosa, Jean-Christophe Filliâtre, Jorge Sousa Pinto, and Bárbara
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]
|
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 text on HAL ]
|
[16]
|
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 |
full text on HAL ]
|
[15]
|
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.
|
[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.
http://digbib.ubka.uni-karlsruhe.de/volltexte/1000019083.
[ bib |
full text on HAL ]
|
[13]
|
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 text on HAL |
PDF ]
|
[12]
|
Évelyne Contejean, Pierre Courtieu, Julien Forest, Andrei Paskevich, Olivier
Pons, and Xavier Urbain.
A3PAT, an Approach for Certified Automated Termination Proofs.
In Éric Cariou, Laurence Duchien, and Yves Ledru, editors,
Journées nationales du GDR-GPL, Pau, France, March 2010. GDR GPL.
[ bib ]
|
[11]
|
Alessandro Cimatti, Anders Franzen, Alberto Griggio, Krishnamani
Kalyanasundaram, and Marco Roveri.
Tighter integration of BDDs and SMT for predicate abstraction.
In Design, Automation & Test in Europe, Dresden. Germany,
March 2010. IEEE.
[ bib |
full text on HAL ]
|
[10]
|
Louis Mandel, Florence Plateau, and Marc Pouzet.
Lucy-n : une extension n-synchrone de Lustre.
In Éric Cariou, Laurence Duchien, and Yves Ledru, editors,
Journées nationales du GDR-GPL, Pau, France, March 2010. GDR GPL.
[ bib ]
|
[9]
|
Louis Mandel, Florence Plateau, and Marc Pouzet.
Clock typing of n-synchronous programs.
In Designing Correct Circuits (DCC 2010), Paphos, Cyprus,
March 2010.
[ bib ]
|
[8]
|
Paolo Herms.
Certification of a chain for deductive program verification.
In Yves Bertot, editor, 2nd Coq Workshop, satellite of ITP'10,
2010.
[ bib |
full text on HAL ]
|
[7]
|
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 Interactive Theorem Proving, volume 6172 of Lecture
Notes in Computer Science, pages 147--162. Springer, 2010.
[ bib |
DOI |
full text on HAL ]
|
[6]
|
Elena Tushkanova, Alain Giorgetti, Claude Marché, and Olga Kouchnarenko.
Specifying generic Java programs: two case studies.
In Claus Brabrand and Pierre-Etienne Moreau, editors, Tenth
Workshop on Language Descriptions, Tools and Applications. ACM Press, 2010.
[ bib |
full text on HAL ]
|
[5]
|
Louis Mandel.
Cours de ReactiveML.
In Vingt-et-unièmes Journées Francophones des Langages
Applicatifs, Vieux-Port La Ciotat, France, January 2010. INRIA.
[ bib |
.pdf ]
|
[4]
|
Louis Mandel, Florence Plateau, and Marc Pouzet.
Lucy-n : une extension n-synchrone de Lustre.
In Vingt-et-unièmes Journées Francophones des Langages
Applicatifs, Vieux-Port La Ciotat, France, January 2010. INRIA.
[ bib |
.pdf ]
Les langages synchrones flot de données permettent de programmer
des réseaux de processus communicant sans buffers.
Pour cela, chaque
flot est associé à un type d'horloges, qui indique les instants de
présence de valeurs sur le flot. La communication entre deux
processus f et g peut être faite sans buffer si le
type du flot de sortie de f est égal au type du flot d'entrée
de g.
Un système de type, le calcul d'horloge, infère des types tels que
cette condition est vérifiée.
Le modèle n-synchrone a pour but de relâcher ce modèle de
programmation en autorisant les communications à travers des buffers
de taille bornée. En pratique, cela consiste à introduire une
règle de sous-typage dans le calcul d'horloge.
Nous avons présenté l'année dernière un article décrivant comment
abstraire des horloges pour vérifier la relation de
sous-typage. Cette année, nous présentons un langage de
programmation n-synchrone : Lucy-n. Dans ce langage, l'inférence
des types d'horloges est paramétrable par l'algorithme de résolution
des contraintes de sous-typage. Nous montrons ici un algorithme
basé sur les travaux de
l'an dernier et comment programmer en Lucy-n à travers l'exemple
d'une application de traitement multimédia.
|
[3]
|
Sylvain Conchon, Jean-Christophe Filliâtre, Fabrice Le Fessant, Julien
Robert, and Guillaume Von Tokarski.
Observation temps-réel de programmes Caml.
In Vingt-et-unièmes Journées Francophones des Langages
Applicatifs, Vieux-Port La Ciotat, France, January 2010. INRIA.
[ bib |
.pdf ]
|
[2]
|
Évelyne Contejean, Pierre Courtieu, Julien Forest, Andrei Paskevich, Olivier
Pons, and Xavier Urbain.
A3PAT, an Approach for Certified Automated Termination Proofs.
In John P. Gallagher and Janis Voigtländer, editors, Partial
Evaluation and Program Manipulation, pages 63--72, Madrid, Spain, January
2010. ACM Press.
[ bib |
DOI |
Abstract ]
|
[1]
|
Sebastian Maneth and Kim Nguyen.
Xpath whole query optimization.
In 36th International Conference on Very Large Data Bases
(VLDB'2010), volume 3, pages 882--893, 2010.
[ bib ]
|