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
Author only
