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