ISABELLE 2014 PAPERS (UNREFEREED): PAPERS WITH ABSTRACTS

ABSTRACT. We describe a formally verified proof of the Central Limit Theorem in the Isabelle proof assistant.

ABSTRACT. We describe work on an Isabelle model for the specification of a separation kernel done within the EURO-MILS project

ABSTRACT. This work in progress report envisions a library for multivariate polynomials developed jointly by experts from computer theorem proving (CTP) and computer algebra (CA). The urgency of verified algorithms has been recognised in the field of CA, but the cultural gap to CTP is considerable; CA users expect high usability and efficiency. This work collects the needs of CA experts and reports on the design of a proof-of-concept prototype in Isabelle/HOL. The CA requirements have not yet been fully settled, and its development is still at an early stage. The authors hope for lively discussions at the Isabelle Workshop.

ABSTRACT. HOL types are naturally interpreted as nonempty sets---this intuition is reflected in the type definition rule for the HOL-based systems (including Isabelle/HOL), where a new type can be defined whenever a nonempty set is exhibited. However, in HOL this definition mechanism cannot be applied inside proof contexts. We analyze some undesired consequences of this limitation and propose a more expressive type-definition rule that addresses it. The new expressive power opens the opportunity for a package that relativizes type-based statements to more flexible set-based variants---to streamline this process, we further implement a rule that transforms the implicit type-class constraints into explicit assumptions. Moreover, our tool is an interesting use case of Lifting and Transfer.

ABSTRACT. We report on the graph and automata library that is used in the fully verified LTL model checker CAVA. Most components of CAVA use some type of graphs or automata.

A common automata library simplifies assembly of the components to a working model checker and reduces redundancy.

The CAVA automata library provides a hierarchy of graph and automata classes, together with some standard algorithms. Its object oriented design allows for sharing of algorithms, theorems, and implementations between the different types of graphs, and also simplifies adding new graph types. Moreover, it is integrated into the Automatic Refinement Framework, supporting automatic refinement of the abstract automata types to efficient data structures.

Note that the CAVA automata library is work in progress. Currently, it is very specifically tailored towards the requirements of the CAVA model checker. Nevertheless, the formalization techniques allow an extension of the library to a wider scope. Moreover, they are not limited to graph libraries, but apply to class hierarchies in general.

ABSTRACT. Isabelle/HOL is not just a theorem prover, it has become a functional programming language. Algebraic datatypes and (pure) recursive functions are defined with various packages and compiled to executable code with the code generator. In this work, we explore whether and how this programming language is suitable for developing applications, which are stateful, interact with the environment, and use external libraries. To that end, we have implemented a prototype of the TLS network protocol as a case study. We present a model of interaction in HOL and its compilation, and discuss on the challenges in application development that the theorem prover/HOL Isabelle poses.

ABSTRACT. A framework for the analysis of the amortized complexity of (functional) data structures is formalized in Isabelle/HOL and applied to two non-trivial examples: skew heaps and splay trees. In the same spirit we show that the move-to-front algorithm for the list update problem is 2-competitive.

ABSTRACT. The first step in program verification is often a call to a verification condition generator (VCG) which decomposes a program into a set of logical formulas, the verification conditions. These verification conditions must then be discharged manually.

The process of constructing the verification conditions loses much of the structure of the original program. In this article, we extend the VCG to attach annotations to the verification conditions and hence preserve the program structure. We implemented this approach in the Isabelle theorem prover. This allows us to replace unstructured proof scripts by structured Isar proofs.

ABSTRACT. This article presents a pattern-based language designed to select (a set of) subterms of a given term in a concise and robust way. Building on this language, we implement a single-step rewriting tactic in the Isabelle theorem prover, which removes the need for obscure "occurrence numbers" for subterm selection.

The language was inspired by the language of patterns of Gonthier and Tassi, but provides an elegant way of handling bound variables and a modular semantics.

ABSTRACT. Isabelle/HOL has recently been enriched with a new definitional package for datatypes and codatatypes. The package introduces the specified types and derives auxiliary constants and characteristic theorems, notably (co)recursors and (co)induction principles. We now introduce support for high-level specifications of (co)recursive functions, in the form of three commands: primrec, primcorec, and primcorecursive. The new commands internally reduce the specifications to arguments to the (co)recursor and generate a number of theorems about the function definition, automating an otherwise tedious process.

ABSTRACT. Gödel’s two incompleteness theorems have been proved in Isabelle. The nominal package was used to handle variable binding in conjunction with de Bruijn indexes. This is the first mechanical proof of the second incompleteness theorem.

ABSTRACT. Verifying the implementation of complex algorithms in reasonable time goes beyond the state of the art of current verification tools. Certifying algorithms compute in addition to each output a witness certifying that the output is correct. A checker for a certifying algorithm checks the witness for correctness and is usually much simpler than the algorithm. Verification of checkers is feasible with current tools and leads to computations that can be completely trusted.

Previous work verified several checkers from the algorithmic library LEDA using the interactive theorem prover Isabelle/HOL as a backend to the automatic code verifier VCC. Recent work shows that verification can be carried out completely within Isabelle/HOL and compares this with the previous approach concluding that this approach is more trustworthy with comparable efforts in the field of graph theory.

Here we use use the more recent framework and present a verification of a Simpl shortest path checker algorithm with nonnegative edge weights solely within Isabelle/HOL.

ABSTRACT. A system demo of Isabelle/jEdit in the forthcoming Isabelle2014 release (summer 2014).