Wiki Agenda Contact Version française

Publications 2013

Back

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

Books and book chapters

[2] Benjamin Wack, Sylvain Conchon, Judicaël Courant, Marc de Falco, Gilles Dowek, Jean-Christophe Filliâtre, and Stéphane Gonnord. Informatique pour tous en classes préparatoires aux grandes écoles : Manuel d'algorithmique et programmation structurée avec Python. Eyrolles, August 2013. [ bib | full text on HAL | http ]
[1] Sylvie Boldo and Guillaume Melquiond. Informatique Mathématique, une photographie en 2013, chapter Arithmétique des ordinateurs et preuves formelles, pages 189--220. Presses Universitaires de Perpignan, Perpignan, France, 2013. [ bib | full text on HAL ]

Journals

[5] Sylvie Boldo, François Clément, Jean-Christophe Filliâtre, Micaela Mayero, Guillaume Melquiond, and Pierre Weis. Wave equation numerical resolution: a comprehensive mechanized proof of a C program. Journal of Automated Reasoning, 50(4):423--456, April 2013. [ bib | DOI | full text on HAL ]
[4] Véronique Benzaken, Giuseppe Castagna, Dario Colazzo, and Kim Nguyen. Optimizing XML querying using type-based document projection. ACM Transactions on Database Systems (TODS), 2013. [ bib | full text on HAL ]
[3] Guillaume Melquiond, Werner Georg Nowak, and Paul Zimmermann. Numerical approximation of the Masser-Gramain constant to four decimal digits: delta=1.819.... Mathematics of Computation, 82:1235--1246, 2013. [ bib | DOI | full text on HAL ]
[2] Diego Arroyuelo, Francisco Claude, Sebastian Maneth, Veli Mäkinen, Gonzalo Navarro, Kim Nguyen, Jouni Sirén, and Niko Välimäki. Fast in-memory XPath search using compressed indexes. Software: Practice and Experience, pages n/a--n/a, 2013. [ bib | DOI ]
Keywords: XML, succinct data structures, XPath, tree automata
[1] Érik Martin-Dorel, Guillaume Melquiond, and Jean-Michel Muller. Some issues related to double roundings. BIT Numerical Mathematics, 53(4):897--924, 2013. [ bib | DOI | full text on HAL ]

Conferences

[20] Sylvain Conchon, Amit Goel, Sava Krstić, Alain Mebsout, and Fatiha Zaïdi. Invariants for finite instances and beyond. In FMCAD, pages 61--68, Portland, Oregon, États-Unis, October 2013. [ bib | DOI | full text on HAL ]
Verification of safety properties of concurrent programs with an arbitrary numbers of processes is an old challenge. In particular, complex parameterized protocols like FLASH are still out of the scope of state-of-the-art model checkers. In this paper, we describe a new algorithm, called Brab, that is able to automatically infer invariants strong enough to prove a protocol like FLASH. Brab computes over-approximations of backward reachable states that are checked to be unreachable in a finite instance of the system. These approximations (candidate invariants) are then model checked together with the original safety properties. Completeness of the approach is ensured by a mechanism for backtracking on spurious traces introduced by too coarse approximations.

