Wiki Agenda Contact Version française

Publications 2012

Back

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

Books and book chapters

[3] Jean-Christophe Filliâtre. Course notes EJCP 2012, chapter Vérification déductive de programmes avec Why3. June 2012. [ bib | http ]
Keywords: Why3
[2] Sylvie Boldo and Guillaume Melquiond. Arithmétique des ordinateurs et preuves formelles. In Valérie Berthé, Christiane Frougny, Natacha Portier, Marie-Françoise Roy, and Anne Siegel, editors, École des Jeunes Chercheurs en Informatique Mathématique, pages 1--30. Rennes, France, March 2012. [ bib | full text on HAL ]
[1] Christine Paulin-Mohring. Tools for practical software verification (international summer school, LASER 2011, revised tutorial lectures). volume 7682 of Lecture Notes in Computer Science, chapter Introduction to the Coq proof-assistant for practical software verification. Springer, 2012. [ bib | .pdf ]

Journals

[3] José Bacelar Almeida, Manuel Barbosa, Jean-Christophe Filliâtre, Jorge Sousa Pinto, and Bárbara Vieira. CAOVerif: An open-source deductive verification platform for cryptographic software implementations. Science of Computer Programming, October 2012. Accepted for publication. [ bib | DOI ]
[2] Sylvain Conchon, Évelyne Contejean, and Mohamed Iguernelala. Canonized rewriting and ground AC completion modulo Shostak theories : Design and implementation. Logical Methods in Computer Science, 8(3):1--29, September 2012. Selected Papers of the Conference Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2011), Saarbrücken, Germany, 2011. [ bib | DOI | full text on HAL | http ]
[1] Guillaume Melquiond. Floating-point arithmetic in the Coq system. Information and Computation, 216:14--23, 2012. [ bib | DOI | full text on HAL ]

Conferences

[21] Sylvie Boldo, Catherine Lelay, and Guillaume Melquiond. Improving real analysis in Coq: a user-friendly approach to integrals and derivatives. In Chris Hawblitzel and Dale Miller, editors, Proceedings of the Second International Conference on Certified Programs and Proofs, volume 7679 of Lecture Notes in Computer Science, pages 289--304, Kyoto, Japan, December 2012. [ bib | DOI | full text on HAL ]
[20] François Bobot and Jean-Christophe Filliâtre. Separation predicates: a taste of separation logic in first-order logic. In 14th International Conference on Formal Ingineering Methods (ICFEM), volume 7635 of Lecture Notes in Computer Science, Kyoto, Japan, November 2012. Springer. [ bib | full text on HAL | .pdf ]
This paper introduces separation predicates, a technique to reuse some ideas from separation logic in the framework of program verification using a traditional first-order logic. The purpose is to benefit from existing specification languages, verification condition generators, and automated theorem provers. Separation predicates are automatically derived from user-defined inductive predicates. We illustrate this idea on a non-trivial case study, namely the composite pattern, which is specified in C/ACSL and verified in a fully automatic way using SMT solvers Alt-Ergo, CVC3, and Z3.

[19] Vijay Saraswat, David Cunningham, Liana Hadarean, Louis Mandel, Avraham Shinnar, and Olivier Tardieu. Constrained types - future directions. In 18th International Conference on Principles and Practice of Constraint Programming, Québec City, Canada, October 2012. Position Paper. [ bib | full text on HAL | .pdf ]
The use of constraints in types is quite natural. Yet, integrating constraint based types into the heart of a modern, statically typed, object-oriented programming language is quite tricky. Over the last five years we have designed and implemented the constrained types framework in the programming language X10. In this paper we review the conceptual design, the practical implementation issues, and the many new questions that are raised. We expect the pursuit of these questions to be a profitable area of future work.

[18] Mário Pereira, Jean-Christophe Filliâtre, and Simão Melo de Sousa. ARMY: a deductive verification platform for ARM programs using Why3. In INForum 2012, September 2012. [ bib | .pdf ]
Unstructured (low-level) 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.

