ABSTRACT. We give a formal and constructive proof in Coq/Ssreflect of the known result that the graphs of treewidth two are exactly those that do not admit K4 as a minor. This result is a milestone towards a formal proof of the recent result that isomorphism of treewidth-two graphs can be finitely axiomatized. The proof is based on a function extracting terms from K4-free graphs in such a way that the interpretation of an extracted term yields a treewidth-two graph isomorphic to the original graph.

ABSTRACT. We present a formalization of a translation from LTL formulae to generalized Büchi Automata in the HOL4 theorem prover. Translations from temporal logics to automata are at the core of model checking algorithms based on automata-theoretic techniques. The translation we verify proceeds in two steps: it produces Very Weak Alternating Automata at an intermediate stage, and then ultimately produces a generalized Büchi Automaton. After verifying both transformations, we also encode both of these automata models using a generic, functional graph type, and use the CakeML compiler to generate fully verified machine code implementing the translation.

ABSTRACT. We formally verify several computational reductions concerning the Post correspondence problem (PCP) using the proof assistant Coq. Our verification includes a reduction of the halting problem for Turing machines to string rewriting, a reduction of string rewriting to PCP, and reductions of PCP to the intersection problem and the palindrome problem for context-free grammars.

ABSTRACT. We present a lightweight framework in Isabelle/HOL for the automatic verified (functional or imperative) memoization of recursive functions. Our tool constructs a memoized version of the recursive function and proves a correspondence theorem between the two functions. A number of simple techniques allow us to achieve bottom-up computation and space-efficient memoization. The framework’s utility is demonstrated on a number of classic dynamic programming problems.

ABSTRACT. Code generated from a verified formalisation typically runs faster when it uses machine words instead of a syntactic representation of integers. This paper presents a library for Isabelle/HOL that links the existing formalisation of words to the machine words that the four target languages of Isabelle/HOL’s code generator provide. Our design ensures that (i) Isabelle/HOL machine words can be mapped soundly and efficiently to all target languages despite the differences in the APIs; (ii) they can be used uniformly with the three evaluation engines in Isabelle/HOL, namely code generation, normalisation by evaluation, and term rewriting; and (iii) they blend in with the existing formalisations of machine words. Several large-scale formalisation projects use our library to speed up their generated code.

To validate the unverified link between machine words in the logic and those in the target languages, we extended Isabelle/HOL with a general-purpose testing facility that compiles test cases expressed within Isabelle/HOL to the four target languages and runs them with the most common implementations of each language. When we applied this to our library of machine words, we discovered miscomputations in the 64-bit word library of one of the target-language implementations.

ABSTRACT. We present a short implementation of the well-known Tortoise and Hare cycle finding algorithm attributed to Robert W. Floyd in the constructive setting of axiom-free Coq. This algorithm is interesting from a constructive perspective because it is both very simple and potentially non-terminating (depending on the input). To overcome potential non-termination, we encode the given termination argument (there exists a cycle) into a bar inductive predicate that we use as termination certificate for the Coq implementation. From this development, we extract the standard OCaml implementation of this algorithm. We generalize the method to the full Floyd's algorithm that computes the entry point and the period of the cycle of the iterated sequence, when they do exist. We also consider the case of the more efficient Brent's algorithm for computing the period only. Again, the extracted codes correspond to the standard OCaml implementations of these algorithms.

ABSTRACT. Among formal methods, the deductive verification approach consists in
first building verification conditions and then resorting to
traditional theorem proving.  Most deductive verification tools
involve a high degree of proof automation through the use of SMT
solvers. Yet there may be a substantial part of interactive theorem
proving in program verification, such as inserting logical cuts, ghost
code, or inductive proofs via lemma functions. In this talk, I will
show how the Why3 tool for deductive verification resembles more and
more a traditional ITP, while stressing key differences between the
two.

ABSTRACT. Watchlist (also hint list) is a mechanism that allows related proofs to guide a proof search for a new conjecture. This mechanism has been used with the Otter and Prover9 theorem provers, both for interactive formalizations and for human-assisted proving of open conjectures in small theories. In this work we explore the use of watchlists in large theories coming from first-order translations of large ITP libraries, aiming at improving hammer-style automation by smarter internal guidance of the ATP systems. In particular, we (i) design watchlist-based clause evaluation heuristics inside the E ATP system, and (ii) develop new proof guiding algorithms that load many previous proofs inside the ATP and focus the proof search using a dynamically updated notion of proof matching. The methods are evaluated on a large set of problems coming from the Mizar library, showing significant improvement of E’s standard portfolio of strategies, and also of the previous best set of strategies invented for Mizar by evolutionary methods.

ABSTRACT. We mechanize in Coq a theorem by Karp, along with several extensions, that provide an easy to use "cookbook" method for verifying tail bounds of randomized algorithms, much like the traditional "Master Theorem" gives bounds for deterministic algorithms. We apply these results to several examples: the number of comparisons performed by QuickSort, the span of parallel QuickSort, the height of randomly generated binary search trees, and the number of rounds needed for a distributed leader election protocol. Because the constants involved in our symbolic bounds are concrete, we are able to use them to derive numerical probability bounds for various input sizes for these examples.

ABSTRACT. This work is a case study of the formal verification and complexity analysis of some famous probabilistic data structures and algorithms in the proof assistant Isabelle/HOL: – the expected number of comparisons in randomised Quicksort – the average-case analysis of deterministic Quicksort – the expected shape of an unbalanced random Binary Search Tree – the expected shape of a Treap The last two have, to our knowledge, never been analysed in a theorem prover before and the last one is particularly interesting because the analysis involves continuous distributions. The verification builds on the existing probability and measure theory in Isabelle/HOL. Algorithms are shallowly embedded and expressed in the Giry monad, which allows for a very natural and high-level presentation.