[19] Guillaume Baudart, Florent Jacquemard, Louis Mandel, and Marc Pouzet. A synchronous embedding of Antescofo, a domain-specific language for interactive mixed music. In Thirteen International Conference on Embedded Software (EMSOFT'13), Montreal, Canada, September 2013. [ bib | full text on HAL | .pdf ]
Antescofo is recently developed software for musical score following and mixed music: it automatically, and in real-time, synchronizes electronic instruments with a musician playing on a classical instrument. Therefore, it faces some of the same major challenges as embedded systems.

The system provides a programming language used by composers to specify musical pieces that mix interacting electronic and classical instruments. This language is developed with and for musicians and it continues to evolve according to their needs. Yet its semantics has only recently been formally defined. This paper presents a synchronous semantics for the core language of Antescofo and an alternative implementation based on an embedding inside an existing synchronous language, namely ReactiveML. The semantics reduces to a few rules, is mathematically precise and leads to an interpretor of only a few hundred lines. The efficiency of this interpretor compares well with that of the actual implementation: on all musical pieces we have tested, response times have been less than the reaction time of the human ear. Moreover, this embedding permitted the prototyping of several new programming constructs, some of which are described in this paper.

[18] Guillaume Baudart, Louis Mandel, and Marc Pouzet. Programming mixed music in ReactiveML. In ACM SIGPLAN Workshop on Functional Art, Music, Modeling and Design (FARM'13), Boston, USA, September 2013. Workshop ICFP 2013. [ bib | full text on HAL | .pdf ]
Mixed music is about live musicians interacting with electronic parts which are controlled by a computer during the performance. It allows composers to use and combine traditional instruments with complex synthesized sounds and other electronic devices. There are several languages dedicated to the writing of mixed music scores. Among them, the Antescofo language coupled with an advanced score follower allows a composer to manage the reactive aspects of musical performances: how electronic parts interact with a musician. However these domain specific languages do not offer the expressiveness of functional programming.

We embed the Antescofo language in a reactive functional programming language, ReactiveML. This approach offers to the composer recursion, higher order, inductive types, as well as a simple way to program complex reactive behaviors thanks to the synchronous model of concurrency on which ReactiveML is built. This article presents how to program mixed music in ReactiveML through several examples.

[17] Louis Mandel, Cédric Pasteur, and Marc Pouzet. Time refinement in a functional synchronous language. In Proceedings of 15th ACM SIGPLAN International Symposium on Principles and Practice of Declarative Programming (PPDP'13), Madrid, Spain, September 2013. [ bib | full text on HAL | .pdf ]
Concurrent and reactive systems often exhibit multiple time scales. For instance, in a discrete simulation, the scale at which agents communicate might be very different from the scale used to model the internals of each agent.

We propose an extension of the synchronous model of concurrency, called reactive domains, to simplify the programming of such systems. Reactive domains allow the creation of local time scales and enable refinement, that is, the replacement of an approximation of a system with a more detailed version without changing its behavior as observed by the rest of the program.

Our work is applied to the ReactiveML language, which extends ML with synchronous language constructs. We present an operational semantics for the extended language and a type system that ensures the soundness of programs.

[16] Catherine Lelay. A New Formalization of Power Series in Coq. In 5th Coq Workshop, pages 1--2, Rennes, France, July 2013. http://coq.inria.fr/coq-workshop/2013#Lelay. [ bib | full text on HAL ]
[15] Jasmin C. Blanchette and Andrei Paskevich. TFF1: The TPTP typed first-order form with rank-1 polymorphism. In 24th International Conference on Automated Deduction (CADE-24), volume 7898 of Lecture Notes in Artificial Intelligence, Lake Placid, USA, June 2013. Springer. [ bib | full text on HAL | .pdf ]
[14] Jean-Christophe Filliâtre. One logic to use them all. In 24th International Conference on Automated Deduction (CADE-24), volume 7898 of Lecture Notes in Artificial Intelligence, pages 1--20, Lake Placid, USA, June 2013. Springer. [ bib | full text on HAL ]
Keywords: Why3
[13] François Bobot, Jean-Christophe Filliâtre, Claude Marché, Guillaume Melquiond, and Andrei Paskevich. Preserving user proofs across specification changes. In Ernie Cohen and Andrey Rybalchenko, editors, Verified Software: Theories, Tools, Experiments (5th International Conference VSTTE), volume 8164 of Lecture Notes in Computer Science, pages 191--201, Atherton, USA, May 2013. Springer. [ bib | full text on HAL ]
Keywords: Why3
[12] Jean-Christophe Filliâtre and Andrei Paskevich. Why3 --- where programs meet provers. In Matthias Felleisen and Philippa Gardner, editors, Proceedings of the 22nd European Symposium on Programming, volume 7792 of Lecture Notes in Computer Science, pages 125--128. Springer, March 2013. [ bib | full text on HAL ]
Keywords: Why3
[11] Arthur Charguéraud. Pretty-big-step semantics. In Matthias Felleisen and Philippa Gardner, editors, Proceedings of the 22nd European Symposium on Programming, volume 7792 of Lecture Notes in Computer Science, pages 41--60. Springer, March 2013. [ bib | full text on HAL ]
[10] Claude Marché and Asma Tafat. Calcul de plus faible précondition, revisité en Why3. In Vingt-quatrièmes Journées Francophones des Langages Applicatifs, Aussois, France, February 2013. [ bib | full text on HAL ]
[9] Sylvain Conchon, Alain Mebsout, and Fatiha Zaïdi. Vérification de systèmes paramétrés avec Cubicle. In Vingt-quatrièmes Journées Francophones des Langages Applicatifs, Aussois, France, February 2013. [ bib | full text on HAL ]
[8] Jean-Christophe Filliâtre and Rémy El Sibaïe. Combine : une bibliothèque OCaml pour la combinatoire. In Vingt-quatrièmes Journées Francophones des Langages Applicatifs, Aussois, France, February 2013. http://www.lri.fr/~filliatr/combine/. [ bib | full text on HAL | .pdf ]
[7] Louis Mandel and Cédric Pasteur. Réactivité des systèmes coopératifs : le cas de ReactiveML. In Vingt-quatrièmes Journées Francophones des Langages Applicatifs, Aussois, France, February 2013. http://rml.lri.fr/jfla13. [ bib | full text on HAL | .pdf ]
La concurrence coopérative est un modèle de programmation très répandu. On peut par exemple l'utiliser en OCaml à travers des bibliothèques comme Lwt, Async ou Equeue. Il a de nombreux avantages tels que l'absence de courses critiques et des implantations légères et efficaces. Néanmoins, un des inconvénients majeurs de ce modèle est qu'il dépend de la discipline du programmeur pour garantir que le système est réactif : un processus peut empêcher les autres de s'exécuter.

ReactiveML est un langage qui étend OCaml avec des constructions de concurrence coopérative. Il propose une analyse statique, l'analyse de réactivité, qui permet de détecter les expressions qui risquent de produire des comportements non coopératifs. Dans cet article, nous présentons cette analyse statique qui se définit à l'aide d'un système de types et effets. Ainsi, comme le typage de données aide les programmeurs à détecter des erreurs d'exécution au plus tôt, l'analyse de réactivité aide à détecter des erreurs de concurrence.

[6] Umut A. Acar, Arthur Charguéraud, and Mike Rainey. Scheduling parallel programs by work stealing with private deques. In Proceedings of the 18th ACM SIGPLAN symposium on Principles and practice of parallel programming, PPoPP '13, pages 219--228. ACM Press, February 2013. [ bib | DOI | full text on HAL ]
[5] Véronique Benzaken, Giuseppe Castagna, Kim Nguyen, and Jérôme Siméon. Static and dynamic semantics of NoSQL languages. In R. Cousot, editor, Proceedings of the 40th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, Roma, Italy, January 2013. ACM Press. [ bib | full text on HAL ]
[4] Sylvie Boldo. How to compute the area of a triangle: a formal revisit. In Proceedings of the 21th IEEE Symposium on Computer Arithmetic, Austin, Texas, USA, 2013. [ bib | full text on HAL ]
[3] Sylvie Boldo, Jacques-Henri Jourdan, Xavier Leroy, and Guillaume Melquiond. A formally-verified C compiler supporting floating-point arithmetic. In Proceedings of the 21th IEEE Symposium on Computer Arithmetic, Austin, Texas, USA, 2013. [ bib | full text on HAL ]
[2] Jean-Christophe Filliâtre. Deductive Program Verification. In Nate Foster, Philippa Gardner, Alan Schmitt, Gareth Smith, Peter Thieman, and Tobias Wrigstad, editors, Programming Languages Mentoring Workshop (PLMW 2013), Rome, Italy, January 2013. [ bib | full text on HAL ]
[1] Daisuke Ishii, Guillaume Melquiond, and Shin Nakajima. Inductive verification of hybrid automata with strongest postcondition calculus. In Einar Broch Johnsen and Luigia Petre, editors, Proceedings of the 10th Conference on Integrated Formal Methods, volume 7940 of Lecture Notes in Computer Science, pages 139--153, Turku, Finland, 2013. [ bib | DOI | full text on HAL ]

PhD theses

[4] Asma Tafat. Preuves par raffinement de programmes avec pointeurs. Thèse de doctorat, Université Paris-Sud, September 2013. [ bib | full text on HAL ]
[3] Mohamed Iguernelala. Strengthening the Heart of an SMT-Solver: Design and Implementation of Efficient Decision Procedures. Thèse de doctorat, Université Paris-Sud, June 2013. [ bib | full text on HAL ]
[2] Cédric Auger. Compilation Certifiée de SCADE/LUSTRE. Thèse de doctorat, Université Paris-Sud, February 2013. http://tel.archives-ouvertes.fr/tel-00818169/. [ bib | full text on HAL ]
[1] Paolo Herms. Certification of a Tool Chain for Deductive Program Verification. Thèse de doctorat, Université Paris-Sud, January 2013. http://tel.archives-ouvertes.fr/tel-00789543. [ bib | full text on HAL ]

Misc.

[4] Jean-Christophe Filliâtre. Deductive program verification with Why3. Lecture notes for the First DigiCosme Spring School, https://www.lri.fr/~marche/DigiCosmeSchool/filliatre.html, 2013. [ bib ]
Keywords: Why3
[3] Claire Dross, Sylvain Conchon, Johannes Kanig, and Andrei Paskevich. Adding decision procedures to SMT solvers using axioms with triggers. Submitted, 2013. [ bib | full text on HAL | .pdf ]
SMT solvers are efficient tools to decide the satisfiability of ground formulas, including a number of built-in theories such as congruence, linear arithmetic, arrays, and bit-vectors. Adding a theory to that list requires delving into the implementation details of a given SMT solver, and is done mainly by the developers of the solver itself. For many useful theories, one can alternatively provide a first-order axiomatization. However, in the presence of quantifiers, SMT solvers are incomplete and exhibit unpredictable behavior. Consequently, this approach can not provide us with a complete and terminating treatment of the theory of interest. In this paper, we propose a framework to solve this problem, based on the notion of instantiation patterns, also known as triggers. Triggers are annotations that suggest instances which are more likely to be useful in proof search. They are implemented in all SMT solvers that handle first-order logic and are included in the SMT-LIB format. In our framework, the user provides a theory axiomatization with triggers, along with a proof of completeness and termination properties of this axiomatization, and obtains a sound, complete, and terminating solver for her theory in return. We describe and prove a corresponding extension of the traditional Abstract DPLL Modulo Theory framework. Implementing this mechanism in a given SMT solver requires a one-time development effort. We believe that this effort is not greater than that of adding a single decision procedure to the same SMT solver. We have implemented the proposed extension in the Alt-Ergo prover and we discuss some implementation details in the paper. To show that our framework can handle complex theories, we prove completeness and termination of a feature-rich axiomatization of doubly-linked lists. Our tests show that our approach results in a better performance of the solver on goals that stem from the verification of programs manipulating doubly-linked lists.

[2] Sylvain Conchon, Mohamed Iguernelala, and Alain Mebsout. A Collaborative Framework for Non-Linear Integer Arithmetic Reasoning in Alt-Ergo. 2013. [ bib | full text on HAL | http ]
[1] Sandrine Blazy, Christine Paulin-Mohring, and David Pichardie, editors. Interactive Theorem Proving - 4th International Conference, ITP 2013, Rennes, France, July 22-26, 2013. Proceedings., volume 7998 of Lecture Notes in Computer Science. Springer, 2013. [ bib | DOI | http ]

Reports

[5] François Bobot, Jean-Christophe Filliâtre, Claude Marché, Guillaume Melquiond, and Andrei Paskevich. The Why3 platform, version 0.82. LRI, CNRS & Univ. Paris-Sud & INRIA Saclay, version 0.82 edition, December 2013. http://why3.lri.fr/download/manual-0.82.pdf. [ bib | full text on HAL | .pdf ]
[4] Cédric Auger, Zohir Bouzid, Pierre Courtieu, Sébastien Tixeuil, and Xavier Urbain. Certified impossibility results for byzantine-tolerant mobile robots. Research Report 1560, LRI, June 2013. [ bib | full text on HAL | http | .pdf ]
[3] François Bobot, Jean-Christophe Filliâtre, Claude Marché, Guillaume Melquiond, and Andrei Paskevich. The Why3 platform, version 0.81. LRI, CNRS & Univ. Paris-Sud & INRIA Saclay, version 0.81 edition, March 2013. http://why3.lri.fr/download/manual-0.81.pdf. [ bib | full text on HAL | .pdf ]
Keywords: Why3
[2] Antoine Rousseau, Aurélie Darnaud, Brice Goglin, Céline Acharian, Christine Leininger, Christophe Godin, Clarisse Holik, Claude Kirchner, Diane Rives, Elodie Darquie, Erwan Kerrien, Fabrice Neyret, Florent Masseglia, Florian Dufour, Gérard Berry, Gilles Dowek, Hélène Robak, Hélène Xypas, Irina Illina, Isabelle Gnaedig, Joanna Jongwane, Jocelyne Ehrel, Laurent Viennot, Laure Guion, Lisette Calderan, Lola Kovacic, Marie Collin, Marie-Agnès Enard, Marie-Hélène Comte, Martin Quinson, Martine Olivi, Mathieu Giraud, Mathilde Dorémus, Mia Ogouchi, Muriel Droin, Nathalie Lacaux, Nicolas Rougier, Nicolas Roussel, Pascal Guitton, Pierre Peterlongo, Rose-Marie Cornus, Simon Vandermeersch, Sophie Maheo, Sylvain Lefebvre, Sylvie Boldo, Thierry Viéville, Véronique Poirel, Aline Chabreuil, Arnaud Fischer, Claude Farge, Claude Vadel, Isabelle Astic, Jean-Pierre Dumont, Loic Féjoz, Patrick Rambert, Pierre Paradinas, Sophie De Quatrebarbes, and Stéphane Laurent. Médiation scientifique : une facette de nos métiers de la recherche. Interne, Inria, March 2013. [ bib | full text on HAL | http ]
Dans ce monde devenu numérique nous savons que c'est une de nos missions d'acteur de la recherche publique, que de rendre accessibles les sciences du numérique au plus grand nombre. Ceci afin que chaque citoyenne et citoyen maîtrise, au delà des usages, les principaux fondements de cette mutation numérique. Et nous croyons que c'est l'acquisition d'une culture scientifique sur ces sujets qui est le levier de cette appropriation. C'est notre mission et notre plaisir d'y contribuer. Ce document a pour but d'aider chaque collègue Inria intéressé à participer à ce volet de nos missions. Devenue une facette de notre métier, comme le rappelle le Plan Stratégique Inria [1], ce que nous appelons médiation scientifique en sciences du numérique (alias, " mecsci ") se professionnalise et change d'échelle. Et c'est environ 1 % de nos ressources qui a vocation à y être consacré. Pour tout l'institut on parle donc de près de 40 équivalents temps-plein distribués à travers le travail quotidien ou ponctuel de plusieurs centaines de collègues chercheurs, ingénieurs, communicants, etc.. Une telle énergie mérite d'être bien employée : au service des meilleurs objectifs ; vers des cibles bien définies qui ont de vrais besoins sur ces sujets ; dans le cadre d'actions leviers qui aident à faire bouger les choses ; et avec une méthodologie efficace qui optimise ce que nous investissons dans de telles activités ; tout en respectant et en encourageant les dynamiques locales et individuelles indépendantes qui restent les sources vives de la médiation scientifique. Voilà pourquoi il y a juste besoin d'offrir en partage à chacune et chacun les éléments fondateurs et méthodologiques de cette médiation scientifique. Offrir aussi quelques bonnes pratiques très concrètes. On parle donc ici d'une organisation distribuée d'actions collaboratives d'où émerge le service public de popularisation scientifique visé. C'est ce que ce document se propose de décrire ici.

Keywords: médiation scientifique ; culture scientifique ; recherche ; popularisation des sciences ; service public.
[1] Martin Clochard. Proving programs with binders, automatically. Master's thesis, Master Parisien de Recherche en Informatique, 2013. [ bib ]

Back

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


This page was generated by bibtex2html.