The ProVal team was stopped at the end of August 2012, and reborn into a new team
Toccata
These pages do not evolve anymore, please follow the link above for uptodate informations about our team.
Publications 2012
BackBooks / Journals / Conferences / PhD theses / Misc. / Reports
Books and book chapters
[2]  JeanChristophe Filliâtre. Course notes EJCP 2012, chapter Vérification déductive de programmes avec Why3. June 2012. [ bib  http ] 
[1]  Christine PaulinMohring. Course notes LASER summerschool 2011, chapter Introduction to the Coq proofassistant for practical software verification. Lecture Notes in Computer Science. Springer, 2012. to appear. [ bib  .pdf ] 
Journals
[4]  Guillaume Melquiond, Werner Georg Nowak, and Paul Zimmermann. Numerical approximation of the MasserGramain constant to four decimal digits: delta=1.819.... Mathematics of Computation, 2012. [ bib  full paper on HAL ] 
[3]  Guillaume Melquiond. Floatingpoint arithmetic in the Coq system. Information and Computation, 216:1423, 2012. [ bib  DOI ] 
[2]  Sylvie Boldo, François Clément, JeanChristophe 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, 2012. Accepted for publication. http://hal.inria.fr/hal00649240/en/. [ bib  full paper on HAL ] 
[1]  José Bacelar Almeida, Manuel Barbosa, JeanChristophe Filliâtre, Jorge Sousa Pinto, and Bárbara Vieira. CAOVerif: An OpenSource Deductive Verification Platform for Cryptographic Software Implementations. Science of Computer Programming, 2012. Accepted for publication. [ bib ] 
Conferences
[18]  Sylvie Boldo, Catherine Lelay, and Guillaume Melquiond. Improving Real Analysis in Coq: a UserFriendly Approach to Integrals and Derivatives. In Proceedings of the The Second International Conference on Certified Programs and Proofs, Kyoto, Japan, December 2012. [ bib  full paper on HAL ] 
[17] 
François Bobot and JeanChristophe Filliâtre.
Separation predicates: a taste of separation logic in firstorder
logic.
In 14th International Conference on Formal Ingineering Methods
(ICFEM), volume 7635 of Lecture Notes in Computer Science, Kyoto,
Japan, November 2012. Springer.
[ bib 
.pdf ]
This paper introduces separation predicates, a technique to reuse some ideas from separation logic in the framework of program verification using a traditional firstorder logic. The purpose is to benefit from existing specification languages, verification condition generators, and automated theorem provers. Separation predicates are automatically derived from userdefined inductive predicates. We illustrate this idea on a nontrivial case study, namely the composite pattern, which is specified in C/ACSL and verified in a fully automatic way using SMT solvers AltErgo, CVC3, and Z3.

[16] 
Mário Pereira, JeanChristophe Filliâtre, and Simão Melo de Sousa.
ARMY: a deductive verification platform for ARM programs using
Why3.
In INForum 2012, September 2012.
[ bib ]
Unstructured (lowlevel) programs tend to be challenging to prove correct, since the control flow is arbitrary complex and there are no obvious points in the code where to insert logical assertions. In this paper, we present a system to formally verify ARM programs, based on a flow sequentialization methodology and a formalized ARM semantics. This system, built upon the why3 verification platform, takes an annotated ARM program, turns it into a set of purely sequential flow programs, translates these programs' instructions into the corresponding formalized opcodes and finally calls the Why3 VCGen to generate the verification conditions that can then be discharged by provers. A prototype has been implemented and used to verify several programming examples.

[15] 
David Baelde, Pierre Courtieu, David GrossAmblard, and Christine
PaulinMohring.
Towards Provably Robust Watermarking.
In ITP 2012, August 2012.
[ bib 
.pdf ]
Watermarking techniques are used to help identifying copies of publicly released information. They consist in applying a slight and secret modification to the data before its release, in a way that should be robust, ie., remain recognizable even in (reasonably) modified copies of the data. In this paper, we present new results about the robustness of watermarking schemes against arbitrary attackers, and the formalization of those results in Coq. We used the ALEA library, which formalizes probability theory and models probabilistic programs using a simple monadic translation. This work illustrates the strengths and particularities of the induced style of reasoning about probabilistic programs. Our technique for proving robustness is adapted from methods commonly used for cryptographic protocols, and we discuss its relevance to the field of watermarking. Keywords: watermarking, probabilistic algorithms, formal proofs, security, interactive theorem proving 
[14] 
Sylvain Conchon, Amit Goel, Sava Krstić, Alain Mebsout, and Fatiha
Zaïdi.
Cubicle: A parallel SMTbased model checker for parameterized
systems.
In Madhusudan Parthasarathy and Sanjit A. Seshia, editors, CAV
2012: Proceedings of the 24th International Conference on Computer Aided
Verification, Lecture Notes in Computer Science, Berkeley, California, USA,
July 2012. Springer.
[ bib ]
Cubicle is a new model checker for verifying safety properties of parameterized systems. It implements a parallel symbolic backward reachability procedure using Satisfiabilty Modulo Theories. Experiments done on classic and challenging mutual exclusion algorithms and cache coherence protocols show that Cubicle is effective and competitive with stateoftheart model checkers.

