eng Schloss Dagstuhl – Leibniz-Zentrum für Informatik Leibniz International Proceedings in Informatics 1868-8969 2019-09-05 141 0 0 10.4230/LIPIcs.ITP.2019 article Harrison, John 1 O'Leary, John 2 Tolmach, Andrew 3 Amazon AWS, Portland, OR, USA Intel Corporation Portland State University, Portland, OR, USA LIPIcs, Volume 141, ITP'19, Complete Volume https://drops.dagstuhl.de/storage/00lipics/lipics-vol141-itp2019/LIPIcs.ITP.2019/LIPIcs.ITP.2019.pdf Theory of computation, Logic eng Schloss Dagstuhl – Leibniz-Zentrum für Informatik Leibniz International Proceedings in Informatics 1868-8969 2019-09-05 141 0:i 0:xiv 10.4230/LIPIcs.ITP.2019.0 article Harrison, John 1 O'Leary, John 2 Tolmach, Andrew 3 Amazon AWS, Portland, OR, USA Intel Corporation Portland State University, Portland, OR, USA Front Matter, Table of Contents, Preface, Conference Organization https://drops.dagstuhl.de/storage/00lipics/lipics-vol141-itp2019/LIPIcs.ITP.2019.0/LIPIcs.ITP.2019.0.pdf Front Matter Table of Contents Preface Conference Organization eng Schloss Dagstuhl – Leibniz-Zentrum für Informatik Leibniz International Proceedings in Informatics 1868-8969 2019-09-05 141 1:1 1:1 10.4230/LIPIcs.ITP.2019.1 article Andronick, June 1 2 CSIRO's Data61, Sydney, Australia UNSW, Sydney, Australia In the last ten years, we have been porting, maintaining, and evolving the world’s largest proof base, the formal proof in Isabelle/HOL of the seL4 microkernel. But actually, there is no such thing as "the seL4 proof"; there are a number of proofs (functional correctness, binary translation validation, integrity and confidentiality proofs, etc) about a number of instances of seL4 (depending on the hardware platform it runs on, the features it includes, the extensions it supports). We will give an overview of the current state of these proofs, and, importantly, the challenges we face in keeping to maintain, evolve and extend them, and the processes we have put in place to manage their dependence on the evolving implementation. https://drops.dagstuhl.de/storage/00lipics/lipics-vol141-itp2019/LIPIcs.ITP.2019.1/LIPIcs.ITP.2019.1.pdf Proof maintentance proof evolution seL4 Isabelle/HOL eng Schloss Dagstuhl – Leibniz-Zentrum für Informatik Leibniz International Proceedings in Informatics 1868-8969 2019-09-05 141 2:1 2:1 10.4230/LIPIcs.ITP.2019.2 article Buzzard, Kevin 1 Imperial College, London, U.K. Formalised mathematics has a serious image problem in mathematics departments. Mathematicians working in "mainstream" areas such as modern algebra, analysis, geometry etc have absolutely no desire to work formally, it slows them down and they cannot see the point. The mathematical community has its own methods for deciding whether a proof (in pdf format) is correct or not; these methods rely on the views of a cabal of experts - our high priests. Our proof of the odd order theorem is "John Thompson got a Fields Medal for the work". This proof is of a rather different nature to the formalised proof of Gonthier et al. Our methods are arcane and mysterious; there is also ample evidence that they are, in general, extremely accurate when it comes to the important stuff. I will talk about my attempts, as a "mainstream mathematician", to introduce formalised mathematics to my community. https://drops.dagstuhl.de/storage/00lipics/lipics-vol141-itp2019/LIPIcs.ITP.2019.2/LIPIcs.ITP.2019.2.pdf Formalization of mathematics eng Schloss Dagstuhl – Leibniz-Zentrum für Informatik Leibniz International Proceedings in Informatics 1868-8969 2019-09-05 141 3:1 3:1 10.4230/LIPIcs.ITP.2019.3 article Dixon, Martin 1 Intel Corp., Hillsboro, Oregon, USA The talk will touch on a number of practical opportunities for formal modeling and methods that Intel sees in HW security research including: instruction sets; the proliferation of programmable agents within SoC’s; and negative space testing. https://drops.dagstuhl.de/storage/00lipics/lipics-vol141-itp2019/LIPIcs.ITP.2019.3/LIPIcs.ITP.2019.3.pdf Hardware security formal modeling instruction sets SoC’s negative space testing eng Schloss Dagstuhl – Leibniz-Zentrum für Informatik Leibniz International Proceedings in Informatics 1868-8969 2019-09-05 141 4:1 4:19 10.4230/LIPIcs.ITP.2019.4 article Abdulaziz, Mohammad 1 https://orcid.org/0000-0002-8244-518X Gretton, Charles 2 https://orcid.org/0000-0001-9803-0168 Norrish, Michael 3 2 https://orcid.org/0000-0003-1163-8467 Technical University of Munich, Germany Australian National University, Canberra, Australia Data61, CSIRO, Canberra, Australia We report on our HOL4 verification of an AI planning algorithm. The algorithm is compositional in the following sense: a planning problem is divided into multiple smaller abstractions, then each of the abstractions is solved, and finally the abstractions' solutions are composed into a solution for the given problem. Formalising the algorithm, which was already quite well understood, revealed nuances in its operation which could lead to computing buggy plans. The formalisation also revealed that the algorithm can be presented more generally, and can be applied to systems with infinite states and actions, instead of only finite ones. Our formalisation extends an earlier model for slightly simpler transition systems, and demonstrates another step towards formal treatments of more and more of the algorithms and reasoning used in AI planning, as well as model checking. https://drops.dagstuhl.de/storage/00lipics/lipics-vol141-itp2019/LIPIcs.ITP.2019.4/LIPIcs.ITP.2019.4.pdf AI Planning Compositional Algorithms Algorithm Verification Transition Systems eng Schloss Dagstuhl – Leibniz-Zentrum für Informatik Leibniz International Proceedings in Informatics 1868-8969 2019-09-05 141 5:1 5:19 10.4230/LIPIcs.ITP.2019.5 article Affeldt, Reynald 1 https://orcid.org/0000-0002-2327-953X Garrigue, Jacques 2 https://orcid.org/0000-0001-8056-5519 Qi, Xuanrui 3 https://orcid.org/0000-0002-2032-1552 Tanaka, Kazunari 2 https://orcid.org/0000-0001-8460-7763 National Institute of Advanced Industrial Science and Technology, Tsukuba, Japan Graduate School of Mathematics, Nagoya University, Japan Department of Computer Science, Tufts University, Medford, MA, United States Succinct data structures give space-efficient representations of large amounts of data without sacrificing performance. They rely on cleverly designed data representations and algorithms. We present here the formalization in Coq/SSReflect of two different tree-based succinct representations and their accompanying algorithms. One is the Level-Order Unary Degree Sequence, which encodes the structure of a tree in breadth-first order as a sequence of bits, where access operations can be defined in terms of Rank and Select, which work in constant time for static bit sequences. The other represents dynamic bit sequences as binary balanced trees, where Rank and Select present a low logarithmic overhead compared to their static versions, and with efficient insertion and deletion. The two can be stacked to provide a dynamic representation of dictionaries for instance. While both representations are well-known, we believe this to be their first formalization and a needed step towards provably-safe implementations of big data. https://drops.dagstuhl.de/storage/00lipics/lipics-vol141-itp2019/LIPIcs.ITP.2019.5/LIPIcs.ITP.2019.5.pdf Coq small-scale reflection succinct data structures LOUDS bit vectors self balancing trees eng Schloss Dagstuhl – Leibniz-Zentrum für Informatik Leibniz International Proceedings in Informatics 1868-8969 2019-09-05 141 6:1 6:19 10.4230/LIPIcs.ITP.2019.6 article Avigad, Jeremy 1 https://orcid.org/0000-0003-1275-315X Carneiro, Mario 1 https://orcid.org/0000-0002-0470-5249 Hudon, Simon 1 Department of Philosophy, Carnegie Mellon University, Pittsburgh, PA, USA A broad class of data types, including arbitrary nestings of inductive types, coinductive types, and quotients, can be represented as quotients of polynomial functors. This provides perspicuous ways of constructing them and reasoning about them in an interactive theorem prover. https://drops.dagstuhl.de/storage/00lipics/lipics-vol141-itp2019/LIPIcs.ITP.2019.6/LIPIcs.ITP.2019.6.pdf data types polynomial functors inductive types coinductive types eng Schloss Dagstuhl – Leibniz-Zentrum für Informatik Leibniz International Proceedings in Informatics 1868-8969 2019-09-05 141 7:1 7:20 10.4230/LIPIcs.ITP.2019.7 article Bertholon, Guillaume 1 https://orcid.org/0000-0001-7000-382X Martin-Dorel, Érik 2 https://orcid.org/0000-0001-9716-9491 Roux, Pierre 3 https://orcid.org/0000-0003-2910-4738 École Normale Supérieure, Paris, France Lab. IRIT, University of Toulouse, CNRS, France ONERA, Toulouse, France Some mathematical proofs involve intensive computations, for instance: the four-color theorem, Hales' theorem on sphere packing (formerly known as the Kepler conjecture) or interval arithmetic. For numerical computations, floating-point arithmetic enjoys widespread usage thanks to its efficiency, despite the introduction of rounding errors. Formal guarantees can be obtained on floating-point algorithms based on the IEEE 754 standard, which precisely specifies floating-point arithmetic and its rounding modes, and a proof assistant such as Coq, that enjoys efficient computation capabilities. Coq offers machine integers, however floating-point arithmetic still needed to be emulated using these integers. A modified version of Coq is presented that enables using the machine floating-point operators. The main obstacles to such an implementation and its soundness are discussed. Benchmarks show potential performance gains of two orders of magnitude. https://drops.dagstuhl.de/storage/00lipics/lipics-vol141-itp2019/LIPIcs.ITP.2019.7/LIPIcs.ITP.2019.7.pdf Coq formal proofs floating-point arithmetic reflexive tactics Cholesky decomposition eng Schloss Dagstuhl – Leibniz-Zentrum für Informatik Leibniz International Proceedings in Informatics 1868-8969 2019-09-05 141 8:1 8:19 10.4230/LIPIcs.ITP.2019.8 article Bréhard, Florent 1 2 Mahboubi, Assia 3 Pous, Damien 4 Plume and AriC teams, LIP, ENS de Lyon, Université de Lyon, Lyon, France MAC team, LAAS-CNRS, Université de Toulouse, CNRS, Toulouse, France Gallinette team, LS2N, INRIA, Université de Nantes, Nantes, France Plume team, LIP, CNRS, ENS de Lyon, Université de Lyon, Lyon, France We present a library to verify rigorous approximations of univariate functions on real numbers, with the Coq proof assistant. Based on interval arithmetic, this library also implements a technique of validation a posteriori based on the Banach fixed-point theorem. We illustrate this technique on the case of operations of division and square root. This library features a collection of abstract structures that organise the specfication of rigorous approximations, and modularise the related proofs. Finally, we provide an implementation of verified Chebyshev approximations, and we discuss a few examples of computations. https://drops.dagstuhl.de/storage/00lipics/lipics-vol141-itp2019/LIPIcs.ITP.2019.8/LIPIcs.ITP.2019.8.pdf approximation theory Chebyshev polynomials Banach fixed-point theorem interval arithmetic Coq eng Schloss Dagstuhl – Leibniz-Zentrum für Informatik Leibniz International Proceedings in Informatics 1868-8969 2019-09-05 141 9:1 9:16 10.4230/LIPIcs.ITP.2019.9 article Brown, Chad E. 1 Kaliszyk, Cezary 2 3 https://orcid.org/0000-0002-8273-6059 Pąk, Karol 4 https://orcid.org/0000-0002-7099-1669 Czech Technical University in Prague, Czech Republic University of Innsbruck, Austria University of Warsaw, Poland University of Białystok, Poland We formally introduce a foundation for computer verified proofs based on higher-order Tarski-Grothendieck set theory. We show that this theory has a model if a 2-inaccessible cardinal exists. This assumption is the same as the one needed for a model of plain Tarski-Grothendieck set theory. The foundation allows the co-existence of proofs based on two major competing foundations for formal proofs: higher-order logic and TG set theory. We align two co-existing Isabelle libraries, Isabelle/HOL and Isabelle/Mizar, in a single foundation in the Isabelle logical framework. We do this by defining isomorphisms between the basic concepts, including integers, functions, lists, and algebraic structures that preserve the important operations. With this we can transfer theorems proved in higher-order logic to TG set theory and vice versa. We practically show this by formally transferring Lagrange’s four-square theorem, Fermat 3-4, and other theorems between the foundations in the Isabelle framework. https://drops.dagstuhl.de/storage/00lipics/lipics-vol141-itp2019/LIPIcs.ITP.2019.9/LIPIcs.ITP.2019.9.pdf model higher-order Tarski Grothendieck proof foundation eng Schloss Dagstuhl – Leibniz-Zentrum für Informatik Leibniz International Proceedings in Informatics 1868-8969 2019-09-05 141 10:1 10:18 10.4230/LIPIcs.ITP.2019.10 article Brun, Matthias 1 Traytel, Dmitriy 2 https://orcid.org/0000-0001-7982-2768 Department of Computer Science, ETH Zürich, Switzerland Institute of Information Security, Department of Computer Science, ETH Zürich, Switzerland Authenticated data structures are a technique for outsourcing data storage and maintenance to an untrusted server. The server is required to produce an efficiently checkable and cryptographically secure proof that it carried out precisely the requested computation. Recently, Miller et al. [https://doi.org/10.1145/2535838.2535851] demonstrated how to support a wide range of such data structures by integrating an authentication construct as a first class citizen in a functional programming language. In this paper, we put this work to the test of formalization in the Isabelle proof assistant. With Isabelle’s help, we uncover and repair several mistakes and modify the small-step semantics to perform call-by-value evaluation rather than requiring terms to be in administrative normal form. https://drops.dagstuhl.de/storage/00lipics/lipics-vol141-itp2019/LIPIcs.ITP.2019.10/LIPIcs.ITP.2019.10.pdf Authenticated Data Structures Verifiable Computation Isabelle/HOL Nominal Isabelle eng Schloss Dagstuhl – Leibniz-Zentrum für Informatik Leibniz International Proceedings in Informatics 1868-8969 2019-09-05 141 11:1 11:19 10.4230/LIPIcs.ITP.2019.11 article Brunner, Julian 1 https://orcid.org/0000-0001-8922-6097 Seidl, Benedikt 1 https://orcid.org/0000-0002-9913-8709 Sickert, Salomon 1 https://orcid.org/0000-0002-0280-8981 Technische Universität München, Germany We present a formalisation of the unified translation approach from linear temporal logic (LTL) to omega-automata from [Javier Esparza et al., 2018]. This approach decomposes LTL formulas into "simple" languages and allows a clear separation of concerns: first, we formalise the purely logical result yielding this decomposition; second, we develop a generic, executable, and expressive automata library providing necessary operations on automata to re-combine the "simple" languages; third, we instantiate this generic theory to obtain a construction for deterministic Rabin automata (DRA). We extract from this particular instantiation an executable tool translating LTL to DRAs. To the best of our knowledge this is the first verified translation of LTL to DRAs that is proven to be double-exponential in the worst case which asymptotically matches the known lower bound. https://drops.dagstuhl.de/storage/00lipics/lipics-vol141-itp2019/LIPIcs.ITP.2019.11/LIPIcs.ITP.2019.11.pdf Automata Theory Automata over Infinite Words Deterministic Automata Linear Temporal Logic Model Checking Verified Algorithms eng Schloss Dagstuhl – Leibniz-Zentrum für Informatik Leibniz International Proceedings in Informatics 1868-8969 2019-09-05 141 12:1 12:17 10.4230/LIPIcs.ITP.2019.12 article Carneiro, Mario 1 https://orcid.org/0000-0002-0470-5249 Carnegie Mellon University, Pittsburgh, PA, USA We present an extension to the mathlib library of the Lean theorem prover formalizing the foundations of computability theory. We use primitive recursive functions and partial recursive functions as the main objects of study, and we use a constructive encoding of partial functions such that they are executable when the programs in question provably halt. Main theorems include the construction of a universal partial recursive function and a proof of the undecidability of the halting problem. Type class inference provides a transparent way to supply Gödel numberings where needed and encapsulate the encoding details. https://drops.dagstuhl.de/storage/00lipics/lipics-vol141-itp2019/LIPIcs.ITP.2019.12/LIPIcs.ITP.2019.12.pdf Lean computability halting problem primitive recursion eng Schloss Dagstuhl – Leibniz-Zentrum für Informatik Leibniz International Proceedings in Informatics 1868-8969 2019-09-05 141 13:1 13:19 10.4230/LIPIcs.ITP.2019.13 article Chen, Ran 1 Cohen, Cyril 2 Lévy, Jean-Jacques 3 Merz, Stephan 4 Théry, Laurent 2 Institute of Software of the Chinese Academy of Sciences, Beijing, China Université Côte d'Azur, Inria, Sophia Antipolis, France Irif & Inria, Paris, France Université de Lorraine, CNRS, Inria, LORIA, Nancy, France Comparing provers on a formalization of the same problem is always a valuable exercise. In this paper, we present the formal proof of correctness of a non-trivial algorithm from graph theory that was carried out in three proof assistants: Why3, Coq, and Isabelle. https://drops.dagstuhl.de/storage/00lipics/lipics-vol141-itp2019/LIPIcs.ITP.2019.13/LIPIcs.ITP.2019.13.pdf Mathematical logic Formal proof Graph algorithm Program verification eng Schloss Dagstuhl – Leibniz-Zentrum für Informatik Leibniz International Proceedings in Informatics 1868-8969 2019-09-05 141 14:1 14:18 10.4230/LIPIcs.ITP.2019.14 article Czajka, Łukasz 1 https://orcid.org/0000-0001-8083-4280 Faculty of Informatics, TU Dortmund University, Germany We introduce two coinduction principles and two proof translations which, under certain conditions, map coinductive proofs that use our principles to guarded Coq proofs. The first principle provides an "operational" description of a proof by coinduction, which is easy to reason with informally. The second principle extends the first one to allow for direct proofs by coinduction of statements with existential quantifiers and multiple coinductive predicates in the conclusion. The principles automatically enforce the correct use of the coinductive hypothesis. We implemented the principles and the proof translations in a Coq plugin. https://drops.dagstuhl.de/storage/00lipics/lipics-vol141-itp2019/LIPIcs.ITP.2019.14/LIPIcs.ITP.2019.14.pdf coinduction Coq guardedness corecursion eng Schloss Dagstuhl – Leibniz-Zentrum für Informatik Leibniz International Proceedings in Informatics 1868-8969 2019-09-05 141 15:1 15:19 10.4230/LIPIcs.ITP.2019.15 article Dahmen, Sander R. 1 https://orcid.org/0000-0002-0014-0789 Hölzl, Johannes 2 https://orcid.org/0000-0003-0869-9250 Lewis, Robert Y. 2 https://orcid.org/0000-0002-5266-1121 Department of Mathematics, Vrije Universiteit Amsterdam, The Netherlands Department of Computer Science, Vrije Universiteit Amsterdam, The Netherlands In 2016, Ellenberg and Gijswijt established a new upper bound on the size of subsets of F^n_q with no three-term arithmetic progression. This problem has received much mathematical attention, particularly in the case q = 3, where it is commonly known as the cap set problem. Ellenberg and Gijswijt’s proof was published in the Annals of Mathematics and is noteworthy for its clever use of elementary methods. This paper describes a formalization of this proof in the Lean proof assistant, including both the general result in F^n_q and concrete values for the case q = 3. We faithfully follow the pen and paper argument to construct the bound. Our work shows that (some) modern mathematics is within the range of proof assistants. https://drops.dagstuhl.de/storage/00lipics/lipics-vol141-itp2019/LIPIcs.ITP.2019.15/LIPIcs.ITP.2019.15.pdf formal proof combinatorics cap set problem Lean eng Schloss Dagstuhl – Leibniz-Zentrum für Informatik Leibniz International Proceedings in Informatics 1868-8969 2019-09-05 141 16:1 16:19 10.4230/LIPIcs.ITP.2019.16 article Eberl, Manuel 1 https://orcid.org/0000-0002-4263-6571 Technical University of Munich, Boltzmannstraße 3, Garching bei München, Germany In this paper, I present a formalisation of a large portion of Apostol’s Introduction to Analytic Number Theory in Isabelle/HOL. Of the 14 chapters in the book, the content of 9 has been mostly formalised, while the content of 3 others was already mostly available in Isabelle before. The most interesting results that were formalised are: - The Riemann and Hurwitz zeta functions and the Dirichlet L functions - Dirichlet’s theorem on primes in arithmetic progressions - An analytic proof of the Prime Number Theorem - The asymptotics of arithmetical functions such as the prime omega function, the divisor count sigma_0(n), and Euler’s totient function phi(n) https://drops.dagstuhl.de/storage/00lipics/lipics-vol141-itp2019/LIPIcs.ITP.2019.16/LIPIcs.ITP.2019.16.pdf Isabelle theorem proving analytic number theory number theory arithmetical function Dirichlet series prime number theorem Dirichlet’s theorem zeta function L functions eng Schloss Dagstuhl – Leibniz-Zentrum für Informatik Leibniz International Proceedings in Informatics 1868-8969 2019-09-05 141 17:1 17:19 10.4230/LIPIcs.ITP.2019.17 article Forster, Yannick 1 Kunze, Fabian 1 Saarland University, Saarland Informatics Campus (SIC), Saarbrücken, Germany We provide a plugin extracting Coq functions of simple polymorphic types to the (untyped) call-by-value lambda calculus L. The plugin is implemented in the MetaCoq framework and entirely written in Coq. We provide Ltac tactics to automatically verify the extracted terms w.r.t a logical relation connecting Coq functions with correct extractions and time bounds, essentially performing a certifying translation and running time validation. We provide three case studies: A universal L-term obtained as extraction from the Coq definition of a step-indexed self-interpreter for L, a many-reduction from solvability of Diophantine equations to the halting problem of L, and a polynomial-time simulation of Turing machines in L. https://drops.dagstuhl.de/storage/00lipics/lipics-vol141-itp2019/LIPIcs.ITP.2019.17/LIPIcs.ITP.2019.17.pdf call-by-value lambda calculus Coq constructive type theory extraction computability eng Schloss Dagstuhl – Leibniz-Zentrum für Informatik Leibniz International Proceedings in Informatics 1868-8969 2019-09-05 141 18:1 18:20 10.4230/LIPIcs.ITP.2019.18 article Guéneau, Armaël 1 Jourdan, Jacques-Henri 2 Charguéraud, Arthur 3 Pottier, François 1 Inria, Paris, France CNRS, LRI, Univ. Paris Sud, Université Paris Saclay, France Inria & Université de Strasbourg, CNRS, ICube, Strasbourg, France We study a state-of-the-art incremental cycle detection algorithm due to Bender, Fineman, Gilbert, and Tarjan. We propose a simple change that allows the algorithm to be regarded as genuinely online. Then, we exploit Separation Logic with Time Credits to simultaneously verify the correctness and the worst-case amortized asymptotic complexity of the modified algorithm. https://drops.dagstuhl.de/storage/00lipics/lipics-vol141-itp2019/LIPIcs.ITP.2019.18/LIPIcs.ITP.2019.18.pdf interactive deductive program verification complexity analysis eng Schloss Dagstuhl – Leibniz-Zentrum für Informatik Leibniz International Proceedings in Informatics 1868-8969 2019-09-05 141 19:1 19:19 10.4230/LIPIcs.ITP.2019.19 article Han, Jesse Michael 1 van Doorn, Floris 1 Department of Mathematics, University of Pittsburgh, PA, USA We describe a formalization of forcing using Boolean-valued models in the Lean 3 theorem prover, including the fundamental theorem of forcing and a deep embedding of first-order logic with a Boolean-valued soundness theorem. As an application of our framework, we specialize our construction to the Boolean algebra of regular opens of the Cantor space 2^{omega_2 x omega} and formally verify the failure of the continuum hypothesis in the resulting model. https://drops.dagstuhl.de/storage/00lipics/lipics-vol141-itp2019/LIPIcs.ITP.2019.19/LIPIcs.ITP.2019.19.pdf Interactive theorem proving formal verification set theory forcing independence proofs continuum hypothesis Boolean-valued models Lean eng Schloss Dagstuhl – Leibniz-Zentrum für Informatik Leibniz International Proceedings in Informatics 1868-8969 2019-09-05 141 20:1 20:18 10.4230/LIPIcs.ITP.2019.20 article Haslbeck, Maximilian P. L. 1 https://orcid.org/0000-0003-4306-869X Lammich, Peter 2 https://orcid.org/0000-0003-3576-0504 Technische Universität München, Germany The University of Manchester, England Separation Logic with Time Credits is a well established method to formally verify the correctness and run-time of algorithms, which has been applied to various medium-sized use-cases. Refinement is a technique in program verification that makes software projects of larger scale manageable. Combining these two techniques for the first time, we present a methodology for verifying the functional correctness and the run-time analysis of algorithms in a modular way. We use it to verify Kruskal’s minimum spanning tree algorithm and the Edmonds - Karp algorithm for network flow. An adaptation of the Isabelle Refinement Framework [Lammich and Tuerk, 2012] enables us to specify the functional result and the run-time behaviour of abstract algorithms which can be refined to more concrete algorithms. From these, executable imperative code can be synthesized by an extension of the Sepref tool [Lammich, 2015], preserving correctness and the run-time bounds of the abstract algorithm. https://drops.dagstuhl.de/storage/00lipics/lipics-vol141-itp2019/LIPIcs.ITP.2019.20/LIPIcs.ITP.2019.20.pdf Isabelle Time Complexity Analysis Separation Logic Program Verification Refinement Run Time Algorithms eng Schloss Dagstuhl – Leibniz-Zentrum für Informatik Leibniz International Proceedings in Informatics 1868-8969 2019-09-05 141 21:1 21:18 10.4230/LIPIcs.ITP.2019.21 article Immler, Fabian 1 https://orcid.org/0000-0002-5468-1513 Rädle, Jonas 2 https://orcid.org/0000-0002-7714-0218 Wenzel, Makarius 3 School of Computer Science, Carnegie Mellon University, USA Fakultät für Informatik, Technische Universität München, Germany Augsburg, Germany We present a novel approach to combine the HOL4 and Isabelle theorem provers: both are implemented in SML and based on distinctive variants of HOL. The design of HOL4 allows to replace its inference kernel modules, and the system infrastructure of Isabelle allows to embed other applications of SML. That is the starting point to provide a virtual instance of HOL4 in the same run-time environment as Isabelle. Moreover, with an implementation of a virtual HOL4 kernel that operates on Isabelle/HOL terms and theorems, we can load substantial HOL4 libraries to make them Isabelle theories, but still disconnected from existing Isabelle content. Finally, we introduce a methodology based on the transfer package of Isabelle to connect the imported HOL4 material to that of Isabelle/HOL. https://drops.dagstuhl.de/storage/00lipics/lipics-vol141-itp2019/LIPIcs.ITP.2019.21/LIPIcs.ITP.2019.21.pdf Virtualization HOL4 Isabelle Isabelle/HOL Isabelle/ML eng Schloss Dagstuhl – Leibniz-Zentrum für Informatik Leibniz International Proceedings in Informatics 1868-8969 2019-09-05 141 22:1 22:19 10.4230/LIPIcs.ITP.2019.22 article Lammich, Peter 1 The University of Manchester, UK We present a framework to generate verified LLVM programs from Isabelle/HOL. It is based on a code generator that generates LLVM text from a simplified fragment of LLVM, shallowly embedded into Isabelle/HOL. On top, we have developed a separation logic, a verification condition generator, and an LLVM backend to the Isabelle Refinement Framework. As case studies, we have produced verified LLVM implementations of binary search and the Knuth-Morris-Pratt string search algorithm. These are one order of magnitude faster than the Standard-ML implementations produced with the original Refinement Framework, and on par with unverified C implementations. Adoption of the original correctness proofs to the new LLVM backend was straightforward. The trusted code base of our approach is the shallow embedding of the LLVM fragment and the code generator, which is a pretty printer combined with some straightforward compilation steps. https://drops.dagstuhl.de/storage/00lipics/lipics-vol141-itp2019/LIPIcs.ITP.2019.22/LIPIcs.ITP.2019.22.pdf Isabelle/HOL LLVM Separation Logic Verification Condition Generator Code Generation eng Schloss Dagstuhl – Leibniz-Zentrum für Informatik Leibniz International Proceedings in Informatics 1868-8969 2019-09-05 141 23:1 23:18 10.4230/LIPIcs.ITP.2019.23 article Lammich, Peter 1 https://orcid.org/0000-0003-3576-0504 Nipkow, Tobias 2 https://orcid.org/0000-0003-0730-515X The University of Manchester, UK Technical University Munich, Germany The starting point of this paper is a new, purely functional, simple and efficient data structure combining a search tree and a priority queue, which we call a priority search tree. The salient feature of priority search trees is that they offer a decrease-key operation, something that is missing from other simple, purely functional priority queue implementations. As two applications of this data structure we verify purely functional, simple and efficient implementations of Prim’s and Dijkstra’s algorithms. This constitutes the first verification of an executable and even efficient version of Prim’s algorithm. https://drops.dagstuhl.de/storage/00lipics/lipics-vol141-itp2019/LIPIcs.ITP.2019.23/LIPIcs.ITP.2019.23.pdf Priority queue Dijkstra’s algorithm Prim’s algorithm verification Isabelle eng Schloss Dagstuhl – Leibniz-Zentrum für Informatik Leibniz International Proceedings in Informatics 1868-8969 2019-09-05 141 24:1 24:18 10.4230/LIPIcs.ITP.2019.24 article Lasser, Sam 1 Casinghino, Chris 2 Fisher, Kathleen 1 Roux, Cody 2 Tufts University, Medford, MA, USA Draper, Cambridge, MA, USA An LL(1) parser is a recursive descent algorithm that uses a single token of lookahead to build a grammatical derivation for an input sequence. We present an LL(1) parser generator that, when applied to grammar G, produces an LL(1) parser for G if such a parser exists. We use the Coq Proof Assistant to verify that the generator and the parsers that it produces are sound and complete, and that they terminate on all inputs without using fuel parameters. As a case study, we extract the tool’s source code and use it to generate a JSON parser. The generated parser runs in linear time; it is two to four times slower than an unverified parser for the same grammar. https://drops.dagstuhl.de/storage/00lipics/lipics-vol141-itp2019/LIPIcs.ITP.2019.24/LIPIcs.ITP.2019.24.pdf interactive theorem proving top-down parsing eng Schloss Dagstuhl – Leibniz-Zentrum für Informatik Leibniz International Proceedings in Informatics 1868-8969 2019-09-05 141 25:1 25:18 10.4230/LIPIcs.ITP.2019.25 article Mehta, Mihir Parang 1 Cook, William R. 1 University of Texas at Austin, USA Filesystems are an essential component of most computer systems. Work on the verification of filesystem functionality has been focused on constructing new filesystems in a manner which simplifies the process of verifying them against specifications. This leaves open the question of whether filesystems already in use are correct at the binary level. This paper introduces LoFAT, a model of the FAT32 filesystem which efficiently implements a subset of the POSIX filesystem operations, and HiFAT, a more abstract model of FAT32 which is simpler to reason about. LoFAT is proved to be correct in terms of refinement of HiFAT, and made executable by enabling the state of the model to be written to and read from FAT32 disk images. EqFAT, an equivalence relation for disk images, considers whether two disk images contain the same directory tree modulo reordering of files and implementation-level details regarding cluster allocation. A suite of co-simulation tests uses EqFAT to compare the operation of existing FAT32 implementations to LoFAT and check the correctness of existing implementations of FAT32 such as the mtools suite of programs and the Linux FAT32 implementation. All models and proofs are formalized and mechanically verified in ACL2. https://drops.dagstuhl.de/storage/00lipics/lipics-vol141-itp2019/LIPIcs.ITP.2019.25/LIPIcs.ITP.2019.25.pdf interactive theorem proving filesystems eng Schloss Dagstuhl – Leibniz-Zentrum für Informatik Leibniz International Proceedings in Informatics 1868-8969 2019-09-05 141 26:1 26:19 10.4230/LIPIcs.ITP.2019.26 article Ringer, Talia 1 Yazdani, Nathaniel 1 Leo, John 2 Grossman, Dan 1 University of Washington, USA Halfaya Research, USA Ornaments express relations between inductive types with the same inductive structure. We implement fully automatic proof reuse for a particular class of ornaments in a Coq plugin, and show how such a tool can give programmers the rewards of using indexed inductive types while automating away many of the costs. The plugin works directly on Coq code; it is the first ornamentation tool for a non-embedded dependently typed language. It is also the first tool to automatically identify ornaments: To lift a function or proof, the user must provide only the source type, the destination type, and the source function or proof. In taking advantage of the mathematical properties of ornaments, our approach produces faster functions and smaller terms than a more general approach to proof reuse in Coq. https://drops.dagstuhl.de/storage/00lipics/lipics-vol141-itp2019/LIPIcs.ITP.2019.26/LIPIcs.ITP.2019.26.pdf ornaments proof reuse proof automation eng Schloss Dagstuhl – Leibniz-Zentrum für Informatik Leibniz International Proceedings in Informatics 1868-8969 2019-09-05 141 27:1 27:19 10.4230/LIPIcs.ITP.2019.27 article Sison, Robert 1 2 https://orcid.org/0000-0003-0313-9764 Murray, Toby 3 Data61, CSIRO, Australia UNSW Sydney, Australia University of Melbourne, Australia It is common to prove by reasoning over source code that programs do not leak sensitive data. But doing so leaves a gap between reasoning and reality that can only be filled by accounting for the behaviour of the compiler. This task is complicated when programs enforce value-dependent information-flow security properties (in which classification of locations can vary depending on values in other locations) and complicated further when programs exploit shared-variable concurrency. Prior work has formally defined a notion of concurrency-aware refinement for preserving value-dependent security properties. However, that notion is considerably more complex than standard refinement definitions typically applied in the verification of semantics preservation by compilers. To date it remains unclear whether it can be applied to a realistic compiler, because there exist no general decomposition principles for separating it into smaller, more familiar, proof obligations. In this work, we provide such a decomposition principle, which we show can almost halve the complexity of proving secure refinement. Further, we demonstrate its applicability to secure compilation, by proving in Isabelle/HOL the preservation of value-dependent security by a proof-of-concept compiler from an imperative While language to a generic RISC-style assembly language, for programs with shared-memory concurrency mediated by locking primitives. Finally, we execute our compiler in Isabelle on a While language model of the Cross Domain Desktop Compositor, demonstrating to our knowledge the first use of a compiler verification result to carry an information-flow security property down to the assembly-level model of a non-trivial concurrent program. https://drops.dagstuhl.de/storage/00lipics/lipics-vol141-itp2019/LIPIcs.ITP.2019.27/LIPIcs.ITP.2019.27.pdf Secure compilation Information flow security Concurrency Verification eng Schloss Dagstuhl – Leibniz-Zentrum für Informatik Leibniz International Proceedings in Informatics 1868-8969 2019-09-05 141 28:1 28:21 10.4230/LIPIcs.ITP.2019.28 article Steinberg, Florian 1 Théry, Laurent 2 Thies, Holger 3 INRIA Saclay, France INRIA Sophia-Antipolis, France Kyushu University, Japan We give a number of formal proofs of theorems from the field of computable analysis. Many of our results specify executable algorithms that work on infinite inputs by means of operating on finite approximations and are proven correct in the sense of computable analysis. The development is done in the proof assistant Coq and heavily relies on the Incone library for information theoretic continuity. This library is developed by one of the authors and the results of this paper extend the library. While full executability in a formal development of mathematical statements about real numbers and the like is not a feature that is unique to the Incone library, its original contribution is to adhere to the conventions of computable analysis to provide a general purpose interface for algorithmic reasoning on continuous structures. The paper includes a brief description of the most important concepts of Incone and its sub libraries mf and Metric. The results that provide complete computational content include that the algebraic operations and the efficient limit operator on the reals are computable, that the countably infinite product of a space with itself is isomorphic to a space of functions, compatibility of the enumeration representation of subsets of natural numbers with the abstract definition of the space of open subsets of the natural numbers, and that continuous realizability implies sequential continuity. We also describe many non-computational results that support the correctness of definitions from the library. These include that the information theoretic notion of continuity used in the library is equivalent to the metric notion of continuity on Baire space, a complete comparison of the different concepts of continuity that arise from metric and represented space structures and the discontinuity of the unrestricted limit operator on the real numbers and the task of selecting an element of a closed subset of the natural numbers. https://drops.dagstuhl.de/storage/00lipics/lipics-vol141-itp2019/LIPIcs.ITP.2019.28/LIPIcs.ITP.2019.28.pdf computable analysis Coq contionuous functionals discontinuity closed choice on the naturals eng Schloss Dagstuhl – Leibniz-Zentrum für Informatik Leibniz International Proceedings in Informatics 1868-8969 2019-09-05 141 29:1 29:18 10.4230/LIPIcs.ITP.2019.29 article Tassi, Enrico 1 Université côte d'Azur - Inria, France We describe a procedure to derive equality tests and their correctness proofs from inductive type declarations in Coq. Programs and proofs are derived compositionally, reusing code and proofs derived previously. The key steps are two. First, we design appropriate induction principles for data types defined using parametric containers. Second, we develop a technique to work around the modularity limitations imposed by the purely syntactic termination check Coq performs on recursive proofs. The unary parametricity translation of inductive data types turns out to be the key to both steps. Last but not least, we provide an implementation of the procedure for the Coq proof assistant based on the Elpi [Dunchev et al., 2015] extension language. https://drops.dagstuhl.de/storage/00lipics/lipics-vol141-itp2019/LIPIcs.ITP.2019.29/LIPIcs.ITP.2019.29.pdf Coq Containers Induction Equality test Parametricity translation eng Schloss Dagstuhl – Leibniz-Zentrum für Informatik Leibniz International Proceedings in Informatics 1868-8969 2019-09-05 141 30:1 30:16 10.4230/LIPIcs.ITP.2019.30 article Yamada, Akihisa 1 https://orcid.org/0000-0001-8872-2240 Dubut, Jérémy 1 2 National Institute of Informatics, Tokyo, Japan Japanese-French Laboratory for Informatics, Tokyo, Japan In this paper, we develop an Isabelle/HOL library of order-theoretic concepts, such as various completeness conditions and fixed-point theorems. We keep our formalization as general as possible: we reprove several well-known results about complete orders, often without any property of ordering, thus complete non-orders. In particular, we generalize the Knaster - Tarski theorem so that we ensure the existence of a quasi-fixed point of monotone maps over complete non-orders, and show that the set of quasi-fixed points is complete under a mild condition - attractivity - which is implied by either antisymmetry or transitivity. This result generalizes and strengthens a result by Stauti and Maaden. Finally, we recover Kleene’s fixed-point theorem for omega-complete non-orders, again using attractivity to prove that Kleene’s fixed points are least quasi-fixed points. https://drops.dagstuhl.de/storage/00lipics/lipics-vol141-itp2019/LIPIcs.ITP.2019.30/LIPIcs.ITP.2019.30.pdf Order Theory Lattice Theory Fixed-Points Isabelle/HOL eng Schloss Dagstuhl – Leibniz-Zentrum für Informatik Leibniz International Proceedings in Informatics 1868-8969 2019-09-05 141 31:1 31:19 10.4230/LIPIcs.ITP.2019.31 article Wu, Minchao 1 https://orcid.org/0000-0001-7651-7944 Goré, Rajeev 1 Research School of Computer Science, Australian National University, Australia We describe a formalization of modal tableaux with histories for the modal logics K, KT and S4 in Lean. We describe how we formalized the static and transitional rules, the non-trivial termination and the correctness of loop-checks. The formalized tableaux are essentially executable decision procedures with soundness and completeness proved. Termination is also proved in order to define them as functions in Lean. All of these decision procedures return a concrete Kripke model in cases where the input set of formulas is satisfiable, and a proof constructed via the tableau rules witnessing unsatisfiability otherwise. We also describe an extensible formalization of backjumping and its verified implementation for the modal logic K. As far as we know, these are the first verified decision procedures for these modal logics. https://drops.dagstuhl.de/storage/00lipics/lipics-vol141-itp2019/LIPIcs.ITP.2019.31/LIPIcs.ITP.2019.31.pdf Formal Methods Interactive Theorem Proving Modal Logic Lean eng Schloss Dagstuhl – Leibniz-Zentrum für Informatik Leibniz International Proceedings in Informatics 1868-8969 2019-09-05 141 32:1 32:19 10.4230/LIPIcs.ITP.2019.32 article Åman Pohjola, Johannes 1 Rostedt, Henrik 2 Myreen, Magnus O. 2 Data61/CSIRO, Sydney, Australia, University of New South Wales, Sydney, Australia Chalmers University of Technology, Gothenburg, Sweden There are useful programs that do not terminate, and yet standard Hoare logics are not able to prove liveness properties about non-terminating programs. This paper shows how a Hoare-like programming logic framework (characteristic formulae) can be extended to enable reasoning about the I/O behaviour of programs that do not terminate. The approach is inspired by transfinite induction rather than coinduction, and does not require non-terminating loops to be productive. This work has been developed in the HOL4 theorem prover and has been integrated into the ecosystem of proof tools surrounding the CakeML programming language. https://drops.dagstuhl.de/storage/00lipics/lipics-vol141-itp2019/LIPIcs.ITP.2019.32/LIPIcs.ITP.2019.32.pdf Program verification non-termination liveness Hoare logic eng Schloss Dagstuhl – Leibniz-Zentrum für Informatik Leibniz International Proceedings in Informatics 1868-8969 2019-09-05 141 33:1 33:7 10.4230/LIPIcs.ITP.2019.33 article Bayer, Jonas 1 David, Marco 2 Pal, Abhik 2 Stock, Benedikt 2 Schleicher, Dierk 3 Freie Universität Berlin, Arnimallee 2, 14195 Berlin, Germany Jacobs University Bremen, Campus Ring 1, 28759 Bremen, Germany Technische Universität Berlin, Germany Hilbert’s 10th problem asks for an algorithm to tell whether or not a given diophantine equation has a solution over the integers. The non-existence of such an algorithm was shown in 1970 by Yuri Matiyasevich. The key step is known as the DPRM theorem: every recursively enumerable set of natural numbers is Diophantine. We present the formalization of Matiyasevich’s proof of the DPRM theorem in Isabelle. To represent recursively enumerable sets in equations, we implement and arithmetize register machines. Using several number-theoretic lemmas, we prove that exponentiation has a diophantine representation. Further, we contribute a small library of number-theoretic implementations of binary digit-wise relations. Finally, we discuss and contribute an is_diophantine predicate. We expect the complete formalization of the DPRM theorem in the near future; at present it is complete except for a minor gap in the arithmetization proofs of register machines and extending the is_diophantine predicate by two binary digit-wise relations. https://drops.dagstuhl.de/storage/00lipics/lipics-vol141-itp2019/LIPIcs.ITP.2019.33/LIPIcs.ITP.2019.33.pdf DPRM theorem Hilbert’s tenth problem Diophantine predicates Register machines Recursively enumerable sets Isabelle Formal verification eng Schloss Dagstuhl – Leibniz-Zentrum für Informatik Leibniz International Proceedings in Informatics 1868-8969 2019-09-05 141 34:1 34:8 10.4230/LIPIcs.ITP.2019.34 article Jakubův, Jan 1 Urban, Josef 1 Czech Technical University in Prague, Czech Republic We describe a very large improvement of existing hammer-style proof automation over large ITP libraries by combining learning and theorem proving. In particular, we have integrated state-of-the-art machine learners into the E automated theorem prover, and developed methods that allow learning and efficient internal guidance of E over the whole Mizar library. The resulting trained system improves the real-time performance of E on the Mizar library by 70% in a single-strategy setting. https://drops.dagstuhl.de/storage/00lipics/lipics-vol141-itp2019/LIPIcs.ITP.2019.34/LIPIcs.ITP.2019.34.pdf Proof automation ITP hammers Automated theorem proving Machine learning eng Schloss Dagstuhl – Leibniz-Zentrum für Informatik Leibniz International Proceedings in Informatics 1868-8969 2019-09-05 141 35:1 35:7 10.4230/LIPIcs.ITP.2019.35 article Kaliszyk, Cezary 1 2 https://orcid.org/0000-0002-8273-6059 Pąk, Karol 3 https://orcid.org/0000-0002-7099-1669 University of Innsbruck, Austria University of Warsaw, Poland University of Białystok, Poland Declarative proof styles of different proof assistants include a number of incompatible features. In this paper we discuss and classify the differences between them and propose efficient algorithms for declarative proof outline translation. We demonstrate the practicality of our algorithms by automatically translating the proof outlines in 200 articles from the Mizar Mathematical Library to the Isabelle/Isar proof style. This generates the corresponding theories with 15301 proof outlines accepted by the Isabelle proof checker. The goal of our translation is to produce a declarative proof in the target system that is both accepted and short and therefore readable. For this three kinds of adaptations are required. First, the proof structure often needs to be rebuilt to capture the extensions of the natural deduction rules supported by the systems. Second, the references to previous items and their labels need to be matched and aligned. Finally, adaptations in the annotations of individual proof step may be necessary. https://drops.dagstuhl.de/storage/00lipics/lipics-vol141-itp2019/LIPIcs.ITP.2019.35/LIPIcs.ITP.2019.35.pdf Declarative Proof Translation Isabelle/Isar Mizar eng Schloss Dagstuhl – Leibniz-Zentrum für Informatik Leibniz International Proceedings in Informatics 1868-8969 2019-09-05 141 36:1 36:7 10.4230/LIPIcs.ITP.2019.36 article Severín, Daniel E. 1 2 https://orcid.org/0000-0003-2391-3489 Depto. de Matemática, Universidad Nacional de Rosario, Argentina CONICET, Argentina The Cockayne-Hedetniemi Domination Chain is a chain of inequalities between classic parameters of graph theory: for a given graph G, ir(G) <= gamma(G) <= iota(G) <= alpha(G) <= Gamma(G) <= IR(G). These parameters return the maximum/minimum cardinality of a set satisfying some property. However, they can be generalized for graphs with weighted vertices where the objective is to maximize/minimize the sum of weights of a set satisfying the same property, and the domination chain still holds for them. In this work, the definition of these parameters as well as the chain is formalized in Coq/Ssreflect. https://drops.dagstuhl.de/storage/00lipics/lipics-vol141-itp2019/LIPIcs.ITP.2019.36/LIPIcs.ITP.2019.36.pdf Domination Chain Coq Formalization of Mathematics