1

A Modular Way to Reason About Iteration

Jean-Christophe Filliâtre,
Mário Pereira

June 2016
NFM 2016: Proceedings of the 8th International Symposium on NASA Formal Methods - Volume 9690

**Publisher:** Springer-Verlag New York, Inc.

In this paper we present an approach to specify programs performing iterations. The idea is to specify iteration in terms of the finite sequence of the elements enumerated so far, and only those. In particular, we are able to deal with non-deterministic and possibly infinite iteration. We show how to ...

2

The spirit of ghost code

Jean-Christophe Filliâtre,
Léon Gondelman,
Andrei Paskevich

June 2016
Formal Methods in System Design: Volume 48 Issue 3, June 2016

**Publisher:** Kluwer Academic Publishers

In the context of deductive program verification, ghost code is a part of the program that is added for the purpose of specification. Ghost code must not interfere with regular code, in the sense that it can be erased without observable difference in the program outcome. In particular, ghost data ...

**Keywords**:
Why3, Ghost code, Deductive software verification

3

Let's verify this with Why3

François Bobot,
Jean-Christophe Filliâtre,
Claude Marché,
Andrei Paskevich

November 2015
International Journal on Software Tools for Technology Transfer (STTT): Volume 17 Issue 6, November 2015

**Publisher:** Springer-Verlag

We present solutions to the three challenges of the VerifyThis competition held at the 18th FM symposium in August 2012. These solutions use the Why3 environment for deductive program verification.

**Keywords**:
Automated theorem proving, Case study, Deductive verification, Formal specification

4

How to Avoid Proving the Absence of Integer Overflows

Martin Clochard,
Jean-Christophe Filliâtre,
Andrei Paskevich

July 2015
VSTTE 2015: Revised Selected Papers of the 7th International Conference on Verified Software: Theories, Tools, and Experiments - Volume 9593

**Publisher:** Springer-Verlag New York, Inc.

When proving safety of programs, we must show, in particular, the absence of integer overflows. Unfortunately, there are lots of situations where performing such a proof is extremely difficult, because the appropriate restrictions on function arguments are invasive and may be hard to infer. Yet, in certain cases, we can ...

5

The Spirit of Ghost Code

Jean-Christophe Filliâtre,
Léon Gondelman,
Andrei Paskevich

July 2014
Proceedings of the 16th International Conference on Computer Aided Verification - Volume 8559

**Publisher:** Springer-Verlag New York, Inc.

In the context of deductive program verification, ghost code is part of the program that is added for the purpose of specification. Ghost code must not interfere with regular code, in the sense that it can be erased without observable difference in the program outcome. In particular, ghost data cannot ...

6

One logic to use them all

Jean-Christophe Filliâtre

June 2013
CADE'13: Proceedings of the 24th international conference on Automated Deduction

**Publisher:** Springer-Verlag

Deductive program verification is making fast progress these days. One of the reasons is a tremendous improvement of theorem provers in the last two decades. This includes various kinds of automated theorem provers, such as ATP systems and SMT solvers, and interactive proof assistants. Yet most tools for program verification ...

7

François Bobot,
Jean-Christophe Filliâtre,
Claude Marché,
Guillaume Melquiond,
Andrei Paskevich

May 2013
VSTTE 2013: Revised Selected Papers of the 5th International Conference on Verified Software: Theories, Tools, Experiments - Volume 8164

**Publisher:** Springer-Verlag New York, Inc.

In the context of deductive program verification, both the specification and the code evolve as the verification process carries on. For instance, a loop invariant gets strengthened when additional properties are added to the specification. This causes all the related proof obligations to change; thus previous user verifications become invalid. ...

8

Wave Equation Numerical Resolution: A Comprehensive Mechanized Proof of a C Program

Sylvie Boldo,
François Clément,
Jean-Christophe Filliâtre,
Micaela Mayero,
Guillaume Melquiond,
Pierre Weis

April 2013
Journal of Automated Reasoning: Volume 50 Issue 4, April 2013

**Publisher:** Springer-Verlag New York, Inc.

We formally prove correct a C program that implements a numerical scheme for the resolution of the one-dimensional acoustic wave equation. Such an implementation introduces errors at several levels: the numerical scheme introduces method errors, and floating-point computations lead to round-off errors. We annotate this C program to specify both ...

**Keywords**:
Acoustic wave equation, Coq formal proof, Convergence of numerical scheme, Formal proof of numerical program, Partial differential equation, Proof of C program, Rounding error analysis

9

Why3: where programs meet provers

Jean-Christophe Filliâtre,
Andrei Paskevich

March 2013
ESOP'13: Proceedings of the 22nd European conference on Programming Languages and Systems

**Publisher:** Springer-Verlag

We present Why3, a tool for deductive program verification, and WhyML, its programming and specification language. WhyML is a first-order language with polymorphic types, pattern matching, and inductive predicates. Programs can make use of record types with mutable fields, type invariants, and ghost code. Verification conditions are discharged by Why3 ...

10

Separation predicates: a taste of separation logic in first-order logic

François Bobot,
Jean-Christophe Filliâtre

November 2012
ICFEM'12: Proceedings of the 14th international conference on Formal Engineering Methods: formal methods and software engineering

**Publisher:** Springer-Verlag

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

11

Discharging proof obligations from atelier b using multiple automated provers

David Mentré,
Claude Marché,
Jean-Christophe Filliâtre,
Masashi Asuka

