ABSTRACT. This is a hands-on tutorial introduction to the proof assistant Isabelle/HOL. Slide presentations alternate with practical exercises: partipants should bring their own laptop with Isabelle installed. There will be seasoned Isabelle tutors to help you using the system. The tutorial takes 3.5h and has three sections:

1. Recursion and induction
   The initial introduction concentrates on defining small functional programs and proving properties about them by induction.
2. Logic and Automation
   This section introduces more of the logic and the available automation, including the famous Sledgehammer that harnesses external automatic theorem provers.
3. Structured proofs
   This section introduces Isabelle's structured proof language Isar, which combines readability (via block-structured natural-deduction proofs) with conciseness (via the rich proof automation infrastructure).

See also Programming and Proving with Isabelle/HOL.

NOTE: Please install this Isabelle release candidate before coming to the tutorial.

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

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. 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. This is a hands-on tutorial introduction to the proof assistant Isabelle/HOL. Slide presentations alternate with practical exercises: partipants should bring their own laptop with Isabelle installed. There will be seasoned Isabelle tutors to help you using the system. The tutorial takes 3.5h and has three sections:

1. Recursion and induction
   The initial introduction concentrates on defining small functional programs and proving properties about them by induction.
2. Logic and Automation
   This section introduces more of the logic and the available automation, including the famous Sledgehammer that harnesses external automatic theorem provers.
3. Structured proofs
   This section introduces Isabelle's structured proof language Isar, which combines readability (via block-structured natural-deduction proofs) with conciseness (via the rich proof automation infrastructure).

See also Programming and Proving with Isabelle/HOL.

NOTE: Please install this <a href="http://isabelle.in.tum.de/website-Isabelle2014-RC0/">Isabelle release candidate</a> before coming to the tutorial.

ABSTRACT. We report on the experience of designing, formally verifying and using CoCon, a conference management system with verified document confidentiality.

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. 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. 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. Isabelle/jEdit is the default user-interface and Prover IDE (PIDE) for Isabelle. After several years of development of Isabelle/PIDE concepts and implementation of Isabelle/Scala infrastructure, Isabelle/jEdit was first released in October 2011 as a proper application. Each subsequent release made significant progress, so that we can speak already of about 5 generations of Isabelle Prover IDEs today.

This short tutorial is meant to help seasoned users of Isabelle, who have not yet discovered the full potential of the jEdit text editor and the Isabelle/jEdit Prover IDE, to get up-to-date. The demonstration will show established functionality of Isabelle2013-2 (December 2013).

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. This system demo will give an overview of NEWS for Isabelle/jEdit in the forthcoming Isabelle2014 release, which is anticipated for summer 2014. Both the prover and the integration with the underlying jEdit editor have been refined in various ways. Here is an incomplete list of notable items: improved completion mechanism, integrated spell-checker, hyperlink navigation within the editor, URL and browser support, support for auxiliary files, and official SML'97 IDE support.

See also Isabelle2014-RC0, which is the same pre-release snapshot that will be used in the Isabelle tutorial.

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. We describe work on an Isabelle/HOL model for the specification of a separation kernel done within the EURO-MILS (http://www.euromils.eu/) project. We chose to extensible records to specify the state. By an example of a theory specifying a group of "event" API calls, it is shown how lemmas on local state are used for obtaining proof obligations for a global separation property.  

ABSTRACT. Using current verification tools to verify complex algorithms in reasonable time is challenging. Certifying algorithms compute not only an output but also a witness certifying that the output is correct. A checker for a certifying algorithm is a simple program that decides whether the witness is correct for a particular input and output. Verification of checkers is feasible and leads to trustworthy computations. 

In previous work, we verified checkers from the algorithmic library LEDA using the interactive theorem prover Isabelle/HOL as a backend to the automatic code verifier VCC. More recently, we showed that verification can be carried out completely within Isabelle/HOL and compared this to the previous approach concluding that the more recent approach is more trustworthy with comparable efforts. Here, we use the more recent framework, and implement a shortest path checker algorithm for graphs with nonnegative edge weights in the imperative pseudo-code language Simpl.  Moreover, we formally verify the checker using Isabelle/HOL.

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. 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.