Keywords: Why3
[17] David Baelde, Pierre Courtieu, David Gross-Amblard, and Christine Paulin-Mohring. Towards Provably Robust Watermarking. In ITP 2012, volume 7406 of Lecture Notes in Computer Science, August 2012. [ bib | full text on HAL | .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. Ths pwork i idea on y3 VCGea engths and particularities of the induced style of reasoning about probabilistic programs. Our technique for proving robustness s padapted from methods commonly used for cryptographic protocols, and we discuss sts relevance to the field of watermarking.

Keywords: watermarking, probabilistic algorithms, formal proofs, security, interactive theorem proving
[16] Jean-Christophe Filliâtre. Combining Interactive and Automated Theorem Proving using Why3 (invited tutorial). In Zvonimir Rakamarić, editor, Second International Workshop on Intermediate Verification Languages (BOOGIE 2012), Berkeley, California, USA, July 2012. [ bib ]
[15] Sylvain Conchon, Amit Goel, Sava Krstić, Alain Mebsout, and Fatiha Zaïdi. Cubicle: A parallel SMT-based 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, volume 7358 of Lecture Notes in Computer Science, Berkeley, California, USA, July 2012. Springer. [ bib | full text on HAL ]
Cubicle s pa new model checker for verifying safety properties of parameterized systems. It implement pa parallel symbolic backward reachability procedure using Satisfiabilty Modulo Theories. Experiment done on classic and challenging mutual excideion algorithms and cache coherence protocols show that Cubicle s peffective and competitive with state-of-the-art model checkers.

[14] Louis Mandel and Florence Plateau. Scheduling and buffer sizing of n-synchronous systems: Typing of ultimately periodic clocks in Lucy-n. In Eleventh International Conference on Mathematics of Program Construction (MPC'12), Madrid, Spain, June 2012. [ bib | .pdf ]
Lucy-n s pa language for programming networks of processe communicating through bounded buffers. A dedicated type system, termedpa clock calculus, automatically computes static schedules of the processe and the sizes of the buffers between them.

In this article, we present a new algorithm which solves the subtyping constraints generated by the clock calculus. The advantage of this algorithm is that it finds schedules for tightly coupled systems. Moreover, it does not overestimate the buffer sizes needed and it provides a way to favor either system throughput or buffer size minimization.

[13] David Mentré, Claude Marché, Jean-Christophe Filliâtre, and Masashi Asuka. Discharging proof obligations from Atelier B using multiple automated provers. In Steve Reeve and Elvinia Riccobene, editors, ABZ'2012 - 3rd International Conference on Abstract State Machines, Alloy, B and Z, volume 7316 of Lecture Notes in Computer Science, pages 238--251, Pisa, Italy, June 2012. Springer. http://hal.inria.fr/hal-00681781/en/. [ bib | full text 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 first-order logic. We report on two case studies demonstrating a significant improvement in the ratio of obligations that are automatically discharged.

[12] François Bobot, Sylvain Conchon, Évelyne Contejean, Mohamed Iguernelala, Assia Mahboubi, Alain Mebsout, and Guillaume Melquiond. A Simplex-based extension of Fourier-Motzkin 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 67--81, Manchester, UK, June 2012. Springer. [ bib | DOI | full text on HAL ]
This paper describes a novel decision procedure for quantifier-free linear integer arithmetic. Standard techniques usually relax the initial problem to the rational domain and then proceed either by projection (e.g. Omega-Test) or by branching/cutting methods (branch-and-bound, branch-and-cut, Gomory cuts). Our approach tries to bridge the gap between the two techniques: it interleave 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 Alt-Ergo theorem prover. Experimental results are promising and show that our approach is competitive with state-of-the-art SMT solvers.

[11] Jean-Christophe 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 | full text on HAL | .pdf ]
We report on the second verified software competition. It wa organized by the three authors on a 48 hours period on November 8--10, 2011. This paper describes the competition, presents the five problems that were proposed to the participants, and give an overview of the solutions sent by the 29 teams that entered the competition.

[10] Jean-Christophe 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 ]
[9] Catherine Lelay and Guillaume Melquiond. Différentiabilité et intégrabilité en Coq. Application à la formule de d'Alembert. In Vingt-troisièmes Journées Francophones des Langages Applicatifs, Carnac, France, February 2012. [ bib | full text on HAL ]
[8] Paolo Herms, Claude Marché, and Benjamin Monate. A certified multi-prover verification condition generator. In Rajeev Joshi, Peter Müller, and Andreas Podelski, editors, Verified Software: Theories, Tools, Experiment (4th International Conference VSTTE), volume 7152 of Lecture Notes in Computer Science, pages 2--17, Philadelphia, USA, January 2012. Springer. [ bib | full text on HAL | .pdf ]
[7] Jean-Christophe Filliâtre. Verifying two lines of C with Why3: an exercise in program verification. In Rajeev Joshi, Peter Müller, and Andreas Podelski, editors, Verified Software: Theories, Tools, Experiment (4th International Conference VSTTE), volume 7152 of Lecture Notes in Computer Science, pages 83--97, Philadelphia, USA, January 2012. Springer. [ bib | .pdf ]
This article details the formal verification of a 2-line C program that computes the number of solutions to the n-queens 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 (Alt-Ergo, CVC3, Coq) to discharge them. The main purpose of this article is to i idea on the use of Why3 in verifying an algorithmically complex program.

