[21]

Sylvie Boldo, Catherine Lelay, and Guillaume Melquiond.
Improving real analysis in Coq: a userfriendly 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 289304, Kyoto,
Japan, December 2012.
[ bib 
DOI 
full text on HAL ]

[20]

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 
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 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.

[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, objectoriented 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, 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 
.pdf ]
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.
Keywords: Why3

[17]

David Baelde, Pierre Courtieu, David GrossAmblard, and Christine
PaulinMohring.
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. 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

[16]

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, volume 7358 of Lecture Notes in Computer Science,
Berkeley, California, USA, July 2012. Springer.
[ bib 
full text on HAL ]
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.

[15]

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

[14]

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 
full text on HAL 
.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.

[13]

François Bobot, Sylvain Conchon, Évelyne 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 
full text on HAL ]
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.

[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, volume
7316 of Lecture Notes in Computer Science, pages 238251, Pisa, Italy,
June 2012. Springer.
http://hal.inria.fr/hal00681781/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 firstorder logic. We report on two
case studies demonstrating a significant improvement in the ratio of
obligations that are automatically discharged.

[11]

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.
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.

[10]

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 ]

[9]

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 text on HAL ]

[8]

Johannes Kanig, Edmond Schonberg, and Claire Dross.
HiLite: 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 2734, Boston, USA, 2012. ACM Press.
[ bib ]

[7]

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, pages 133148, Nagoya, Japan,
2012. Schloss DagstuhlLeibnizZentrum fuer Informatik.
[ bib 
DOI 
full text on HAL ]

[6]

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 
full text on HAL ]

[5]

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 ]

[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, pages
1221, Manchester, UK, 2012. LORIA.
[ bib ]

[3]

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, volume 7421 of
Lecture Notes in Computer Science. Springer, 2012.
[ bib 
full text on HAL 
.pdf ]

[2]

JeanChristophe 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, Experiments (4th International
Conference VSTTE), volume 7152 of Lecture Notes in Computer Science,
pages 8397, Philadelphia, USA, January 2012. Springer.
[ 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.
Keywords: Why3

[1]

Paolo Herms, Claude Marché, and Benjamin Monate.
A certified multiprover verification condition generator.
In Rajeev Joshi, Peter Müller, and Andreas Podelski, editors,
Verified Software: Theories, Tools, Experiments (4th International
Conference VSTTE), volume 7152 of Lecture Notes in Computer Science,
pages 217, Philadelphia, USA, January 2012. Springer.
[ bib 
full text on HAL 
.pdf ]
