ITP on Sunday, July 11th

09:00‑10:00 Session 1
Chair: Matt Kaufmann [NOTE: A copy of the full program, with links to slides as well as to the agenda and minutes of the business meeting, may be found HERE.]
Location: AT LT5
09:00 Norbert Schirmer and Ernie Cohen
From Total Store Order to Sequential Consistency: A Practical Reduction Theorem

When verifying a concurrent program, it is usual to assume sequentially consistent memory. However, most modern multiprocessors buffer their stores, providing native sequential consistency only at a substantial performance penalty. To regain sequential consistency, a programmer has to follow an appropriate programming discipline. However, existing na\"ive disciplines, such as protecting all shared accesses with locks to avoid data races, or flushing store buffers according to a protocol that allows arbitrary data races, are not flexible enough for building high-performance multiprocessor software.

We present a new discipline for concurrent programming under TSO (total store order, with store buffer forwarding). Instead of using concurrency primitives, such as locks, it is based on maintaining ownership information in ghost state, allowing the discipline to be expressed as a state invariant and verified through conventional program reasoning. We prove in Isabelle/HOL that if every execution of a program in a system without store buffers follows the discipline, then every execution of the program with store buffers is sequentially consistent.

09:30 Freek Verbeek and Julien Schmaltz
Proof Pearl: A formal proof of Duato's condition for deadlock-free adaptive networks

Deadlocks occur in interconnection networks as messages compete for free channels or empty buffers. Deadlocks are often associated to a circular wait between processes and resources. In the context of networks, Duato proved that for adaptive routing networks a cyclic dependency is not sufficient to create a deadlock. He proposed deadlock-free routing techniques allowing cyclic dependencies between channels or buffers. His work was a breakthrough. It was also counterintuitive and only a complex mathematical proof could convince his peers about the soundness of his theory. We define a necessary and sufficient condition that captures Duato's intuition but that is more intuitive and leads to a simpler proof. However, our condition is logically equivalent to Duato's one. We used the ACL2 theorem proving system to formalize our condition and its proof. In particular, we used two features of ACL2, namely the encapsulation principle and quantifiers, to perform an elegant formalization based on second order functions.

10:30‑12:30 Session 2
Chair: David Pichardie
Location: AT LT5
10:30 Ramana Kumar and Michael Norrish
(Nominal) Unification by Recursive Descent with Triangular Substitutions

We mechanise termination and correctness for two unification algorithms, written in a recursive descent style. One computes unifiers for first order terms, the other for nominal terms (terms including $\alpha$-equivalent binding structure). Both algorithms work with triangular substitutions in accumulator-passing style: taking a substitution as input, and returning an extension of that substitution on success.

This style of algorithm has performance benefits and has not been mechanised previously. The algorithms use nested recursion so the termination proofs are non-trivial; the termination relation is also slightly different from usual.

11:00 Jean-François Dufourd and Yves Bertot
Formal study of plane Delaunay triangulation

This article presents the formal proof of correctness for a plane Delaunay triangulation algorithm. It consists in repeating a sequence of edge flippings from an initial triangulation until the Delaunay property is achieved. To describe triangulations, we rely on a combinatorial hypermap specification framework we have been developing for years. We embed hypermaps in the plane by attaching coordinates to elements in a consistent way. We then describe what are legal and illegal Delaunay edges and a flipping operation which we show preserves hypermap, triangulation, and embedding invariants. To prove the termination of the algorithm, we use a generic approach expressing that any non-cyclic relation is well-founded when working on a finite set.

11:30 Sylvie Boldo, François Clément, Jean-Christophe Filliatre, Micaela Mayero, Guillaume Melquiond and Pierre Weis
Formal Proof of a Wave Equation Resolution Scheme: the Method Error

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 one and formally prove its convergence in Coq. The main difficulties lie in the proper definition of asymptotic behaviors and the implicit way they are handled in the mathematical pen-and-paper proofs. To our knowledge, this is the first time such kind of mathematical proof is machine-checked.

12:00 Anthony Fox and Magnus Myreen
A Trustworthy Monadic Formalization of the ARMv7 Instruction Set Architecture

This paper presents a new HOL4 formalization of the current ARM instruction set architecture, ARMv7. This is a modern RISC architecture with many advanced features. The formalization is detailed and extensive. Considerable tool support has been developed, with the goal of making the model accessible and easy to work with. The model, and supporting tools, are publicly available and we wish to encourage others to make use of this resource. This paper explains our monadic specification approach and gives some details of the endeavours that have been made to ensure that the sizeable model is valid and trustworthy. A novel and efficient testing approach has been developed, based on automated forward proof and communication with ARM development boards.

14:00‑15:00 FLoC Plenary Talks: tribute to Amir and Robin
Chair: Moshe Vardi
Location: George Square Lecture Theatre
14:00 David Harel (Weizmann Institute of Science)
Amir Pnueli: A Gentle Giant, Lord of the Phi's and the Psi's.
14:30 Gordon Plotkin (University of Edinburgh)
Robin Milner, a Craftsman of Tools for the Mind.
15:30‑17:00 Session 3
Chair: Cesar Munoz
Location: AT LT5
15:30 Brian Huffman and Christian Urban
Proof Pearl: A New Foundation for Nominal Isabelle

Pitts et al introduced a beautiful theory about names and binding based on the notions of permutation and support. The engineering challenge is to smoothly adapt this theory to a theorem prover environment, in our case Isabelle/HOL. An earlier approach adapting this work was based on a concrete representation of permutations as list of pairs of atoms, which in comparison to the work presented here caused inconveniences for the user and made proofs and ML-code unnecessarily complicated. In this paper we use a more abstract representation of permutations based on functions. As a result, we can iron out the inconveniences, considerably simplify proofs and also drastically reduce the amount of custom ML-code. We end up with a pleasing and formalised theory of permutations and support, on which we can built an improved version of Nominal Isabelle.

16:00 John Cowles and Ruben Gamboa
Using a First Order Logic to Verify That Some Set of Reals Has No Lebesgue Measure

This paper presents a formal proof of Vitali's theorem that not all sets of real numbers can have a Lebesgue measure, where the notion of "measure" is given very general and reasonable constraints. A careful examination of Vitali's proof identifies a set of axioms that are sufficient to prove Vitali's theorem, including a first-order theory of the reals as a complete, ordered field, "enough" sets of reals, and the axiom of choice. The main contribution of this paper is a positive demonstration that the axioms and inference rules in ACL2(r), a variant of ACL2 with support for nonstandard analysis, are sufficient to carry out this proof.

16:30 Tarek Mhamdi, Osman Hasan and Sofiene Tahar
On the Formalization of the Lebesgue Integration Theory in HOL

Lebesgue integration is a fundamental concept in many mathematical theories, such as real analysis, probability and information theories. Reported higher-order-logic formalizations of the Lebesgue integral either do not include, or have a very limited support for the Borel algebra, which is the sigma algebra used on any topological space over which the Lebesgue integral is defined. In this paper, we overcome this limitation by presenting a formalization of Borel sigma algebra that can be used on any topological space, such as the complex numbers or the n-dimensional Euclidean space. Building on top of this framework, we have been able to prove some key Lebesgue integral properties, like its linearity and monotone convergence. Furthermore, we present the formalization of the "almost everywhere" relation and prove that the Lebesgue integral does not distinguish between functions which differ on a null set as well as other important results based on this concept. To illustrate the effectiveness of our approach we present the formal verification of Markov and Chebyshev inequalities and the weak law of large numbers theorem, which are widely used properties in the probability and information theories.