Program

10:00 - 10:45	Xavier Leroy - Verasco: Formal verification of a C static analyzer based on abstract interpretation
10:50 - 11:35	Wouter Swierstra - Semantics of version control
11:40 - 13:10	Lunch
13:10 - 13:55	Lars Birkedal - Higher-Order Concurrent Separation Logic: Why and How
14:00 - 14:45	Yves Bertot - Structuring mathematical proofs: an example on multivariate polynomials and proofs of transcendence
14:45 - 15:15	Coffee break
15:15 - 16:00	Robbert Krebbers - Formalization of C: What we have learned and beyond

Abstracts

Verasco: Formal verification of a C static analyzer based on abstract interpretation

Xavier Leroy, Inria Paris-Rocquencourt (download slides)

The ongoing Verasco project aims at developing and verifying (in Coq) a static analyzer for the CompCert subset of the C language (minus recursion and dynamic allocation). The goal of the analyzer is to establish the absence of run-time errors (e.g. out-of-bound array accesses) in the analyzed C code. It follows the general approach of abstract interpretation, whereas analyzing a program is viewed as executing it in a nonstandard semantics that builds on a combination of abstract domains capturing program properties of interest, e.g. variation intervals for numerical variables, linear inequalities between variables, or nonaliasing properties of pointers. The formal verification of the analyzer aims at proving that it is sound with respect to the dynamic semantics of the language: if the analyzer reports no alarms, the program executes without run-time errors. This formal verification raises a number of interesting issues, ranging from the conceptual (what is a good specification for an abstract domain? how to relate program executions in the concrete and in the abstract?) to the practical (proving the nontrivial algorithms and data structures involved in numerical abstract domains).

(Joint work with: Jacques-Henri Jourdan, Vincent Laporte, Sandrine Blazy, David Pichardie)

Semantics of version control

Wouter Swierstra, Utrecht University (download slides)

As software becomes increasingly complex, software configuration management is becoming ever more important. This talk shows how logics for reasoning about mutable state, such as separation logic, can also be used to give semantics for version control systems. By applying these ideas from the programming language research community, developers may reason formally about the broader software development process.

Higher-Order Concurrent Separation Logic: Why and How

Lars Birkedal, Aarhus University (download slides)

I will give an overview of some of my groups work on developing program logics for modular reasoning about partial correctness of higher-order, concurrent, imperative programs.

Structuring mathematical proofs: an example on multivariate polynomials and proofs of transcendence

Yves Bertot, Inria Sophia Antipolis (download slides)

Proofs in mathematics stress theorem proving tools in ways that are different from proofs of computer software and systems. In particular, I believe that proofs in mathematics require more facilities for changing points of views about looking at the same object. This is particularly visible when considering proofs at the interface of two domains of mathematics that contain their own culture of mathematical tricks. Our own experiments revolve around questions at the interface of analysis and algebra: proofs of transcendence. The first proof of this family was performed in 2011 in Hol-Light by J. Bingham. In 2014, we decided to understand what was needed for a proof that pi is transcendental. The extra ingredient is multivariate polynomials, especially symmetric polynomials and the theorem known as the fundamental theorem of symmetric polynomials, which is actually an algorithm. We completed the development, just achieving the first formalized proof of transcendence for pi. Beyond the mathematical result, we learn lessons that are important to help structuring large development and re-use mathematics formalized over the internet.

(Joint work with Sophie Bernard, Laurence Rideau, and Pierre-Yves Strub)

Formalization of C: What we have learned and beyond

Robbert Krebbers, Aarhus University (download slides)

In this talk, I will present an overview of the results contained in my thesis The C standard formalized in Coq, which concerns a formalization of a large part of the C11 standard in the Coq proof standard. In particular, I will discuss our experiences with the informal process of programming language standardization and how that interacted with the development of a formal version of the said programming language. Apart from that, I will discuss directions for future research.