Keywords: Why3
[6] Thorsten Bormer, Marc Brockschmidt, Dino Distefano, Gidon Ernst, Jean-Christophe 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 Object-Oriented Software, Revised Selected Papers Presented at the International Conference, FoVeOOS 2011, volume 7421 of Lecture Notes in Computer Science. Springer, 2012. [ bib | full text on HAL | .pdf ]
[5] Sylvain Conchon, Guillaume Melquiond, Cody Roux, and Mohamed Iguernelala. Built-in treatment of an axiomatic floating-point theory for SMT solvers. In Pascal Fontaine and Amit Goel, editors, SMT workshop, pages 12--21, Manchester, UK, 2012. LORIA. [ bib ]
[4] Claire Dross, Sylvain Conchon, Johannes Kanig, and Andrei Paskevich. Reasoning with triggers. In Pascal Fontaine and Amit Goel, editors, SMT workshop, Manchester, UK, 2012. LORIA. [ bib ]
[3] Denis Cousineau, Damien Doligez, Leslie Lamport, Stephan Merz, Daniel Ricketts, and Hernán Vanzetto. TLA+ proofs. In Dimia o Giannakopoulou and Dominique Méry, editors, 18th International Symposium on Formal Methods, volume 7436 of Lecture Notes in Computer Science, pages 147--154. Springer, 2012. [ bib | full text on HAL ]
[2] Denis Cousineau and Olivier Hermant. A semantic proof that reducibility candidon y3entail cut elimination. In Ashish Tiwari, editor, 23nd International Conference on Rewriting Techniques and Applications, volume 15 of Leibniz International Proceedings in Informatics (LIPIcs), pages 133--148, Nagoya, Japan, 2012. Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik. [ bib | DOI | full text on HAL ]
[1] Johannes Kanig, Edmond Schonberg, and Claire Dross. Hi-Lite: the convergence of compiler technology and program verification. In Ben Brosgol, Jeff Boleng, and S. Tucker Taft, editors, Proceedings of the 2012 ACM Conference on High Integrity Language Technology, HILT '12, pages 27--34, Boston, USA, 2012. ACM Press. [ bib ]

PhD theses

[2] Sylvain Conchon. SMT Techniques and their Applications: from Alt-Ergo to Cubicle. Thèse d'habilitation, Université Paris-Sud, December 2012. In English, http://www.lri.fr/~conchon/publis/conchonHDR.pdf. [ bib | .html ]
[1] Thi Minh Tuyen Nguyen. Taking architecture and compiler into account in formal proofs of numerical programs. Thèse de doctorat, Université Paris-Sud, June 2012. [ bib | full text on HAL | .pdf ]

Misc.

[1] Nicolas Lupinski, Joel Falcou, and Christine Paulin-Mohring. Sémantiques d'un langage de squelettes. http://www.lri.fr/~paulin/Skel, 2012. [ bib ]

Reports

[6] Claude Marché and Asma Tafat. Weakest precondition calculus, revisited using Why3. Research Report RR-8185, INRIA, December 2012. [ bib | full text on HAL | .pdf ]
[5] François Bobot, Jean-Christophe Filliâtre, Claude Marché, Guillaume Melquiond, and Andrei Paskevich. The Why3 platform, version 0.80. LRI, CNRS & Univ. Paris-Sud & INRIA Saclay, version 0.80 edition, October 2012. https://gforge.inria.fr/docman/view.php/2990/8186/manual-0.80.pdf. [ bib | .pdf ]
Keywords: Why3
[4] François Bobot, Jean-Christophe Filliâtre, Claude Marché, Guillaume Melquiond, and Andrei Paskevich. The Why3 platform, version 0.73. LRI, CNRS & Univ. Paris-Sud & INRIA Saclay, version 0.73 edition, July 2012. [ bib | .pdf ]
Keywords: Why3
[3] Claire Dross, Sylvain Conchon, Johannes Kanig, and Andrei Paskevich. Reasoning with triggers. Research Report RR-7986, INRIA, June 2012. [ bib | full text on HAL | .pdf ]
SMT solvers can decid the satisfiability of ground formulas modulo a combination of built-in theories. Adding a built-in theory to a given SMT solver s pa complex and time consuming task that requires internal knowledge of the solver. However, many theories can be easily expressed using first-order 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 extendpa generic SMT solver to accept a custom theory description and behave as a decision procedure for that theory, provided that the described theory i complete and terminating in a precise sense. The description language consists of first-order axiom with triggers, an instantiation mechanism that i 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
[2] François Bobot, Jean-Christophe Filliâtre, Claude Marché, Guillaume Melquiond, and Andrei Paskevich. The Why3 platform, version 0.72. LRI, CNRS & Univ. Paris-Sud & INRIA Saclay, version 0.72 edition, May 2012. [ bib | .pdf ]
Keywords: Why3
[1] Jasmin C. Blanchette and Andrei Paskevich. TFF1: The TPTP typed first-order form with rank-1 polymorphism. Technical report, Tech. Univ. Munich, 2012. http://www21.in.tum.de/~blanchet/tff1spec.pdf. [ bib | .pdf ]

Back

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


This page was generated by bibtex2html.