June 2012
ABZ'12: Proceedings of the Third international conference on Abstract State Machines, Alloy, B, VDM, and Z

**Publisher:** Springer-Verlag

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

Verifying two lines of c with why3: an exercise in program verification

Jean-Christophe Filliâtre

January 2012
VSTTE'12: Proceedings of the 4th international conference on Verified Software: theories, tools, experiments

**Publisher:** Springer-Verlag

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

13

The COST IC0701 verification competition 2011

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,
Mattias Ulbrich

October 2011
FoVeOOS'11: Proceedings of the 2011 international conference on Formal Verification of Object-Oriented Software

**Publisher:** Springer-Verlag

This paper reports on the experiences with the program verification competition held during the FoVeOOS conference in October 2011. There were 6 teams participating in this competition. We discuss the three different challenges that were posed and the solutions developed by the teams. We conclude with a discussion about the ...

14

Jean-Christophe Filliâtre

October 2011
International Journal on Software Tools for Technology Transfer (STTT) - VSTTE 2009: Volume 13 Issue 5, October 2011

**Publisher:** Springer-Verlag

Deductive software verification, also known as program proving, expresses the correctness of a program as a set of mathematical statements, called verification conditions. They are then discharged using either automated or interactive theorem provers. We briefly review this research area, with an emphasis on tools.

**Keywords**:
Automated theorem prover, Hoare logic, Proof assistant, Specification language

15

Correct code containing containers

Claire Dross,
Jean-Christophe Filliâtre,
Yannick Moy

June 2011
TAP'11: Proceedings of the 5th international conference on Tests and proofs

**Publisher:** Springer-Verlag

For critical software development, containers such as lists, vectors, sets or maps are an attractive alternative to ad-hoc data structures based on pointers. As standards like DO-178C put formal verification and testing on an equal footing, it is important to give users the ability to apply both to the verification ...

**Keywords**:
API usage verification, axiomatization, verification by contracts, SMT, automatic provers, iterators, annotations, containers

16

Functory: a distributed computing library for objective caml

Jean-Christophe Filliâtre,
K. Kalyanasundaram

May 2011
TFP'11: Proceedings of the 12th international conference on Trends in Functional Programming

**Publisher:** Springer-Verlag

We present Functory, a distributed computing library for Objective Caml. The main features of this library include (1) a polymorphic API, (2) several implementations to adapt to different deployment scenarios such as sequential, multi-core or network, and (3) a reliable fault-tolerance mechanism. This paper describes the motivation behind this work, ...

17

Formal proof of a wave equation resolution scheme: the method error

Sylvie Boldo,
François Clément,
Jean-Christophe Filliâtre,
Micaela Mayero,
Guillaume Melquiond,
Pierre Weis

July 2010
ITP'10: Proceedings of the First international conference on Interactive Theorem Proving

**Publisher:** Springer-Verlag

Popular finite difference numerical schemes for the resolution of the one-dimensional acoustic wave equation are well-known to be convergent. We present a comprehensive formalization of the simplest scheme and formally prove its convergence in Coq. The main difficulties lie in the proper definition of asymptotic behaviors and the implicit way ...

**Keywords**:
numerical scheme, partial differential equation, acoustic wave equation, coq formal proofs

18

Who: a verifier for effectful higher-order programs

Johannes Kanig,
Jean-Christophe Filliâtre

August 2009
ML '09: Proceedings of the 2009 ACM SIGPLAN workshop on ML

**Publisher:** ACM

**Bibliometrics**:

Citation Count: 7

Downloads (6 Weeks): 0, Downloads (12 Months): 4, Downloads (Overall): 67

Full text available:

PDF

We present Who, a tool for verifying effectful higher-order functions. It features Effect polymorphism , higher-order logic and the possibility to reason about state in the logic, which enable highly modular specifications of generic code. Several small examples and a larger case study demonstrate its usefulness. The Who tool is ...

**Keywords**:
hoare logic, higher-order programs

19

Combining Coq and Gappa for Certifying Floating-Point Programs

Sylvie Boldo,
Jean-Christophe Filliâtre,
Guillaume Melquiond

July 2009
Calculemus '09/MKM '09: Proceedings of the 16th Symposium, 8th International Conference. Held as Part of CICM '09 on Intelligent Computer Mathematics

**Publisher:** Springer-Verlag

Formal verification of numerical programs is notoriously difficult. On the one hand, there exist automatic tools specialized in floating-point arithmetic, such as Gappa, but they target very restrictive logics. On the other hand, there are interactive theorem provers based on the LCF approach, such as Coq, that handle a general-purpose ...

20

A functional implementation of the garsia--wachs algorithm: (functional pearl)

Jean-Christophe Filliatre

September 2008
ML '08: Proceedings of the 2008 ACM SIGPLAN workshop on ML

**Publisher:** ACM

**Bibliometrics**:

Citation Count: 0

Downloads (6 Weeks): 3, Downloads (12 Months): 8, Downloads (Overall): 111

Full text available:

Pdf

This functional pearl proposes an ML implementation of the Garsia-Wachs algorithm. This somewhat obscure algorithm builds a binary tree with minimum weighted path length from weighted leaf nodes with given inorder. Our solution exhibits the usual benefits of functional programming (use of immutable data structures, pattern-matching, polymorphism) and nicely compares ...

**Keywords**:
zipper, applicative programming, garsia-wachs algorithm, optimum binary trees