Marelle Bibliography

Termination of recursive functions is an important property in proof assistants based on dependent type theories; it implies consistency and decidability of type checking. Type-based termination is a mechanism for ensuring termination that uses types annotated with size information to check that recursive calls are performed on smaller arguments. Our long-term goal is to extend the Calculus of Inductive Constructions with a type-based termination mechanism and prove its logical consistency. In this paper, we present an extension of the Calculus of Constructions (including universes and impredicativity) with sized natural numbers, and prove strong normalization and logical consistency. Moreover, the proof can be easily adapted to include other inductive types.

We discuss a formal development for the certification of Newton's method. We address several issues encountered in the formal study of numerical algorithms: developing the necessary libraries for our proofs, adapting paper proofs to suite the features of a proof assistant, and designing new proofs based on the existing ones to deal with optimizations of the method. We start from Kantorovitch's theorem that states the convergence of Newton's method in the case of a system of equations. To formalize this proof inside the proof assistant Coq we first need to code the necessary concepts from multivariate analysis. We also prove that rounding at each step in Newton's method still yields a convergent process with an accurate correlation between the precision of the input and that of the result. An algorithm including rounding is a more accurate model for computations with Newton's method in practice.

Keywords: proof assistants ; formalization of mathematics ; multivariate analysis ; Kantorovitch's theorem ; Newton's method with rounding

First, we develop verification rules in separation logic for primi tives concerning multithreading: the primitives fork and join that control how threads start and how threads wait, and the primitive for reentrant locks (locks that can be acquired and released more than once) that are used in Java.

Second, we develop three analyses that use separation logic. The first analysis permits to specify sequences of method calls and to verify that they are correct w.r.t. method contracts. The second analysis presents a fast algorithm to disprove entailment between separation logic formulae. The third analysis shows how to parallelize a nd optimize programs by rewriting their proofs.

We show how, given a program and its separation logic proof, one can parallelize and optimize this program and transform its pr oof simultaneously to obtain a proven parallelized and optimized program. To achieve this goal, we present new proof rules for generating pr oof trees and a rewrite system on proof trees.

We describe an algorithm to disprove entailment between separation logic formulas. We abstract models of formulas by their size and check whether two formulas have models whose sizes are compatible. Given two formulas A and B that do not have compatible models, we can conclude that A does not entail B. We provide two different abstractions (of different precision) of models. Our algorithm is of interest wherever entailment checking is performed (such as in program verifiers).

In the Design By Contract (DBC) approach, programmers specify methods with pre and postconditions (also called contracts). Earlier work added protocols to the DBC approach to describe allowed method call sequences for classes. We extend this work to We present the semantical foundations of our extension. We describe a new technique to check that method contracts are correct w.r.t. to protocols. We show how to generate programs that must be proven to show that method contracts are correct w.r.t. to protocols. Because little support currently exists to help writing method contracts, our technique helps programmers to check their contracts early in the development process.

We describe the formal verification of two theorems of theoretical biology. These theorems concern genetic regulatory networks: they give, in a discrete modeling framework, relations between the topology and the dynamics of these biological networks. In the considered discrete modeling framework, the dynamics is described by a transition graph, where vertices are vectors indicating the expression level of each gene, and where edges represent the evolution of these expression levels. The topology is also described by a graph, called interaction graph, where vertices are genes and where edges correspond to influences between genes. The two results we formalize show that circuits of some kind must be present in the interaction graph if some behaviors are possible in the transition graph. This work was performed with the ssreflect extension of the Coq system.

Keywords: Formalization of Algebra, Coercive subtyping, Type inference, Coq, SSReflect

We discuss usage protocols for iterator objects that prevent concurrent modifications of the underlying collection while iterators are in progress. We formalize these protocols in Java-like object interfaces, enriched with separation logic contracts. We present examples of iterator clients and proofs that they adhere to the iterator protocol, as well as examples of iterator implementations and proofs that they implement the iterator interface.

This article describes the formal verification of a compilation algorithm that transforms parallel moves (parallel assignments between variables) into a semantically-equivalent sequence of elementary moves. Two different specifications of the algorithm are given: an inductive specification and a functional one, each with its correctness proofs. A functional program can then be extracted and integrated in the Compcert verified compiler.