[13] 
Louis Mandel and Florence Plateau.
Scheduling and buffer sizing of nsynchronous systems: Typing of
ultimately periodic clocks in Lucyn.
In Eleventh International Conference on Mathematics of Program
Construction (MPC'12), Madrid, Spain, June 2012.
[ bib 
.pdf ]
Lucyn is a language for programming networks of processes communicating through bounded buffers. A dedicated type system, termed a clock calculus, automatically computes static schedules of the processes and the sizes of the buffers between them.

[12] 
David Mentré, Claude Marché, JeanChristophe Filliâtre, and Masashi
Asuka.
Discharging proof obligations from Atelier B using multiple
automated provers.
In Steve Reeves and Elvinia Riccobene, editors, ABZ'2012  3rd
International Conference on Abstract State Machines, Alloy, B and Z, Lecture
Notes in Computer Science, Pisa, Italy, June 2012. Springer.
http://hal.inria.fr/hal00681781/en/.
[ bib 
full paper on HAL ]
We present a method to discharge proof obligations from Atelier B using multiple SMT solvers. It is based on a faithful modeling of B's set theory into polymorphic firstorder logic. We report on two case studies demonstrating a significant improvement in the ratio of obligations that are automatically discharged.

[11] 
François Bobot, Sylvain Conchon, Evelyne Contejean, Mohamed Iguernelala,
Assia Mahboubi, Alain Mebsout, and Guillaume Melquiond.
A Simplexbased extension of FourierMotzkin for solving linear
integer arithmetic.
In Bernhard Gramlich, Dale Miller, and Ulrike Sattler, editors,
IJCAR 2012: Proceedings of the 6th International Joint Conference on
Automated Reasoning, volume 7364 of Lecture Notes in Computer Science,
pages 6781, Manchester, UK, June 2012. Springer.
[ bib 
DOI ]
This paper describes a novel decision procedure for quantifierfree linear integer arithmetic. Standard techniques usually relax the initial problem to the rational domain and then proceed either by projection (e.g. OmegaTest) or by branching/cutting methods (branchandbound, branchandcut, Gomory cuts). Our approach tries to bridge the gap between the two techniques: it interleaves an exhaustive search for a model with bounds inference. These bounds are computed provided an oracle capable of finding constant positive linear combinations of affine forms. We also show how to design an efficient oracle based on the Simplex procedure. Our algorithm is proved sound, complete, and terminating and is implemented in the AltErgo theorem prover. Experimental results are promising and show that our approach is competitive with stateoftheart SMT solvers.

[10] 
JeanChristophe Filliâtre, Andrei Paskevich, and Aaron Stump.
The 2nd verified software competition: Experience report.
In Vladimir Klebanov and Sarah Grebing, editors, COMPARE2012:
1st International Workshop on Comparative Empirical Evaluation of Reasoning
Systems, Manchester, UK, June 2012. EasyChair.
[ bib 
.pdf ]
We report on the second verified software competition. It was organized by the three authors on a 48 hours period on November 810, 2011. This paper describes the competition, presents the five problems that were proposed to the participants, and gives an overview of the solutions sent by the 29 teams that entered the competition.

[9]  JeanChristophe Filliâtre. Combining Interactive and Automated Theorem Proving in Why3 (invited talk). In Keijo Heljanko and Hugo Herbelin, editors, Automation in Proof Assistants 2012, Tallinn, Estonia, April 2012. [ bib ] 
[8]  Catherine Lelay and Guillaume Melquiond. Différentiabilité et intégrabilité en Coq. Application à la formule de d'Alembert. In Vingttroisièmes Journées Francophones des Langages Applicatifs, Carnac, France, February 2012. [ bib  full paper on HAL ] 
[7]  Paolo Herms, Claude Marché, and Benjamin Monate. A certified multiprover verification condition generator. In Rajeev Joshi, Peter Müller, and Andreas Podelski, editors, VSTTE, Lecture Notes in Computer Science. Springer, 2012. [ bib  .pdf ] 
[6] 
JeanChristophe Filliâtre.
Verifying two lines of C with Why3: an exercise in program
verification.
In Verified Software: Theories, Tools and Experiments (VSTTE),
Philadelphia, USA, January 2012.
[ bib 
.pdf ]
This article details the formal verification of a 2line C program that computes the number of solutions to the nqueens problem. The formal proof of (an abstraction of) the C code is performed using the Why3 tool to generate the verification conditions and several provers (AltErgo, CVC3, Coq) to discharge them. The main purpose of this article is to illustrate the use of Why3 in verifying an algorithmically complex program.

[5]  Thorsten Bormer, Marc Brockschmidt, Dino Distefano, Gidon Ernst, JeanChristophe Filliâtre, Radu Grigore, Marieke Huisman, Vladimir Klebanov, Claude Marché, Rosemary Monahan, Wojciech Mostowski, Nadia Polikarpova, Christoph Scheben, Gerhard Schellhorn, Bogdan Tofan, Julian Tschannen, and Mattias Ulbrich. The COST IC0701 verification competition 2011. In Bernhard Beckert, Ferruccio Damiani, and Dilian Gurov, editors, Formal Verification of ObjectOriented Software, Revised Selected Papers Presented at the International Conference, FoVeOOS 2011, Lecture Notes in Computer Science. Springer, 2012. [ bib  .pdf ] 
[4]  Sylvain Conchon, Guillaume Melquiond, Cody Roux, and Mohamed Iguernelala. Builtin treatment of an axiomatic floatingpoint theory for SMT solvers. In Pascal Fontaine and Amit Goel, editors, SMT workshop, Manchester, UK, 2012. http://smt2012.loria.fr/. [ bib ] 
[3]  Claire Dross, Sylvain Conchon, Johannes Kanig, and Andrei Paskevich. Reasoning with triggers. In Pascal Fontaine and Amit Goel, editors, SMT workshop, Manchester, UK, 2012. http://smt2012.loria.fr/. [ bib ] 
[2]  Denis Cousineau, Damien Doligez, Leslie Lamport, Stephan Merz, Daniel Ricketts, and Hernán Vanzetto. TLA+ proofs. In Dimitra Giannakopoulou and Dominique Méry, editors, 18th International Symposium on Formal Methods, volume 7436 of Lecture Notes in Computer Science, pages 147154. Springer, 2012. [ bib ] 
[1]  Denis Cousineau and Olivier Hermant. A semantic proof that reducibility candidates entail cut elimination. In Ashish Tiwari, editor, 23nd International Conference on Rewriting Techniques and Applications, volume 15 of Leibniz International Proceedings in Informatics (LIPIcs), pages 133148, Nagoya, Japan, 2012. Schloss DagstuhlLeibnizZentrum fuer Informatik. [ bib ] 
PhD theses
[1]  Thi Minh Tuyen Nguyen. Taking architecture and compiler into account in formal proofs of numerical programs. Thèse de doctorat, Université ParisSud, June 2012. [ bib  .pdf ] 
Misc.
Reports
[3]  François Bobot, JeanChristophe Filliâtre, Claude Marché, Guillaume Melquiond, and Andrei Paskevich. The Why3 platform, version 0.73. LRI, CNRS & Univ. ParisSud & INRIA Saclay, version 0.73 edition, July 2012. https://gforge.inria.fr/docman/view.php/2990/8052/manual0.73.pdf. [ bib ] 
[2] 
Claire Dross, Sylvain Conchon, Johannes Kanig, and Andrei Paskevich.
Reasoning with triggers.
Research Report RR7986, INRIA, June 2012.
[ bib 
full paper on HAL 
.pdf ]
SMT solvers can decide the satisfiability of ground formulas modulo a combination of builtin theories. Adding a builtin theory to a given SMT solver is a complex and time consuming task that requires internal knowledge of the solver. However, many theories can be easily expressed using firstorder formulas. Unfortunately, since universal quantifiers are not handled in a complete way by SMT solvers, these axiomatics cannot be used as decision procedures. In this paper, we show how to extend a generic SMT solver to accept a custom theory description and behave as a decision procedure for that theory, provided that the described theory is complete and terminating in a precise sense. The description language consists of firstorder axioms with triggers, an instantiation mechanism that is found in many SMT solvers. This mechanism, which usually lacks a clear semantics in existing languages and tools, is rigorously defined here; this definition can be used to prove completeness and termination of the theory. We demonstrate on two examples, how such proofs can be achieved in our formalism. Keywords: Quantifiers, Triggers, SMT Solvers, Theories 
[1]  François Bobot, JeanChristophe Filliâtre, Claude Marché, Guillaume Melquiond, and Andrei Paskevich. The Why3 platform, version 0.72. LRI, CNRS & Univ. ParisSud & INRIA Saclay, version 0.72 edition, May 2012. https://gforge.inria.fr/docman/view.php/2990/7919/manual0.72.pdf. [ bib ] 
Back
Books / Journals / Conferences / PhD theses / Misc. / Reports
This page was generated by bibtex2html.