date = 2014-02-06
license = LGPL
topic = Mathematics/Analysis
abstract =
We apply data refinement to implement the real numbers, where we support all
numbers in the field extension Q[sqrt(b)], i.e., all numbers of the form p +
q * sqrt(b) for rational numbers p and q and some fixed natural number b. To
this end, we also developed algorithms to precisely compute roots of a
rational number, and to perform a factorization of natural numbers which
eliminates duplicate prime factors.
Our results have been used to certify termination proofs which involve
polynomial interpretations over the reals.
extra-history =
Change history:
[2014-07-11]: Moved NthRoot_Impl to Sqrt-Babylonian.
notify = rene.thiemann@uibk.ac.at
[ShortestPath]
title = An Axiomatic Characterization of the Single-Source Shortest Path Problem
author = Christine Rizkallah
date = 2013-05-22
topic = Mathematics/Graph theory
abstract = This theory is split into two sections. In the first section, we give a formal proof that a well-known axiomatic characterization of the single-source shortest path problem is correct. Namely, we prove that in a directed graph with a non-negative cost function on the edges the single-source shortest path function is the only function that satisfies a set of four axioms. In the second section, we give a formal proof of the correctness of an axiomatic characterization of the single-source shortest path problem for directed graphs with general cost functions. The axioms here are more involved because we have to account for potential negative cycles in the graph. The axioms are summarized in three Isabelle locales.
notify =
[Launchbury]
title = The Correctness of Launchbury's Natural Semantics for Lazy Evaluation
author = Joachim Breitner
date = 2013-01-31
topic = Computer science/Programming languages/Lambda calculi, Computer science/Semantics
abstract = In his seminal paper "Natural Semantics for Lazy Evaluation", John Launchbury proves his semantics correct with respect to a denotational semantics, and outlines an adequacy proof. We have formalized both semantics and machine-checked the correctness proof, clarifying some details. Furthermore, we provide a new and more direct adequacy proof that does not require intermediate operational semantics.
extra-history =
Change history:
[2014-05-24]: Added the proof of adequacy, as well as simplified and improved the existing proofs. Adjusted abstract accordingly.
[2015-03-16]: Booleans and if-then-else added to syntax and semantics, making this entry suitable to be used by the entry "Call_Arity".
notify =
[Call_Arity]
title = The Safety of Call Arity
author = Joachim Breitner
date = 2015-02-20
topic = Computer science/Programming languages/Transformations
abstract =
We formalize the Call Arity analysis, as implemented in GHC, and prove
both functional correctness and, more interestingly, safety (i.e. the
transformation does not increase allocation).
We use syntax and the denotational semantics from the entry
"Launchbury", where we formalized Launchbury's natural semantics for
lazy evaluation.
The functional correctness of Call Arity is proved with regard to that
denotational semantics. The operational properties are shown with
regard to a small-step semantics akin to Sestoft's mark 1 machine,
which we prove to be equivalent to Launchbury's semantics.
We use Christian Urban's Nominal2 package to define our terms and make
use of Brian Huffman's HOLCF package for the domain-theoretical
aspects of the development.
extra-history =
Change history:
[2015-03-16]: This entry now builds on top of the Launchbury entry,
and the equivalency proof of the natural and the small-step semantics
was added.
notify =
[CCS]
title = CCS in nominal logic
author = Jesper Bengtson
date = 2012-05-29
topic = Computer science/Concurrency/Process calculi
abstract = We formalise a large portion of CCS as described in Milner's book 'Communication and Concurrency' using the nominal datatype package in Isabelle. Our results include many of the standard theorems of bisimulation equivalence and congruence, for both weak and strong versions. One main goal of this formalisation is to keep the machine-checked proofs as close to their pen-and-paper counterpart as possible.
This entry is described in detail in Bengtson's thesis.
notify =
[Pi_Calculus]
title = The pi-calculus in nominal logic
author = Jesper Bengtson
date = 2012-05-29
topic = Computer science/Concurrency/Process calculi
abstract = We formalise the pi-calculus using the nominal datatype package, based on ideas from the nominal logic by Pitts et al., and demonstrate an implementation in Isabelle/HOL. The purpose is to derive powerful induction rules for the semantics in order to conduct machine checkable proofs, closely following the intuitive arguments found in manual proofs. In this way we have covered many of the standard theorems of bisimulation equivalence and congruence, both late and early, and both strong and weak in a uniform manner. We thus provide one of the most extensive formalisations of a the pi-calculus ever done inside a theorem prover.
A significant gain in our formulation is that agents are identified up to alpha-equivalence, thereby greatly reducing the arguments about bound names. This is a normal strategy for manual proofs about the pi-calculus, but that kind of hand waving has previously been difficult to incorporate smoothly in an interactive theorem prover. We show how the nominal logic formalism and its support in Isabelle accomplishes this and thus significantly reduces the tedium of conducting completely formal proofs. This improves on previous work using weak higher order abstract syntax since we do not need extra assumptions to filter out exotic terms and can keep all arguments within a familiar first-order logic.
This entry is described in detail in Bengtson's thesis.
notify =
[Psi_Calculi]
title = Psi-calculi in Isabelle
author = Jesper Bengtson
date = 2012-05-29
topic = Computer science/Concurrency/Process calculi
abstract = Psi-calculi are extensions of the pi-calculus, accommodating arbitrary nominal datatypes to represent not only data but also communication channels, assertions and conditions, giving it an expressive power beyond the applied pi-calculus and the concurrent constraint pi-calculus.
We have formalised psi-calculi in the interactive theorem prover Isabelle using its nominal datatype package. One distinctive feature is that the framework needs to treat binding sequences, as opposed to single binders, in an efficient way. While different methods for formalising single binder calculi have been proposed over the last decades, representations for such binding sequences are not very well explored.
The main effort in the formalisation is to keep the machine checked proofs as close to their pen-and-paper counterparts as possible. This includes treating all binding sequences as atomic elements, and creating custom induction and inversion rules that to remove the bulk of manual alpha-conversions.
This entry is described in detail in Bengtson's thesis.
notify =
[Encodability_Process_Calculi]
title = Analysing and Comparing Encodability Criteria for Process Calculi
author = Kirstin Peters , Rob van Glabbeek
date = 2015-08-10
topic = Computer science/Concurrency/Process calculi
abstract = Encodings or the proof of their absence are the main way to
compare process calculi. To analyse the quality of encodings and to rule out
trivial or meaningless encodings, they are augmented with quality
criteria. There exists a bunch of different criteria and different variants
of criteria in order to reason in different settings. This leads to
incomparable results. Moreover it is not always clear whether the criteria
used to obtain a result in a particular setting do indeed fit to this
setting. We show how to formally reason about and compare encodability
criteria by mapping them on requirements on a relation between source and
target terms that is induced by the encoding function. In particular we
analyse the common criteria full abstraction, operational correspondence,
divergence reflection, success sensitiveness, and respect of barbs; e.g. we
analyse the exact nature of the simulation relation (coupled simulation
versus bisimulation) that is induced by different variants of operational
correspondence. This way we reduce the problem of analysing or comparing
encodability criteria to the better understood problem of comparing
relations on processes.
notify = kirstin.peters@tu-berlin.de
[Circus]
title = Isabelle/Circus
author = Abderrahmane Feliachi , Burkhart Wolff , Marie-Claude Gaudel
contributors = Makarius Wenzel
date = 2012-05-27
topic = Computer science/Concurrency/Process calculi, Computer science/System description languages
abstract = The Circus specification language combines elements for complex data and behavior specifications, using an integration of Z and CSP with a refinement calculus. Its semantics is based on Hoare and He's Unifying Theories of Programming (UTP). Isabelle/Circus is a formalization of the UTP and the Circus language in Isabelle/HOL. It contains proof rules and tactic support that allows for proofs of refinement for Circus processes (involving both data and behavioral aspects).
The Isabelle/Circus environment supports a syntax for the semantic definitions which is close to textbook presentations of Circus. This article contains an extended version of corresponding VSTTE Paper together with the complete formal development of its underlying commented theories.
extra-history =
Change history:
[2014-06-05]: More polishing, shorter proofs, added Circus syntax, added Makarius Wenzel as contributor.
notify =
[Dijkstra_Shortest_Path]
title = Dijkstra's Shortest Path Algorithm
author = Benedikt Nordhoff , Peter Lammich
topic = Computer science/Algorithms/Graph
date = 2012-01-30
abstract = We implement and prove correct Dijkstra's algorithm for the
single source shortest path problem, conceived in 1956 by E. Dijkstra.
The algorithm is implemented using the data refinement framework for monadic,
nondeterministic programs. An efficient implementation is derived using data
structures from the Isabelle Collection Framework.
notify = lammich@in.tum.de
[Refine_Monadic]
title = Refinement for Monadic Programs
author = Peter Lammich
topic = Computer science/Programming languages/Logics
date = 2012-01-30
abstract = We provide a framework for program and data refinement in Isabelle/HOL.
The framework is based on a nondeterminism-monad with assertions, i.e.,
the monad carries a set of results or an assertion failure.
Recursion is expressed by fixed points. For convenience, we also provide
while and foreach combinators.
The framework provides tools to automatize canonical tasks, such as
verification condition generation, finding appropriate data refinement relations,
and refine an executable program to a form that is accepted by the
Isabelle/HOL code generator.
This submission comes with a collection of examples and a user-guide,
illustrating the usage of the framework.
extra-history =
Change history:
[2012-04-23] Introduced ordered FOREACH loops
[2012-06] New features:
REC_rule_arb and RECT_rule_arb allow for generalizing over variables.
prepare_code_thms - command extracts code equations for recursion combinators.
[2012-07] New example: Nested DFS for emptiness check of Buchi-automata with witness.
New feature:
fo_rule method to apply resolution using first-order matching. Useful for arg_conf, fun_cong.
[2012-08] Adaptation to ICF v2.
[2012-10-05] Adaptations to include support for Automatic Refinement Framework.
[2013-09] This entry now depends on Automatic Refinement
[2014-06] New feature: vc_solve method to solve verification conditions.
Maintenace changes: VCG-rules for nfoldli, improved setup for FOREACH-loops.
[2014-07] Now defining recursion via flat domain. Dropped many single-valued prerequisites.
Changed notion of data refinement. In single-valued case, this matches the old notion.
In non-single valued case, the new notion allows for more convenient rules.
In particular, the new definitions allow for projecting away ghost variables as a refinement step.
[2014-11] New features: le-or-fail relation (leof), modular reasoning about loop invariants.
notify = lammich@in.tum.de
[Refine_Imperative_HOL]
title = The Imperative Refinement Framework
author = Peter Lammich
notify = lammich@in.tum.de
date = 2016-08-08
topic = Computer science/Programming languages/Transformations,Computer science/Data structures
abstract =
We present the Imperative Refinement Framework (IRF), a tool that
supports a stepwise refinement based approach to imperative programs.
This entry is based on the material we presented in [ITP-2015,
CPP-2016]. It uses the Monadic Refinement Framework as a frontend for
the specification of the abstract programs, and Imperative/HOL as a
backend to generate executable imperative programs. The IRF comes
with tool support to synthesize imperative programs from more
abstract, functional ones, using efficient imperative implementations
for the abstract data structures. This entry also includes the
Imperative Isabelle Collection Framework (IICF), which provides a
library of re-usable imperative collection data structures. Moreover,
this entry contains a quickstart guide and a reference manual, which
provide an introduction to using the IRF for Isabelle/HOL experts. It
also provids a collection of (partly commented) practical examples,
some highlights being Dijkstra's Algorithm, Nested-DFS, and a generic
worklist algorithm with subsumption. Finally, this entry contains
benchmark scripts that compare the runtime of some examples against
reference implementations of the algorithms in Java and C++.
[ITP-2015] Peter Lammich: Refinement to Imperative/HOL. ITP 2015:
253--269 [CPP-2016] Peter Lammich: Refinement based verification of
imperative data structures. CPP 2016: 27--36
[Automatic_Refinement]
title = Automatic Data Refinement
author = Peter Lammich
topic = Computer science/Programming languages/Logics
date = 2013-10-02
abstract = We present the Autoref tool for Isabelle/HOL, which automatically
refines algorithms specified over abstract concepts like maps
and sets to algorithms over concrete implementations like red-black-trees,
and produces a refinement theorem. It is based on ideas borrowed from
relational parametricity due to Reynolds and Wadler.
The tool allows for rapid prototyping of verified, executable algorithms.
Moreover, it can be configured to fine-tune the result to the user~s needs.
Our tool is able to automatically instantiate generic algorithms, which
greatly simplifies the implementation of executable data structures.
This AFP-entry provides the basic tool, which is then used by the
Refinement and Collection Framework to provide automatic data refinement for
the nondeterminism monad and various collection datastructures.
notify = lammich@in.tum.de
[EdmondsKarp_Maxflow]
title = Formalizing the Edmonds-Karp Algorithm
author = Peter Lammich , S. Reza Sefidgar<>
notify = lammich@in.tum.de
date = 2016-08-12
topic = Computer science/Algorithms/Graph
abstract =
We present a formalization of the Ford-Fulkerson method for computing
the maximum flow in a network. Our formal proof closely follows a
standard textbook proof, and is accessible even without being an
expert in Isabelle/HOL--- the interactive theorem prover used for the
formalization. We then use stepwise refinement to obtain the
Edmonds-Karp algorithm, and formally prove a bound on its complexity.
Further refinement yields a verified implementation, whose execution
time compares well to an unverified reference implementation in Java.
This entry is based on our ITP-2016 paper with the same title.
[VerifyThis2018]
title = VerifyThis 2018 - Polished Isabelle Solutions
author = Peter Lammich , Simon Wimmer
topic = Computer science/Algorithms
date = 2018-04-27
notify = lammich@in.tum.de
abstract =
VerifyThis
2018 was a program verification competition associated with
ETAPS 2018. It was the 7th event in the VerifyThis competition series.
In this entry, we present polished and completed versions of our
solutions that we created during the competition.
[PseudoHoops]
title = Pseudo Hoops
author = George Georgescu <>, Laurentiu Leustean <>, Viorel Preoteasa
topic = Mathematics/Algebra
date = 2011-09-22
abstract = Pseudo-hoops are algebraic structures introduced by B. Bosbach under the name of complementary semigroups. In this formalization we prove some properties of pseudo-hoops and we define the basic concepts of filter and normal filter. The lattice of normal filters is isomorphic with the lattice of congruences of a pseudo-hoop. We also study some important classes of pseudo-hoops. Bounded Wajsberg pseudo-hoops are equivalent to pseudo-Wajsberg algebras and bounded basic pseudo-hoops are equivalent to pseudo-BL algebras. Some examples of pseudo-hoops are given in the last section of the formalization.
notify = viorel.preoteasa@aalto.fi
[MonoBoolTranAlgebra]
title = Algebra of Monotonic Boolean Transformers
author = Viorel Preoteasa
topic = Computer science/Programming languages/Logics
date = 2011-09-22
abstract = Algebras of imperative programming languages have been successful in reasoning about programs. In general an algebra of programs is an algebraic structure with programs as elements and with program compositions (sequential composition, choice, skip) as algebra operations. Various versions of these algebras were introduced to model partial correctness, total correctness, refinement, demonic choice, and other aspects. We formalize here an algebra which can be used to model total correctness, refinement, demonic and angelic choice. The basic model of this algebra are monotonic Boolean transformers (monotonic functions from a Boolean algebra to itself).
notify = viorel.preoteasa@aalto.fi
[LatticeProperties]
title = Lattice Properties
author = Viorel Preoteasa
topic = Mathematics/Order
date = 2011-09-22
abstract = This formalization introduces and collects some algebraic structures based on lattices and complete lattices for use in other developments. The structures introduced are modular, and lattice ordered groups. In addition to the results proved for the new lattices, this formalization also introduces theorems about latices and complete lattices in general.
extra-history =
Change history:
[2012-01-05]: Removed the theory about distributive complete lattices which is in the standard library now.
Added a theory about well founded and transitive relations and a result about fixpoints in complete lattices and well founded relations.
Moved the results about conjunctive and disjunctive functions to a new theory.
Removed the syntactic classes for inf and sup which are in the standard library now.
notify = viorel.preoteasa@aalto.fi
[Impossible_Geometry]
title = Proving the Impossibility of Trisecting an Angle and Doubling the Cube
author = Ralph Romanos , Lawrence C. Paulson
topic = Mathematics/Algebra, Mathematics/Geometry
date = 2012-08-05
abstract = Squaring the circle, doubling the cube and trisecting an angle, using a compass and straightedge alone, are classic unsolved problems first posed by the ancient Greeks. All three problems were proved to be impossible in the 19th century. The following document presents the proof of the impossibility of solving the latter two problems using Isabelle/HOL, following a proof by Carrega. The proof uses elementary methods: no Galois theory or field extensions. The set of points constructible using a compass and straightedge is defined inductively. Radical expressions, which involve only square roots and arithmetic of rational numbers, are defined, and we find that all constructive points have radical coordinates. Finally, doubling the cube and trisecting certain angles requires solving certain cubic equations that can be proved to have no rational roots. The Isabelle proofs require a great many detailed calculations.
notify = ralph.romanos@student.ecp.fr, lp15@cam.ac.uk
[IP_Addresses]
title = IP Addresses
author = Cornelius Diekmann , Julius Michaelis , Lars Hupel
notify = diekmann@net.in.tum.de
date = 2016-06-28
topic = Computer science/Networks
abstract =
This entry contains a definition of IP addresses and a library to work
with them. Generic IP addresses are modeled as machine words of
arbitrary length. Derived from this generic definition, IPv4 addresses
are 32bit machine words, IPv6 addresses are 128bit words.
Additionally, IPv4 addresses can be represented in dot-decimal
notation and IPv6 addresses in (compressed) colon-separated notation.
We support toString functions and parsers for both notations. Sets of
IP addresses can be represented with a netmask (e.g.
192.168.0.0/255.255.0.0) or in CIDR notation (e.g. 192.168.0.0/16). To
provide executable code for set operations on IP address ranges, the
library includes a datatype to work on arbitrary intervals of machine
words.
[Simple_Firewall]
title = Simple Firewall
author = Cornelius Diekmann , Julius Michaelis , Maximilian Haslbeck
notify = diekmann@net.in.tum.de, max.haslbeck@gmx.de
date = 2016-08-24
topic = Computer science/Networks
abstract =
We present a simple model of a firewall. The firewall can accept or
drop a packet and can match on interfaces, IP addresses, protocol, and
ports. It was designed to feature nice mathematical properties: The
type of match expressions was carefully crafted such that the
conjunction of two match expressions is only one match expression.
This model is too simplistic to mirror all aspects of the real world.
In the upcoming entry "Iptables Semantics", we will translate the
Linux firewall iptables to this model. For a fixed service (e.g. ssh,
http), we provide an algorithm to compute an overview of the
firewall's filtering behavior. The algorithm computes minimal service
matrices, i.e. graphs which partition the complete IPv4 and IPv6
address space and visualize the allowed accesses between partitions.
For a detailed description, see
Verified iptables Firewall
Analysis, IFIP Networking 2016.
[Iptables_Semantics]
title = Iptables Semantics
author = Cornelius Diekmann , Lars Hupel
notify = diekmann@net.in.tum.de, hupel@in.tum.de
date = 2016-09-09
topic = Computer science/Networks
abstract =
We present a big step semantics of the filtering behavior of the
Linux/netfilter iptables firewall. We provide algorithms to simplify
complex iptables rulests to a simple firewall model (c.f. AFP entry Simple_Firewall)
and to verify spoofing protection of a ruleset.
Internally, we embed our semantics into ternary logic, ultimately
supporting every iptables match condition by abstracting over
unknowns. Using this AFP entry and all entries it depends on, we
created an easy-to-use, stand-alone haskell tool called fffuu. The tool does not
require any input —except for the iptables-save dump of
the analyzed firewall— and presents interesting results about
the user's ruleset. Real-Word firewall errors have been uncovered, and
the correctness of rulesets has been proved, with the help of
our tool.
[Routing]
title = Routing
author = Julius Michaelis , Cornelius Diekmann
notify = afp@liftm.de
date = 2016-08-31
topic = Computer science/Networks
abstract =
This entry contains definitions for routing with routing
tables/longest prefix matching. A routing table entry is modelled as
a record of a prefix match, a metric, an output port, and an optional
next hop. A routing table is a list of entries, sorted by prefix
length and metric. Additionally, a parser and serializer for the
output of the ip-route command, a function to create a relation from
output port to corresponding destination IP space, and a model of a
Linux-style router are included.
[KBPs]
title = Knowledge-based programs
author = Peter Gammie
topic = Computer science/Automata and formal languages
date = 2011-05-17
abstract = Knowledge-based programs (KBPs) are a formalism for directly relating agents' knowledge and behaviour. Here we present a general scheme for compiling KBPs to executable automata with a proof of correctness in Isabelle/HOL. We develop the algorithm top-down, using Isabelle's locale mechanism to structure these proofs, and show that two classic examples can be synthesised using Isabelle's code generator.
extra-history =
Change history:
[2012-03-06]: Add some more views and revive the code generation.
notify = kleing@cse.unsw.edu.au
[Tarskis_Geometry]
title = The independence of Tarski's Euclidean axiom
author = T. J. M. Makarios
topic = Mathematics/Geometry
date = 2012-10-30
abstract =
Tarski's axioms of plane geometry are formalized and, using the standard
real Cartesian model, shown to be consistent. A substantial theory of
the projective plane is developed. Building on this theory, the
Klein-Beltrami model of the hyperbolic plane is defined and shown to
satisfy all of Tarski's axioms except his Euclidean axiom; thus Tarski's
Euclidean axiom is shown to be independent of his other axioms of plane
geometry.
An earlier version of this work was the subject of the author's
MSc thesis,
which contains natural-language explanations of some of the
more interesting proofs.
notify = tjm1983@gmail.com
[General-Triangle]
title = The General Triangle Is Unique
author = Joachim Breitner
topic = Mathematics/Geometry
date = 2011-04-01
abstract = Some acute-angled triangles are special, e.g. right-angled or isoscele triangles. Some are not of this kind, but, without measuring angles, look as if they were. In that sense, there is exactly one general triangle. This well-known fact is proven here formally.
notify = mail@joachim-breitner.de
[LightweightJava]
title = Lightweight Java
author = Rok Strniša , Matthew Parkinson
topic = Computer science/Programming languages/Language definitions
date = 2011-02-07
abstract = A fully-formalized and extensible minimal imperative fragment of Java.
notify = rok@strnisa.com
[Lower_Semicontinuous]
title = Lower Semicontinuous Functions
author = Bogdan Grechuk
topic = Mathematics/Analysis
date = 2011-01-08
abstract = We define the notions of lower and upper semicontinuity for functions from a metric space to the extended real line. We prove that a function is both lower and upper semicontinuous if and only if it is continuous. We also give several equivalent characterizations of lower semicontinuity. In particular, we prove that a function is lower semicontinuous if and only if its epigraph is a closed set. Also, we introduce the notion of the lower semicontinuous hull of an arbitrary function and prove its basic properties.
notify = hoelzl@in.tum.de
[RIPEMD-160-SPARK]
title = RIPEMD-160
author = Fabian Immler
topic = Computer science/Programming languages/Static analysis
date = 2011-01-10
abstract = This work presents a verification of an implementation in SPARK/ADA of the cryptographic hash-function RIPEMD-160. A functional specification of RIPEMD-160 is given in Isabelle/HOL. Proofs for the verification conditions generated by the static-analysis toolset of SPARK certify the functional correctness of the implementation.
extra-history =
Change history:
[2015-11-09]: Entry is now obsolete, moved to Isabelle distribution.
notify = immler@in.tum.de
[Regular-Sets]
title = Regular Sets and Expressions
author = Alexander Krauss , Tobias Nipkow
contributors = Manuel Eberl
topic = Computer science/Automata and formal languages
date = 2010-05-12
abstract = This is a library of constructions on regular expressions and languages. It provides the operations of concatenation, Kleene star and derivative on languages. Regular expressions and their meaning are defined. An executable equivalence checker for regular expressions is verified; it does not need automata but works directly on regular expressions. By mapping regular expressions to binary relations, an automatic and complete proof method for (in)equalities of binary relations over union, concatenation and (reflexive) transitive closure is obtained. Extended regular expressions with complement and intersection are also defined and an equivalence checker is provided.
extra-history =
Change history:
[2011-08-26]: Christian Urban added a theory about derivatives and partial derivatives of regular expressions
[2012-05-10]: Tobias Nipkow added extended regular expressions
[2012-05-10]: Tobias Nipkow added equivalence checking with partial derivatives
notify = nipkow@in.tum.de, krauss@in.tum.de, christian.urban@kcl.ac.uk
[Regex_Equivalence]
title = Unified Decision Procedures for Regular Expression Equivalence
author = Tobias Nipkow , Dmitriy Traytel
topic = Computer science/Automata and formal languages
date = 2014-01-30
abstract =
We formalize a unified framework for verified decision procedures for regular
expression equivalence. Five recently published formalizations of such
decision procedures (three based on derivatives, two on marked regular
expressions) can be obtained as instances of the framework. We discover that
the two approaches based on marked regular expressions, which were previously
thought to be the same, are different, and one seems to produce uniformly
smaller automata. The common framework makes it possible to compare the
performance of the different decision procedures in a meaningful way.
The formalization is described in a paper of the same name presented at
Interactive Theorem Proving 2014.
notify = nipkow@in.tum.de, traytel@in.tum.de
[MSO_Regex_Equivalence]
title = Decision Procedures for MSO on Words Based on Derivatives of Regular Expressions
author = Dmitriy Traytel , Tobias Nipkow
topic = Computer science/Automata and formal languages, Logic/General logic/Decidability of theories
date = 2014-06-12
abstract =
Monadic second-order logic on finite words (MSO) is a decidable yet
expressive logic into which many decision problems can be encoded. Since MSO
formulas correspond to regular languages, equivalence of MSO formulas can be
reduced to the equivalence of some regular structures (e.g. automata). We
verify an executable decision procedure for MSO formulas that is not based
on automata but on regular expressions.
Decision procedures for regular expression equivalence have been formalized
before, usually based on Brzozowski derivatives. Yet, for a straightforward
embedding of MSO formulas into regular expressions an extension of regular
expressions with a projection operation is required. We prove total
correctness and completeness of an equivalence checker for regular
expressions extended in that way. We also define a language-preserving
translation of formulas into regular expressions with respect to two
different semantics of MSO.
The formalization is described in this ICFP 2013 functional pearl.
notify = traytel@in.tum.de, nipkow@in.tum.de
[Formula_Derivatives]
title = Derivatives of Logical Formulas
author = Dmitriy Traytel
topic = Computer science/Automata and formal languages, Logic/General logic/Decidability of theories
date = 2015-05-28
abstract =
We formalize new decision procedures for WS1S, M2L(Str), and Presburger
Arithmetics. Formulas of these logics denote regular languages. Unlike
traditional decision procedures, we do not translate formulas into automata
(nor into regular expressions), at least not explicitly. Instead we devise
notions of derivatives (inspired by Brzozowski derivatives for regular
expressions) that operate on formulas directly and compute a syntactic
bisimulation using these derivatives. The treatment of Boolean connectives and
quantifiers is uniform for all mentioned logics and is abstracted into a
locale. This locale is then instantiated by different atomic formulas and their
derivatives (which may differ even for the same logic under different encodings
of interpretations as formal words).
The WS1S instance is described in the draft paper A
Coalgebraic Decision Procedure for WS1S by the author.
notify = traytel@in.tum.de
[Myhill-Nerode]
title = The Myhill-Nerode Theorem Based on Regular Expressions
author = Chunhan Wu <>, Xingyuan Zhang <>, Christian Urban
contributors = Manuel Eberl
topic = Computer science/Automata and formal languages
date = 2011-08-26
abstract = There are many proofs of the Myhill-Nerode theorem using automata. In this library we give a proof entirely based on regular expressions, since regularity of languages can be conveniently defined using regular expressions (it is more painful in HOL to define regularity in terms of automata). We prove the first direction of the Myhill-Nerode theorem by solving equational systems that involve regular expressions. For the second direction we give two proofs: one using tagging-functions and another using partial derivatives. We also establish various closure properties of regular languages. Most details of the theories are described in our ITP 2011 paper.
notify = christian.urban@kcl.ac.uk
[Universal_Turing_Machine]
title = Universal Turing Machine
author = Jian Xu<>, Xingyuan Zhang<>, Christian Urban , Sebastiaan J. C. Joosten
topic = Logic/Computability, Computer science/Automata and formal languages
date = 2019-02-08
notify = sjcjoosten@gmail.com, christian.urban@kcl.ac.uk
abstract =
We formalise results from computability theory: recursive functions,
undecidability of the halting problem, and the existence of a
universal Turing machine. This formalisation is the AFP entry
corresponding to the paper Mechanising Turing Machines and Computability Theory
in Isabelle/HOL, ITP 2013.
[CYK]
title = A formalisation of the Cocke-Younger-Kasami algorithm
author = Maksym Bortin
date = 2016-04-27
topic = Computer science/Algorithms, Computer science/Automata and formal languages
abstract =
The theory provides a formalisation of the Cocke-Younger-Kasami
algorithm (CYK for short), an approach to solving the word problem
for context-free languages. CYK decides if a word is in the
languages generated by a context-free grammar in Chomsky normal form.
The formalized algorithm is executable.
notify = maksym.bortin@nicta.com.au
[Boolean_Expression_Checkers]
title = Boolean Expression Checkers
author = Tobias Nipkow
date = 2014-06-08
topic = Computer science/Algorithms, Logic/General logic/Mechanization of proofs
abstract =
This entry provides executable checkers for the following properties of
boolean expressions: satisfiability, tautology and equivalence. Internally,
the checkers operate on binary decision trees and are reasonably efficient
(for purely functional algorithms).
extra-history =
Change history: [2015-09-23]: Salomon Sickert added an interface that does not require the usage of the Boolean formula datatype. Furthermore the general Mapping type is used instead of an association list.
notify = nipkow@in.tum.de
[Presburger-Automata]
title = Formalizing the Logic-Automaton Connection
author = Stefan Berghofer , Markus Reiter <>
date = 2009-12-03
topic = Computer science/Automata and formal languages, Logic/General logic/Decidability of theories
abstract = This work presents a formalization of a library for automata on bit strings. It forms the basis of a reflection-based decision procedure for Presburger arithmetic, which is efficiently executable thanks to Isabelle's code generator. With this work, we therefore provide a mechanized proof of a well-known connection between logic and automata theory. The formalization is also described in a publication [TPHOLs 2009].
notify = berghofe@in.tum.de
[Functional-Automata]
title = Functional Automata
author = Tobias Nipkow
date = 2004-03-30
topic = Computer science/Automata and formal languages
abstract = This theory defines deterministic and nondeterministic automata in a functional representation: the transition function/relation and the finality predicate are just functions. Hence the state space may be infinite. It is shown how to convert regular expressions into such automata. A scanner (generator) is implemented with the help of functional automata: the scanner chops the input up into longest recognized substrings. Finally we also show how to convert a certain subclass of functional automata (essentially the finite deterministic ones) into regular sets.
notify = nipkow@in.tum.de
[Statecharts]
title = Formalizing Statecharts using Hierarchical Automata
author = Steffen Helke , Florian Kammüller
topic = Computer science/Automata and formal languages
date = 2010-08-08
abstract = We formalize in Isabelle/HOL the abtract syntax and a synchronous
step semantics for the specification language Statecharts. The formalization
is based on Hierarchical Automata which allow a structural decomposition of
Statecharts into Sequential Automata. To support the composition of
Statecharts, we introduce calculating operators to construct a Hierarchical
Automaton in a stepwise manner. Furthermore, we present a complete semantics
of Statecharts including a theory of data spaces, which enables the modelling
of racing effects. We also adapt CTL for
Statecharts to build a bridge for future combinations with model
checking. However the main motivation of this work is to provide a sound and
complete basis for reasoning on Statecharts. As a central meta theorem we
prove that the well-formedness of a Statechart is preserved by the semantics.
notify = nipkow@in.tum.de
[Stuttering_Equivalence]
title = Stuttering Equivalence
author = Stephan Merz
topic = Computer science/Automata and formal languages
date = 2012-05-07
abstract = Two omega-sequences are stuttering equivalent if they differ only by finite repetitions of elements. Stuttering equivalence is a fundamental concept in the theory of concurrent and distributed systems. Notably, Lamport argues that refinement notions for such systems should be insensitive to finite stuttering. Peled and Wilke showed that all PLTL (propositional linear-time temporal logic) properties that are insensitive to stuttering equivalence can be expressed without the next-time operator. Stuttering equivalence is also important for certain verification techniques such as partial-order reduction for model checking.
We formalize stuttering equivalence in Isabelle/HOL. Our development relies on the notion of stuttering sampling functions that may skip blocks of identical sequence elements. We also encode PLTL and prove the theorem due to Peled and Wilke.
extra-history =
Change history:
[2013-01-31]: Added encoding of PLTL and proved Peled and Wilke's theorem. Adjusted abstract accordingly.
notify = Stephan.Merz@loria.fr
[Coinductive_Languages]
title = A Codatatype of Formal Languages
author = Dmitriy Traytel
topic = Computer science/Automata and formal languages
date = 2013-11-15
abstract = We define formal languages as a codataype of infinite trees
branching over the alphabet. Each node in such a tree indicates whether the
path to this node constitutes a word inside or outside of the language. This
codatatype is isormorphic to the set of lists representation of languages,
but caters for definitions by corecursion and proofs by coinduction.
Regular operations on languages are then defined by primitive corecursion.
A difficulty arises here, since the standard definitions of concatenation and
iteration from the coalgebraic literature are not primitively
corecursive-they require guardedness up-to union/concatenation.
Without support for up-to corecursion, these operation must be defined as a
composition of primitive ones (and proved being equal to the standard
definitions). As an exercise in coinduction we also prove the axioms of
Kleene algebra for the defined regular operations.
Furthermore, a language for context-free grammars given by productions in
Greibach normal form and an initial nonterminal is constructed by primitive
corecursion, yielding an executable decision procedure for the word problem
without further ado.
notify = traytel@in.tum.de
[Tree-Automata]
title = Tree Automata
author = Peter Lammich
date = 2009-11-25
topic = Computer science/Automata and formal languages
abstract = This work presents a machine-checked tree automata library for Standard-ML, OCaml and Haskell. The algorithms are efficient by using appropriate data structures like RB-trees. The available algorithms for non-deterministic automata include membership query, reduction, intersection, union, and emptiness check with computation of a witness for non-emptiness. The executable algorithms are derived from less-concrete, non-executable algorithms using data-refinement techniques. The concrete data structures are from the Isabelle Collections Framework. Moreover, this work contains a formalization of the class of tree-regular languages and its closure properties under set operations.
notify = peter.lammich@uni-muenster.de, nipkow@in.tum.de
[Depth-First-Search]
title = Depth First Search
author = Toshiaki Nishihara <>, Yasuhiko Minamide <>
date = 2004-06-24
topic = Computer science/Algorithms/Graph
abstract = Depth-first search of a graph is formalized with recdef. It is shown that it visits all of the reachable nodes from a given list of nodes. Executable ML code of depth-first search is obtained using the code generation feature of Isabelle/HOL.
notify = lp15@cam.ac.uk, krauss@in.tum.de
[FFT]
title = Fast Fourier Transform
author = Clemens Ballarin
date = 2005-10-12
topic = Computer science/Algorithms/Mathematical
abstract = We formalise a functional implementation of the FFT algorithm over the complex numbers, and its inverse. Both are shown equivalent to the usual definitions of these operations through Vandermonde matrices. They are also shown to be inverse to each other, more precisely, that composition of the inverse and the transformation yield the identity up to a scalar.
notify = ballarin@in.tum.de
[Gauss-Jordan-Elim-Fun]
title = Gauss-Jordan Elimination for Matrices Represented as Functions
author = Tobias Nipkow
date = 2011-08-19
topic = Computer science/Algorithms/Mathematical, Mathematics/Algebra
abstract = This theory provides a compact formulation of Gauss-Jordan elimination for matrices represented as functions. Its distinctive feature is succinctness. It is not meant for large computations.
notify = nipkow@in.tum.de
[UpDown_Scheme]
title = Verification of the UpDown Scheme
author = Johannes Hölzl
date = 2015-01-28
topic = Computer science/Algorithms/Mathematical
abstract =
The UpDown scheme is a recursive scheme used to compute the stiffness matrix
on a special form of sparse grids. Usually, when discretizing a Euclidean
space of dimension d we need O(n^d) points, for n points along each dimension.
Sparse grids are a hierarchical representation where the number of points is
reduced to O(n * log(n)^d). One disadvantage of such sparse grids is that the
algorithm now operate recursively in the dimensions and levels of the sparse grid.
The UpDown scheme allows us to compute the stiffness matrix on such a sparse
grid. The stiffness matrix represents the influence of each representation
function on the L^2 scalar product. For a detailed description see
Dirk Pflüger's PhD thesis. This formalization was developed as an
interdisciplinary project (IDP) at the Technische Universität München.
notify = hoelzl@in.tum.de
[GraphMarkingIBP]
title = Verification of the Deutsch-Schorr-Waite Graph Marking Algorithm using Data Refinement
author = Viorel Preoteasa , Ralph-Johan Back
date = 2010-05-28
topic = Computer science/Algorithms/Graph
abstract = The verification of the Deutsch-Schorr-Waite graph marking algorithm is used as a benchmark in many formalizations of pointer programs. The main purpose of this mechanization is to show how data refinement of invariant based programs can be used in verifying practical algorithms. The verification starts with an abstract algorithm working on a graph given by a relation next on nodes. Gradually the abstract program is refined into Deutsch-Schorr-Waite graph marking algorithm where only one bit per graph node of additional memory is used for marking.
extra-history =
Change history:
[2012-01-05]: Updated for the new definition of data refinement and the new syntax for demonic and angelic update statements
notify = viorel.preoteasa@aalto.fi
[Efficient-Mergesort]
title = Efficient Mergesort
topic = Computer science/Algorithms
date = 2011-11-09
author = Christian Sternagel
abstract = We provide a formalization of the mergesort algorithm as used in GHC's Data.List module, proving correctness and stability. Furthermore, experimental data suggests that generated (Haskell-)code for this algorithm is much faster than for previous algorithms available in the Isabelle distribution.
extra-history =
Change history:
[2012-10-24]:
Added reference to journal article.
[2018-09-17]:
Added theory Efficient_Mergesort that works exclusively with the mutual
induction schemas generated by the function package.
[2018-09-19]:
Added theory Mergesort_Complexity that proves an upper bound on the number of
comparisons that are required by mergesort.
[2018-09-19]:
Theory Efficient_Mergesort replaces theory Efficient_Sort but keeping the old
name Efficient_Sort.
notify = c.sternagel@gmail.com
[SATSolverVerification]
title = Formal Verification of Modern SAT Solvers
author = Filip Marić
date = 2008-07-23
topic = Computer science/Algorithms
abstract = This document contains formal correctness proofs of modern SAT solvers. Following (Krstic et al, 2007) and (Nieuwenhuis et al., 2006), solvers are described using state-transition systems. Several different SAT solver descriptions are given and their partial correctness and termination is proved. These include: - a solver based on classical DPLL procedure (using only a backtrack-search with unit propagation),
- a very general solver with backjumping and learning (similar to the description given in (Nieuwenhuis et al., 2006)), and
- a solver with a specific conflict analysis algorithm (similar to the description given in (Krstic et al., 2007)).
Within the SAT solver correctness proofs, a large number of lemmas about propositional logic and CNF formulae are proved. This theory is self-contained and could be used for further exploring of properties of CNF based SAT algorithms.
notify =
[Transitive-Closure]
title = Executable Transitive Closures of Finite Relations
topic = Computer science/Algorithms/Graph
date = 2011-03-14
author = Christian Sternagel , René Thiemann
license = LGPL
abstract = We provide a generic work-list algorithm to compute the transitive closure of finite relations where only successors of newly detected states are generated. This algorithm is then instantiated for lists over arbitrary carriers and red black trees (which are faster but require a linear order on the carrier), respectively. Our formalization was performed as part of the IsaFoR/CeTA project where reflexive transitive closures of large tree automata have to be computed.
extra-history =
Change history:
[2014-09-04] added example simprocs in Finite_Transitive_Closure_Simprocs
notify = c.sternagel@gmail.com, rene.thiemann@uibk.ac.at
[Transitive-Closure-II]
title = Executable Transitive Closures
topic = Computer science/Algorithms/Graph
date = 2012-02-29
author = René Thiemann
license = LGPL
abstract =
We provide a generic work-list algorithm to compute the
(reflexive-)transitive closure of relations where only successors of newly
detected states are generated.
In contrast to our previous work, the relations do not have to be finite,
but each element must only have finitely many (indirect) successors.
Moreover, a subsumption relation can be used instead of pure equality.
An executable variant of the algorithm is available where the generic operations
are instantiated with list operations.
This formalization was performed as part of the IsaFoR/CeTA project,
and it has been used to certify size-change
termination proofs where large transitive closures have to be computed.
notify = rene.thiemann@uibk.ac.at
[MuchAdoAboutTwo]
title = Much Ado About Two
author = Sascha Böhme
date = 2007-11-06
topic = Computer science/Algorithms
abstract = This article is an Isabelle formalisation of a paper with the same title. In a similar way as Knuth's 0-1-principle for sorting algorithms, that paper develops a 0-1-2-principle for parallel prefix computations.
notify = boehmes@in.tum.de
[DiskPaxos]
title = Proving the Correctness of Disk Paxos
date = 2005-06-22
author = Mauro Jaskelioff , Stephan Merz
topic = Computer science/Algorithms/Distributed
abstract = Disk Paxos is an algorithm for building arbitrary fault-tolerant distributed systems. The specification of Disk Paxos has been proved correct informally and tested using the TLC model checker, but up to now, it has never been fully formally verified. In this work we have formally verified its correctness using the Isabelle theorem prover and the HOL logic system, showing that Isabelle is a practical tool for verifying properties of TLA+ specifications.
notify = kleing@cse.unsw.edu.au
[GenClock]
title = Formalization of a Generalized Protocol for Clock Synchronization
author = Alwen Tiu
date = 2005-06-24
topic = Computer science/Algorithms/Distributed
abstract = We formalize the generalized Byzantine fault-tolerant clock synchronization protocol of Schneider. This protocol abstracts from particular algorithms or implementations for clock synchronization. This abstraction includes several assumptions on the behaviors of physical clocks and on general properties of concrete algorithms/implementations. Based on these assumptions the correctness of the protocol is proved by Schneider. His proof was later verified by Shankar using the theorem prover EHDM (precursor to PVS). Our formalization in Isabelle/HOL is based on Shankar's formalization.
notify = kleing@cse.unsw.edu.au
[ClockSynchInst]
title = Instances of Schneider's generalized protocol of clock synchronization
author = Damián Barsotti
date = 2006-03-15
topic = Computer science/Algorithms/Distributed
abstract = F. B. Schneider ("Understanding protocols for Byzantine clock synchronization") generalizes a number of protocols for Byzantine fault-tolerant clock synchronization and presents a uniform proof for their correctness. In Schneider's schema, each processor maintains a local clock by periodically adjusting each value to one computed by a convergence function applied to the readings of all the clocks. Then, correctness of an algorithm, i.e. that the readings of two clocks at any time are within a fixed bound of each other, is based upon some conditions on the convergence function. To prove that a particular clock synchronization algorithm is correct it suffices to show that the convergence function used by the algorithm meets Schneider's conditions. Using the theorem prover Isabelle, we formalize the proofs that the convergence functions of two algorithms, namely, the Interactive Convergence Algorithm (ICA) of Lamport and Melliar-Smith and the Fault-tolerant Midpoint algorithm of Lundelius-Lynch, meet Schneider's conditions. Furthermore, we experiment on handling some parts of the proofs with fully automatic tools like ICS and CVC-lite. These theories are part of a joint work with Alwen Tiu and Leonor P. Nieto "Verification of Clock Synchronization Algorithms: Experiments on a combination of deductive tools" in proceedings of AVOCS 2005. In this work the correctness of Schneider schema was also verified using Isabelle (entry GenClock in AFP).
notify = kleing@cse.unsw.edu.au
[Heard_Of]
title = Verifying Fault-Tolerant Distributed Algorithms in the Heard-Of Model
date = 2012-07-27
author = Henri Debrat , Stephan Merz
topic = Computer science/Algorithms/Distributed
abstract =
Distributed computing is inherently based on replication, promising
increased tolerance to failures of individual computing nodes or
communication channels. Realizing this promise, however, involves
quite subtle algorithmic mechanisms, and requires precise statements
about the kinds and numbers of faults that an algorithm tolerates (such
as process crashes, communication faults or corrupted values). The
landmark theorem due to Fischer, Lynch, and Paterson shows that it is
impossible to achieve Consensus among N asynchronously communicating
nodes in the presence of even a single permanent failure. Existing
solutions must rely on assumptions of "partial synchrony".
Indeed, there have been numerous misunderstandings on what exactly a given
algorithm is supposed to realize in what kinds of environments. Moreover, the
abundance of subtly different computational models complicates comparisons
between different algorithms. Charron-Bost and Schiper introduced the Heard-Of
model for representing algorithms and failure assumptions in a uniform
framework, simplifying comparisons between algorithms.
In this contribution, we represent the Heard-Of model in Isabelle/HOL. We define
two semantics of runs of algorithms with different unit of atomicity and relate
these through a reduction theorem that allows us to verify algorithms in the
coarse-grained semantics (where proofs are easier) and infer their correctness
for the fine-grained one (which corresponds to actual executions). We
instantiate the framework by verifying six Consensus algorithms that differ in
the underlying algorithmic mechanisms and the kinds of faults they tolerate.
notify = Stephan.Merz@loria.fr
[Consensus_Refined]
title = Consensus Refined
date = 2015-03-18
author = Ognjen Maric <>, Christoph Sprenger
topic = Computer science/Algorithms/Distributed
abstract =
Algorithms for solving the consensus problem are fundamental to
distributed computing. Despite their brevity, their
ability to operate in concurrent, asynchronous and failure-prone
environments comes at the cost of complex and subtle
behaviors. Accordingly, understanding how they work and proving
their correctness is a non-trivial endeavor where abstraction
is immensely helpful.
Moreover, research on consensus has yielded a large number of
algorithms, many of which appear to share common algorithmic
ideas. A natural question is whether and how these similarities can
be distilled and described in a precise, unified way.
In this work, we combine stepwise refinement and
lockstep models to provide an abstract and unified
view of a sizeable family of consensus algorithms. Our models
provide insights into the design choices underlying the different
algorithms, and classify them based on those choices.
notify = sprenger@inf.ethz.ch
[Key_Agreement_Strong_Adversaries]
title = Refining Authenticated Key Agreement with Strong Adversaries
author = Joseph Lallemand , Christoph Sprenger
topic = Computer science/Security
license = LGPL
date = 2017-01-31
notify = joseph.lallemand@loria.fr, sprenger@inf.ethz.ch
abstract =
We develop a family of key agreement protocols that are correct by
construction. Our work substantially extends prior work on developing
security protocols by refinement. First, we strengthen the adversary
by allowing him to compromise different resources of protocol
participants, such as their long-term keys or their session keys. This
enables the systematic development of protocols that ensure strong
properties such as perfect forward secrecy. Second, we broaden the
class of protocols supported to include those with non-atomic keys and
equationally defined cryptographic operators. We use these extensions
to develop key agreement protocols including signed Diffie-Hellman and
the core of IKEv1 and SKEME.
[Security_Protocol_Refinement]
title = Developing Security Protocols by Refinement
author = Christoph Sprenger , Ivano Somaini<>
topic = Computer science/Security
license = LGPL
date = 2017-05-24
notify = sprenger@inf.ethz.ch
abstract =
We propose a development method for security protocols based on
stepwise refinement. Our refinement strategy transforms abstract
security goals into protocols that are secure when operating over an
insecure channel controlled by a Dolev-Yao-style intruder. As
intermediate levels of abstraction, we employ messageless guard
protocols and channel protocols communicating over channels with
security properties. These abstractions provide insights on why
protocols are secure and foster the development of families of
protocols sharing common structure and properties. We have implemented
our method in Isabelle/HOL and used it to develop different entity
authentication and key establishment protocols, including realistic
features such as key confirmation, replay caches, and encrypted
tickets. Our development highlights that guard protocols and channel
protocols provide fundamental abstractions for bridging the gap
between security properties and standard protocol descriptions based
on cryptographic messages. It also shows that our refinement approach
scales to protocols of nontrivial size and complexity.
[Abortable_Linearizable_Modules]
title = Abortable Linearizable Modules
author = Rachid Guerraoui , Viktor Kuncak , Giuliano Losa
date = 2012-03-01
topic = Computer science/Algorithms/Distributed
abstract =
We define the Abortable Linearizable Module automaton (ALM for short)
and prove its key composition property using the IOA theory of
HOLCF. The ALM is at the heart of the Speculative Linearizability
framework. This framework simplifies devising correct speculative
algorithms by enabling their decomposition into independent modules
that can be analyzed and proved correct in isolation. It is
particularly useful when working in a distributed environment, where
the need to tolerate faults and asynchrony has made current
monolithic protocols so intricate that it is no longer tractable to
check their correctness. Our theory contains a typical example of a
refinement proof in the I/O-automata framework of Lynch and Tuttle.
notify = giuliano@losa.fr, nipkow@in.tum.de
[Amortized_Complexity]
title = Amortized Complexity Verified
author = Tobias Nipkow
date = 2014-07-07
topic = Computer science/Data structures
abstract =
A framework for the analysis of the amortized complexity of functional
data structures is formalized in Isabelle/HOL and applied to a number of
standard examples and to the folowing non-trivial ones: skew heaps,
splay trees, splay heaps and pairing heaps.
A preliminary version of this work (without pairing heaps) is described
in a paper
published in the proceedings of the conference on Interactive
Theorem Proving ITP 2015. An extended version of this publication
is available here.
extra-history =
Change history:
[2015-03-17]: Added pairing heaps by Hauke Brinkop.
[2016-07-12]: Moved splay heaps from here to Splay_Tree
[2016-07-14]: Moved pairing heaps from here to the new Pairing_Heap
notify = nipkow@in.tum.de
[Dynamic_Tables]
title = Parameterized Dynamic Tables
author = Tobias Nipkow
date = 2015-06-07
topic = Computer science/Data structures
abstract =
This article formalizes the amortized analysis of dynamic tables
parameterized with their minimal and maximal load factors and the
expansion and contraction factors.
A full description is found in a
companion paper.
notify = nipkow@in.tum.de
[AVL-Trees]
title = AVL Trees
author = Tobias Nipkow , Cornelia Pusch <>
date = 2004-03-19
topic = Computer science/Data structures
abstract = Two formalizations of AVL trees with room for extensions. The first formalization is monolithic and shorter, the second one in two stages, longer and a bit simpler. The final implementation is the same. If you are interested in developing this further, please contact gerwin.klein@nicta.com.au.
extra-history =
Change history:
[2011-04-11]: Ondrej Kuncar added delete function
notify = kleing@cse.unsw.edu.au
[BDD]
title = BDD Normalisation
author = Veronika Ortner <>, Norbert Schirmer <>
date = 2008-02-29
topic = Computer science/Data structures
abstract = We present the verification of the normalisation of a binary decision diagram (BDD). The normalisation follows the original algorithm presented by Bryant in 1986 and transforms an ordered BDD in a reduced, ordered and shared BDD. The verification is based on Hoare logics.
notify = kleing@cse.unsw.edu.au, norbert.schirmer@web.de
[BinarySearchTree]
title = Binary Search Trees
author = Viktor Kuncak
date = 2004-04-05
topic = Computer science/Data structures
abstract = The correctness is shown of binary search tree operations (lookup, insert and remove) implementing a set. Two versions are given, for both structured and linear (tactic-style) proofs. An implementation of integer-indexed maps is also verified.
notify = lp15@cam.ac.uk
[Splay_Tree]
title = Splay Tree
author = Tobias Nipkow
notify = nipkow@in.tum.de
date = 2014-08-12
topic = Computer science/Data structures
abstract =
Splay trees are self-adjusting binary search trees which were invented by Sleator and Tarjan [JACM 1985].
This entry provides executable and verified functional splay trees
as well as the related splay heaps (due to Okasaki).
The amortized complexity of splay trees and heaps is analyzed in the AFP entry
Amortized Complexity.
extra-history =
Change history:
[2016-07-12]: Moved splay heaps here from Amortized_Complexity
[Root_Balanced_Tree]
title = Root-Balanced Tree
author = Tobias Nipkow
notify = nipkow@in.tum.de
date = 2017-08-20
topic = Computer science/Data structures
abstract =
Andersson introduced general balanced trees,
search trees based on the design principle of partial rebuilding:
perform update operations naively until the tree becomes too
unbalanced, at which point a whole subtree is rebalanced. This article
defines and analyzes a functional version of general balanced trees,
which we call root-balanced trees. Using a lightweight model
of execution time, amortized logarithmic complexity is verified in
the theorem prover Isabelle.
This is the Isabelle formalization of the material decribed in the APLAS 2017 article
Verified Root-Balanced Trees
by the same author, which also presents experimental results that show
competitiveness of root-balanced with AVL and red-black trees.
[Skew_Heap]
title = Skew Heap
author = Tobias Nipkow
date = 2014-08-13
topic = Computer science/Data structures
abstract =
Skew heaps are an amazingly simple and lightweight implementation of
priority queues. They were invented by Sleator and Tarjan [SIAM 1986]
and have logarithmic amortized complexity. This entry provides executable
and verified functional skew heaps.
The amortized complexity of skew heaps is analyzed in the AFP entry
Amortized Complexity.
notify = nipkow@in.tum.de
[Pairing_Heap]
title = Pairing Heap
author = Hauke Brinkop , Tobias Nipkow
date = 2016-07-14
topic = Computer science/Data structures
abstract =
This library defines three different versions of pairing heaps: a
functional version of the original design based on binary
trees [Fredman et al. 1986], the version by Okasaki [1998] and
a modified version of the latter that is free of structural invariants.
The amortized complexity of pairing heaps is analyzed in the AFP article
Amortized Complexity.
extra-0 = Origin: This library was extracted from Amortized Complexity and extended.
notify = nipkow@in.tum.de
[Priority_Queue_Braun]
title = Priority Queues Based on Braun Trees
author = Tobias Nipkow
date = 2014-09-04
topic = Computer science/Data structures
abstract =
This entry verifies priority queues based on Braun trees. Insertion
and deletion take logarithmic time and preserve the balanced nature
of Braun trees. Two implementations of deletion are provided.
notify = nipkow@in.tum.de
extra-history =
Change history:
[2019-12-16]: Added theory Priority_Queue_Braun2 with second version of del_min
[Binomial-Queues]
title = Functional Binomial Queues
author = René Neumann
date = 2010-10-28
topic = Computer science/Data structures
abstract = Priority queues are an important data structure and efficient implementations of them are crucial. We implement a functional variant of binomial queues in Isabelle/HOL and show its functional correctness. A verification against an abstract reference specification of priority queues has also been attempted, but could not be achieved to the full extent.
notify = florian.haftmann@informatik.tu-muenchen.de
[Binomial-Heaps]
title = Binomial Heaps and Skew Binomial Heaps
author = Rene Meis , Finn Nielsen , Peter Lammich
date = 2010-10-28
topic = Computer science/Data structures
abstract =
We implement and prove correct binomial heaps and skew binomial heaps.
Both are data-structures for priority queues.
While binomial heaps have logarithmic findMin, deleteMin,
insert, and meld operations,
skew binomial heaps have constant time findMin, insert,
and meld operations, and only the deleteMin-operation is
logarithmic. This is achieved by using skew links to avoid
cascading linking on insert-operations, and data-structural
bootstrapping to get constant-time findMin and meld
operations. Our implementation follows the paper by Brodal and Okasaki.
notify = peter.lammich@uni-muenster.de
[Finger-Trees]
title = Finger Trees
author = Benedikt Nordhoff , Stefan Körner , Peter Lammich
date = 2010-10-28
topic = Computer science/Data structures
abstract =
We implement and prove correct 2-3 finger trees.
Finger trees are a general purpose data structure, that can be used to
efficiently implement other data structures, such as priority queues.
Intuitively, a finger tree is an annotated sequence, where the annotations are
elements of a monoid. Apart from operations to access the ends of the sequence,
the main operation is to split the sequence at the point where a
monotone predicate over the sum of the left part of the sequence
becomes true for the first time.
The implementation follows the paper of Hinze and Paterson.
The code generator can be used to get efficient, verified code.
notify = peter.lammich@uni-muenster.de
[Trie]
title = Trie
author = Andreas Lochbihler , Tobias Nipkow
date = 2015-03-30
topic = Computer science/Data structures
abstract =
This article formalizes the ``trie'' data structure invented by
Fredkin [CACM 1960]. It also provides a specialization where the entries
in the trie are lists.
extra-0 =
Origin: This article was extracted from existing articles by the authors.
notify = nipkow@in.tum.de
[FinFun]
title = Code Generation for Functions as Data
author = Andreas Lochbihler
date = 2009-05-06
topic = Computer science/Data structures
abstract = FinFuns are total functions that are constant except for a finite set of points, i.e. a generalisation of finite maps. They are formalised as a new type in Isabelle/HOL such that the code generator can handle equality tests and quantification on FinFuns. On the code output level, FinFuns are explicitly represented by constant functions and pointwise updates, similarly to associative lists. Inside the logic, they behave like ordinary functions with extensionality. Via the update/constant pattern, a recursion combinator and an induction rule for FinFuns allow for defining and reasoning about operators on FinFun that are also executable.
extra-history =
Change history:
[2010-08-13]:
new concept domain of a FinFun as a FinFun
(revision 34b3517cbc09)
[2010-11-04]:
new conversion function from FinFun to list of elements in the domain
(revision 0c167102e6ed)
[2012-03-07]:
replace sets as FinFuns by predicates as FinFuns because the set type constructor has been reintroduced
(revision b7aa87989f3a)
notify = nipkow@in.tum.de
[Collections]
title = Collections Framework
author = Peter Lammich
contributors = Andreas Lochbihler , Thomas Tuerk <>
date = 2009-11-25
topic = Computer science/Data structures
abstract = This development provides an efficient, extensible, machine checked collections framework. The library adopts the concepts of interface, implementation and generic algorithm from object-oriented programming and implements them in Isabelle/HOL. The framework features the use of data refinement techniques to refine an abstract specification (using high-level concepts like sets) to a more concrete implementation (using collection datastructures, like red-black-trees). The code-generator of Isabelle/HOL can be used to generate efficient code.
extra-history =
Change history:
[2010-10-08]: New Interfaces: OrderedSet, OrderedMap, List.
Fifo now implements list-interface: Function names changed: put/get --> enqueue/dequeue.
New Implementations: ArrayList, ArrayHashMap, ArrayHashSet, TrieMap, TrieSet.
Invariant-free datastructures: Invariant implicitely hidden in typedef.
Record-interfaces: All operations of an interface encapsulated as record.
Examples moved to examples subdirectory.
[2010-12-01]: New Interfaces: Priority Queues, Annotated Lists. Implemented by finger trees, (skew) binomial queues.
[2011-10-10]: SetSpec: Added operations: sng, isSng, bexists, size_abort, diff, filter, iterate_rule_insertP
MapSpec: Added operations: sng, isSng, iterate_rule_insertP, bexists, size, size_abort, restrict,
map_image_filter, map_value_image_filter
Some maintenance changes
[2012-04-25]: New iterator foundation by Tuerk. Various maintenance changes.
[2012-08]: Collections V2. New features: Polymorphic iterators. Generic algorithm instantiation where required. Naming scheme changed from xx_opname to xx.opname.
A compatibility file CollectionsV1 tries to simplify porting of existing theories, by providing old naming scheme and the old monomorphic iterator locales.
[2013-09]: Added Generic Collection Framework based on Autoref. The GenCF provides: Arbitrary nesting, full integration with Autoref.
[2014-06]: Maintenace changes to GenCF: Optimized inj_image on list_set. op_set_cart (Cartesian product). big-Union operation. atLeastLessThan - operation ({a..<b})
notify = lammich@in.tum.de
[Containers]
title = Light-weight Containers
author = Andreas Lochbihler
contributors = René Thiemann
date = 2013-04-15
topic = Computer science/Data structures
abstract =
This development provides a framework for container types like sets and maps such that generated code implements these containers with different (efficient) data structures.
Thanks to type classes and refinement during code generation, this light-weight approach can seamlessly replace Isabelle's default setup for code generation.
Heuristics automatically pick one of the available data structures depending on the type of elements to be stored, but users can also choose on their own.
The extensible design permits to add more implementations at any time.
To support arbitrary nesting of sets, we define a linear order on sets based on a linear order of the elements and provide efficient implementations.
It even allows to compare complements with non-complements.
extra-history =
Change history:
[2013-07-11]: add pretty printing for sets (revision 7f3f52c5f5fa)
[2013-09-20]:
provide generators for canonical type class instantiations
(revision 159f4401f4a8 by René Thiemann)
[2014-07-08]: add support for going from partial functions to mappings (revision 7a6fc957e8ed)
[2018-03-05]: add two application examples: depth-first search and 2SAT (revision e5e1a1da2411)
notify = mail@andreas-lochbihler.de
[FileRefinement]
title = File Refinement
author = Karen Zee , Viktor Kuncak
date = 2004-12-09
topic = Computer science/Data structures
abstract = These theories illustrates the verification of basic file operations (file creation, file read and file write) in the Isabelle theorem prover. We describe a file at two levels of abstraction: an abstract file represented as a resizable array, and a concrete file represented using data blocks.
notify = kkz@mit.edu
[Datatype_Order_Generator]
title = Generating linear orders for datatypes
author = René Thiemann
date = 2012-08-07
topic = Computer science/Data structures
abstract =
We provide a framework for registering automatic methods to derive
class instances of datatypes, as it is possible using Haskell's ``deriving Ord, Show, ...'' feature.
We further implemented such automatic methods to derive (linear) orders or hash-functions which are
required in the Isabelle Collection Framework. Moreover, for the tactic of Huffman and Krauss to show that a
datatype is countable, we implemented a wrapper so that this tactic becomes accessible in our framework.
Our formalization was performed as part of the IsaFoR/CeTA project.
With our new tactic we could completely remove
tedious proofs for linear orders of two datatypes.
This development is aimed at datatypes generated by the "old_datatype"
command.
notify = rene.thiemann@uibk.ac.at
[Deriving]
title = Deriving class instances for datatypes
author = Christian Sternagel , René Thiemann
date = 2015-03-11
topic = Computer science/Data structures
abstract =
We provide a framework for registering automatic methods
to derive class instances of datatypes,
as it is possible using Haskell's ``deriving Ord, Show, ...'' feature.
We further implemented such automatic methods to derive comparators, linear orders, parametrizable equality functions,
and hash-functions which are required in the
Isabelle Collection Framework and the Container Framework.
Moreover, for the tactic of Blanchette to show that a datatype is countable, we implemented a
wrapper so that this tactic becomes accessible in our framework. All of the generators are based on
the infrastructure that is provided by the BNF-based datatype package.
Our formalization was performed as part of the IsaFoR/CeTA project.
With our new tactics we could remove
several tedious proofs for (conditional) linear orders, and conditional equality operators
within IsaFoR and the Container Framework.
notify = rene.thiemann@uibk.ac.at
[List-Index]
title = List Index
date = 2010-02-20
author = Tobias Nipkow
topic = Computer science/Data structures
abstract = This theory provides functions for finding the index of an element in a list, by predicate and by value.
notify = nipkow@in.tum.de
[List-Infinite]
title = Infinite Lists
date = 2011-02-23
author = David Trachtenherz <>
topic = Computer science/Data structures
abstract = We introduce a theory of infinite lists in HOL formalized as functions over naturals (folder ListInf, theories ListInf and ListInf_Prefix). It also provides additional results for finite lists (theory ListInf/List2), natural numbers (folder CommonArith, esp. division/modulo, naturals with infinity), sets (folder CommonSet, esp. cutting/truncating sets, traversing sets of naturals).
notify = nipkow@in.tum.de
[Matrix]
title = Executable Matrix Operations on Matrices of Arbitrary Dimensions
topic = Computer science/Data structures
date = 2010-06-17
author = Christian Sternagel , René Thiemann
license = LGPL
abstract =
We provide the operations of matrix addition, multiplication,
transposition, and matrix comparisons as executable functions over
ordered semirings. Moreover, it is proven that strongly normalizing
(monotone) orders can be lifted to strongly normalizing (monotone) orders
over matrices. We further show that the standard semirings over the
naturals, integers, and rationals, as well as the arctic semirings
satisfy the axioms that are required by our matrix theory. Our
formalization is part of the CeTA system
which contains several termination techniques. The provided theories have
been essential to formalize matrix-interpretations and arctic
interpretations.
extra-history =
Change history:
[2010-09-17]: Moved theory on arbitrary (ordered) semirings to Abstract Rewriting.
notify = rene.thiemann@uibk.ac.at, christian.sternagel@uibk.ac.at
[Matrix_Tensor]
title = Tensor Product of Matrices
topic = Computer science/Data structures, Mathematics/Algebra
date = 2016-01-18
author = T.V.H. Prathamesh
abstract =
In this work, the Kronecker tensor product of matrices and the proofs of
some of its properties are formalized. Properties which have been formalized
include associativity of the tensor product and the mixed-product
property.
notify = prathamesh@imsc.res.in
[Huffman]
title = The Textbook Proof of Huffman's Algorithm
author = Jasmin Christian Blanchette
date = 2008-10-15
topic = Computer science/Data structures
abstract = Huffman's algorithm is a procedure for constructing a binary tree with minimum weighted path length. This report presents a formal proof of the correctness of Huffman's algorithm written using Isabelle/HOL. Our proof closely follows the sketches found in standard algorithms textbooks, uncovering a few snags in the process. Another distinguishing feature of our formalization is the use of custom induction rules to help Isabelle's automatic tactics, leading to very short proofs for most of the lemmas.
notify = jasmin.blanchette@gmail.com
[Partial_Function_MR]
title = Mutually Recursive Partial Functions
author = René Thiemann
topic = Computer science/Functional programming
date = 2014-02-18
license = LGPL
abstract = We provide a wrapper around the partial-function command that supports mutual recursion.
notify = rene.thiemann@uibk.ac.at
[Lifting_Definition_Option]
title = Lifting Definition Option
author = René Thiemann
topic = Computer science/Functional programming
date = 2014-10-13
license = LGPL
abstract =
We implemented a command that can be used to easily generate
elements of a restricted type {x :: 'a. P x},
provided the definition is of the form
f ys = (if check ys then Some(generate ys :: 'a) else None) where
ys is a list of variables y1 ... yn and
check ys ==> P(generate ys) can be proved.
In principle, such a definition is also directly possible using the
lift_definition command. However, then this definition will not be
suitable for code-generation. To this end, we automated a more complex
construction of Joachim Breitner which is amenable for code-generation, and
where the test check ys will only be performed once. In the
automation, one auxiliary type is created, and Isabelle's lifting- and
transfer-package is invoked several times.
notify = rene.thiemann@uibk.ac.at
[Coinductive]
title = Coinductive
topic = Computer science/Functional programming
author = Andreas Lochbihler
contributors = Johannes Hölzl
date = 2010-02-12
abstract = This article collects formalisations of general-purpose coinductive data types and sets. Currently, it contains coinductive natural numbers, coinductive lists, i.e. lazy lists or streams, infinite streams, coinductive terminated lists, coinductive resumptions, a library of operations on coinductive lists, and a version of König's lemma as an application for coinductive lists.
The initial theory was contributed by Paulson and Wenzel. Extensions and other coinductive formalisations of general interest are welcome.
extra-history =
Change history:
[2010-06-10]:
coinductive lists: setup for quotient package
(revision 015574f3bf3c)
[2010-06-28]:
new codatatype terminated lazy lists
(revision e12de475c558)
[2010-08-04]:
terminated lazy lists: setup for quotient package;
more lemmas
(revision 6ead626f1d01)
[2010-08-17]:
Koenig's lemma as an example application for coinductive lists
(revision f81ce373fa96)
[2011-02-01]:
lazy implementation of coinductive (terminated) lists for the code generator
(revision 6034973dce83)
[2011-07-20]:
new codatatype resumption
(revision 811364c776c7)
[2012-06-27]:
new codatatype stream with operations (with contributions by Peter Gammie)
(revision dd789a56473c)
[2013-03-13]:
construct codatatypes with the BNF package and adjust the definitions and proofs,
setup for lifting and transfer packages
(revision f593eda5b2c0)
[2013-09-20]:
stream theory uses type and operations from HOL/BNF/Examples/Stream
(revision 692809b2b262)
[2014-04-03]:
ccpo structure on codatatypes used to define ldrop, ldropWhile, lfilter, lconcat as least fixpoint;
ccpo topology on coinductive lists contributed by Johannes Hölzl;
added examples
(revision 23cd8156bd42)
notify = mail@andreas-lochbihler.de
[Stream-Fusion]
title = Stream Fusion
author = Brian Huffman
topic = Computer science/Functional programming
date = 2009-04-29
abstract = Stream Fusion is a system for removing intermediate list structures from Haskell programs; it consists of a Haskell library along with several compiler rewrite rules. (The library is available online.)
These theories contain a formalization of much of the Stream Fusion library in HOLCF. Lazy list and stream types are defined, along with coercions between the two types, as well as an equivalence relation for streams that generate the same list. List and stream versions of map, filter, foldr, enumFromTo, append, zipWith, and concatMap are defined, and the stream versions are shown to respect stream equivalence.
notify = brianh@cs.pdx.edu
[Tycon]
title = Type Constructor Classes and Monad Transformers
author = Brian Huffman
date = 2012-06-26
topic = Computer science/Functional programming
abstract =
These theories contain a formalization of first class type constructors
and axiomatic constructor classes for HOLCF. This work is described
in detail in the ICFP 2012 paper Formal Verification of Monad
Transformers by the author. The formalization is a revised and
updated version of earlier joint work with Matthews and White.
Based on the hierarchy of type classes in Haskell, we define classes
for functors, monads, monad-plus, etc. Each one includes all the
standard laws as axioms. We also provide a new user command,
tycondef, for defining new type constructors in HOLCF. Using tycondef,
we instantiate the type class hierarchy with various monads and monad
transformers.
notify = huffman@in.tum.de
[CoreC++]
title = CoreC++
author = Daniel Wasserrab
date = 2006-05-15
topic = Computer science/Programming languages/Language definitions
abstract = We present an operational semantics and type safety proof for multiple inheritance in C++. The semantics models the behavior of method calls, field accesses, and two forms of casts in C++ class hierarchies. For explanations see the OOPSLA 2006 paper by Wasserrab, Nipkow, Snelting and Tip.
notify = nipkow@in.tum.de
[FeatherweightJava]
title = A Theory of Featherweight Java in Isabelle/HOL
author = J. Nathan Foster , Dimitrios Vytiniotis
date = 2006-03-31
topic = Computer science/Programming languages/Language definitions
abstract = We formalize the type system, small-step operational semantics, and type soundness proof for Featherweight Java, a simple object calculus, in Isabelle/HOL.
notify = kleing@cse.unsw.edu.au
[Jinja]
title = Jinja is not Java
author = Gerwin Klein , Tobias Nipkow
date = 2005-06-01
topic = Computer science/Programming languages/Language definitions
abstract = We introduce Jinja, a Java-like programming language with a formal semantics designed to exhibit core features of the Java language architecture. Jinja is a compromise between realism of the language and tractability and clarity of the formal semantics. The following aspects are formalised: a big and a small step operational semantics for Jinja and a proof of their equivalence; a type system and a definite initialisation analysis; a type safety proof of the small step semantics; a virtual machine (JVM), its operational semantics and its type system; a type safety proof for the JVM; a bytecode verifier, i.e. data flow analyser for the JVM; a correctness proof of the bytecode verifier w.r.t. the type system; a compiler and a proof that it preserves semantics and well-typedness. The emphasis of this work is not on particular language features but on providing a unified model of the source language, the virtual machine and the compiler. The whole development has been carried out in the theorem prover Isabelle/HOL.
notify = kleing@cse.unsw.edu.au, nipkow@in.tum.de
[JinjaThreads]
title = Jinja with Threads
author = Andreas Lochbihler
date = 2007-12-03
topic = Computer science/Programming languages/Language definitions
abstract = We extend the Jinja source code semantics by Klein and Nipkow with Java-style arrays and threads. Concurrency is captured in a generic framework semantics for adding concurrency through interleaving to a sequential semantics, which features dynamic thread creation, inter-thread communication via shared memory, lock synchronisation and joins. Also, threads can suspend themselves and be notified by others. We instantiate the framework with the adapted versions of both Jinja source and byte code and show type safety for the multithreaded case. Equally, the compiler from source to byte code is extended, for which we prove weak bisimilarity between the source code small step semantics and the defensive Jinja virtual machine. On top of this, we formalise the JMM and show the DRF guarantee and consistency. For description of the different parts, see Lochbihler's papers at FOOL 2008, ESOP 2010, ITP 2011, and ESOP 2012.
extra-history =
Change history:
[2008-04-23]:
added bytecode formalisation with arrays and threads, added thread joins
(revision f74a8be156a7)
[2009-04-27]:
added verified compiler from source code to bytecode;
encapsulate native methods in separate semantics
(revision e4f26541e58a)
[2009-11-30]:
extended compiler correctness proof to infinite and deadlocking computations
(revision e50282397435)
[2010-06-08]:
added thread interruption;
new abstract memory model with sequential consistency as implementation
(revision 0cb9e8dbd78d)
[2010-06-28]:
new thread interruption model
(revision c0440d0a1177)
[2010-10-15]:
preliminary version of the Java memory model for source code
(revision 02fee0ef3ca2)
[2010-12-16]:
improved version of the Java memory model, also for bytecode
executable scheduler for source code semantics
(revision 1f41c1842f5a)
[2011-02-02]:
simplified code generator setup
new random scheduler
(revision 3059dafd013f)
[2011-07-21]:
new interruption model,
generalized JMM proof of DRF guarantee,
allow class Object to declare methods and fields,
simplified subtyping relation,
corrected division and modulo implementation
(revision 46e4181ed142)
[2012-02-16]:
added example programs
(revision bf0b06c8913d)
[2012-11-21]:
type safety proof for the Java memory model,
allow spurious wake-ups
(revision 76063d860ae0)
[2013-05-16]:
support for non-deterministic memory allocators
(revision cc3344a49ced)
[2017-10-20]:
add an atomic compare-and-swap operation for volatile fields
(revision a6189b1d6b30)
notify = mail@andreas-lochbihler.de
[Locally-Nameless-Sigma]
title = Locally Nameless Sigma Calculus
author = Ludovic Henrio , Florian Kammüller , Bianca Lutz , Henry Sudhof
date = 2010-04-30
topic = Computer science/Programming languages/Language definitions
abstract = We present a Theory of Objects based on the original functional sigma-calculus by Abadi and Cardelli but with an additional parameter to methods. We prove confluence of the operational semantics following the outline of Nipkow's proof of confluence for the lambda-calculus reusing his theory Commutation, a generic diamond lemma reduction. We furthermore formalize a simple type system for our sigma-calculus including a proof of type safety. The entire development uses the concept of Locally Nameless representation for binders. We reuse an earlier proof of confluence for a simpler sigma-calculus based on de Bruijn indices and lists to represent objects.
notify = nipkow@in.tum.de
[Attack_Trees]
title = Attack Trees in Isabelle for GDPR compliance of IoT healthcare systems
author = Florian Kammueller
topic = Computer science/Security
date = 2020-04-27
notify = florian.kammuller@gmail.com
abstract =
In this article, we present a proof theory for Attack Trees. Attack
Trees are a well established and useful model for the construction of
attacks on systems since they allow a stepwise exploration of high
level attacks in application scenarios. Using the expressiveness of
Higher Order Logic in Isabelle, we develop a generic
theory of Attack Trees with a state-based semantics based on Kripke
structures and CTL. The resulting framework
allows mechanically supported logic analysis of the meta-theory of the
proof calculus of Attack Trees and at the same time the developed
proof theory enables application to case studies. A central
correctness and completeness result proved in Isabelle establishes a
connection between the notion of Attack Tree validity and CTL. The
application is illustrated on the example of a healthcare IoT system
and GDPR compliance verification.
[AutoFocus-Stream]
title = AutoFocus Stream Processing for Single-Clocking and Multi-Clocking Semantics
author = David Trachtenherz <>
date = 2011-02-23
topic = Computer science/Programming languages/Language definitions
abstract = We formalize the AutoFocus Semantics (a time-synchronous subset of the Focus formalism) as stream processing functions on finite and infinite message streams represented as finite/infinite lists. The formalization comprises both the conventional single-clocking semantics (uniform global clock for all components and communications channels) and its extension to multi-clocking semantics (internal execution clocking of a component may be a multiple of the external communication clocking). The semantics is defined by generic stream processing functions making it suitable for simulation/code generation in Isabelle/HOL. Furthermore, a number of AutoFocus semantics properties are formalized using definitions from the IntervalLogic theories.
notify = nipkow@in.tum.de
[FocusStreamsCaseStudies]
title = Stream Processing Components: Isabelle/HOL Formalisation and Case Studies
author = Maria Spichkova
date = 2013-11-14
topic = Computer science/Programming languages/Language definitions
abstract = This set of theories presents an Isabelle/HOL formalisation of stream processing components introduced
in Focus,
a framework for formal specification and development of interactive systems.
This is an extended and updated version of the formalisation, which was
elaborated within the methodology "Focus on Isabelle".
In addition, we also applied the formalisation on three case studies
that cover different application areas: process control (Steam Boiler System),
data transmission (FlexRay communication protocol),
memory and processing components (Automotive-Gateway System).
notify = lp15@cam.ac.uk, maria.spichkova@rmit.edu.au
[Isabelle_Meta_Model]
title = A Meta-Model for the Isabelle API
author = Frédéric Tuong , Burkhart Wolff
date = 2015-09-16
topic = Computer science/Programming languages/Language definitions
abstract =
We represent a theory of (a fragment of) Isabelle/HOL in
Isabelle/HOL. The purpose of this exercise is to write packages for
domain-specific specifications such as class models, B-machines, ...,
and generally speaking, any domain-specific languages whose
abstract syntax can be defined by a HOL "datatype". On this basis, the
Isabelle code-generator can then be used to generate code for global
context transformations as well as tactic code.
Consequently the package is geared towards
parsing, printing and code-generation to the Isabelle API.
It is at the moment not sufficiently rich for doing meta theory on
Isabelle itself. Extensions in this direction are possible though.
Moreover, the chosen fragment is fairly rudimentary. However it should be
easily adapted to one's needs if a package is written on top of it.
The supported API contains types, terms, transformation of
global context like definitions and data-type declarations as well
as infrastructure for Isar-setups.
This theory is drawn from the
Featherweight OCL
project where
it is used to construct a package for object-oriented data-type theories
generated from UML class diagrams. The Featherweight OCL, for example, allows for
both the direct execution of compiled tactic code by the Isabelle API
as well as the generation of ".thy"-files for debugging purposes.
Gained experience from this project shows that the compiled code is sufficiently
efficient for practical purposes while being based on a formal model
on which properties of the package can be proven such as termination of certain
transformations, correctness, etc.
notify = tuong@users.gforge.inria.fr, wolff@lri.fr
[Clean]
title = Clean - An Abstract Imperative Programming Language and its Theory
author = Frédéric Tuong , Burkhart Wolff
topic = Computer science/Programming languages, Computer science/Semantics
date = 2019-10-04
notify = wolff@lri.fr, ftuong@lri.fr
abstract =
Clean is based on a simple, abstract execution model for an imperative
target language. “Abstract” is understood in contrast to “Concrete
Semantics”; alternatively, the term “shallow-style embedding” could be
used. It strives for a type-safe notion of program-variables, an
incremental construction of the typed state-space, support of
incremental verification, and open-world extensibility of new type
definitions being intertwined with the program definitions. Clean is
based on a “no-frills” state-exception monad with the usual
definitions of bind and unit for the compositional glue of state-based
computations. Clean offers conditionals and loops supporting C-like
control-flow operators such as break and return. The state-space
construction is based on the extensible record package. Direct
recursion of procedures is supported. Clean’s design strives for
extreme simplicity. It is geared towards symbolic execution and proven
correct verification tools. The underlying libraries of this package,
however, deliberately restrict themselves to the most elementary
infrastructure for these tasks. The package is intended to serve as
demonstrator semantic backend for Isabelle/C, or for the
test-generation techniques.
[PCF]
title = Logical Relations for PCF
author = Peter Gammie
date = 2012-07-01
topic = Computer science/Programming languages/Lambda calculi
abstract = We apply Andy Pitts's methods of defining relations over domains to
several classical results in the literature. We show that the Y
combinator coincides with the domain-theoretic fixpoint operator,
that parallel-or and the Plotkin existential are not definable in
PCF, that the continuation semantics for PCF coincides with the
direct semantics, and that our domain-theoretic semantics for PCF is
adequate for reasoning about contextual equivalence in an
operational semantics. Our version of PCF is untyped and has both
strict and non-strict function abstractions. The development is
carried out in HOLCF.
notify = peteg42@gmail.com
[POPLmark-deBruijn]
title = POPLmark Challenge Via de Bruijn Indices
author = Stefan Berghofer
date = 2007-08-02
topic = Computer science/Programming languages/Lambda calculi
abstract = We present a solution to the POPLmark challenge designed by Aydemir et al., which has as a goal the formalization of the meta-theory of System F<:. The formalization is carried out in the theorem prover Isabelle/HOL using an encoding based on de Bruijn indices. We start with a relatively simple formalization covering only the basic features of System F<:, and explain how it can be extended to also cover records and more advanced binding constructs.
notify = berghofe@in.tum.de
[Lam-ml-Normalization]
title = Strong Normalization of Moggis's Computational Metalanguage
author = Christian Doczkal
date = 2010-08-29
topic = Computer science/Programming languages/Lambda calculi
abstract = Handling variable binding is one of the main difficulties in formal proofs. In this context, Moggi's computational metalanguage serves as an interesting case study. It features monadic types and a commuting conversion rule that rearranges the binding structure. Lindley and Stark have given an elegant proof of strong normalization for this calculus. The key construction in their proof is a notion of relational TT-lifting, using stacks of elimination contexts to obtain a Girard-Tait style logical relation. I give a formalization of their proof in Isabelle/HOL-Nominal with a particular emphasis on the treatment of bound variables.
notify = doczkal@ps.uni-saarland.de, nipkow@in.tum.de
[MiniML]
title = Mini ML
author = Wolfgang Naraschewski <>, Tobias Nipkow
date = 2004-03-19
topic = Computer science/Programming languages/Type systems
abstract = This theory defines the type inference rules and the type inference algorithm W for MiniML (simply-typed lambda terms with let) due to Milner. It proves the soundness and completeness of W w.r.t. the rules.
notify = kleing@cse.unsw.edu.au
[Simpl]
title = A Sequential Imperative Programming Language Syntax, Semantics, Hoare Logics and Verification Environment
author = Norbert Schirmer <>
date = 2008-02-29
topic = Computer science/Programming languages/Language definitions, Computer science/Programming languages/Logics
license = LGPL
abstract = We present the theory of Simpl, a sequential imperative programming language. We introduce its syntax, its semantics (big and small-step operational semantics) and Hoare logics for both partial as well as total correctness. We prove soundness and completeness of the Hoare logic. We integrate and automate the Hoare logic in Isabelle/HOL to obtain a practically usable verification environment for imperative programs. Simpl is independent of a concrete programming language but expressive enough to cover all common language features: mutually recursive procedures, abrupt termination and exceptions, runtime faults, local and global variables, pointers and heap, expressions with side effects, pointers to procedures, partial application and closures, dynamic method invocation and also unbounded nondeterminism.
notify = kleing@cse.unsw.edu.au, norbert.schirmer@web.de
[Separation_Algebra]
title = Separation Algebra
author = Gerwin Klein , Rafal Kolanski , Andrew Boyton
date = 2012-05-11
topic = Computer science/Programming languages/Logics
license = BSD
abstract = We present a generic type class implementation of separation algebra for Isabelle/HOL as well as lemmas and generic tactics which can be used directly for any instantiation of the type class. The ex directory contains example instantiations that include structures such as a heap or virtual memory.
The abstract separation algebra is based upon "Abstract Separation Logic" by Calcagno et al. These theories are also the basis of the ITP 2012 rough diamond "Mechanised Separation Algebra" by the authors.
The aim of this work is to support and significantly reduce the effort for future separation logic developments in Isabelle/HOL by factoring out the part of separation logic that can be treated abstractly once and for all. This includes developing typical default rule sets for reasoning as well as automated tactic support for separation logic.
notify = kleing@cse.unsw.edu.au, rafal.kolanski@nicta.com.au
[Separation_Logic_Imperative_HOL]
title = A Separation Logic Framework for Imperative HOL
author = Peter Lammich , Rene Meis
date = 2012-11-14
topic = Computer science/Programming languages/Logics
license = BSD
abstract =
We provide a framework for separation-logic based correctness proofs of
Imperative HOL programs. Our framework comes with a set of proof methods to
automate canonical tasks such as verification condition generation and
frame inference. Moreover, we provide a set of examples that show the
applicability of our framework. The examples include algorithms on lists,
hash-tables, and union-find trees. We also provide abstract interfaces for
lists, maps, and sets, that allow to develop generic imperative algorithms
and use data-refinement techniques.
As we target Imperative HOL, our programs can be translated to
efficiently executable code in various target languages, including
ML, OCaml, Haskell, and Scala.
notify = lammich@in.tum.de
[Inductive_Confidentiality]
title = Inductive Study of Confidentiality
author = Giampaolo Bella
date = 2012-05-02
topic = Computer science/Security
abstract = This document contains the full theory files accompanying article Inductive Study of Confidentiality --- for Everyone in Formal Aspects of Computing. They aim at an illustrative and didactic presentation of the Inductive Method of protocol analysis, focusing on the treatment of one of the main goals of security protocols: confidentiality against a threat model. The treatment of confidentiality, which in fact forms a key aspect of all protocol analysis tools, has been found cryptic by many learners of the Inductive Method, hence the motivation for this work. The theory files in this document guide the reader step by step towards design and proof of significant confidentiality theorems. These are developed against two threat models, the standard Dolev-Yao and a more audacious one, the General Attacker, which turns out to be particularly useful also for teaching purposes.
notify = giamp@dmi.unict.it
[Possibilistic_Noninterference]
title = Possibilistic Noninterference
author = Andrei Popescu , Johannes Hölzl
date = 2012-09-10
topic = Computer science/Security, Computer science/Programming languages/Type systems
abstract = We formalize a wide variety of Volpano/Smith-style noninterference
notions for a while language with parallel composition.
We systematize and classify these notions according to
compositionality w.r.t. the language constructs. Compositionality
yields sound syntactic criteria (a.k.a. type systems) in a uniform way.
An article
about these proofs is published in the proceedings
of the conference Certified Programs and Proofs 2012.
notify = hoelzl@in.tum.de
[SIFUM_Type_Systems]
title = A Formalization of Assumptions and Guarantees for Compositional Noninterference
author = Sylvia Grewe , Heiko Mantel , Daniel Schoepe
date = 2014-04-23
topic = Computer science/Security, Computer science/Programming languages/Type systems
abstract = Research in information-flow security aims at developing methods to
identify undesired information leaks within programs from private
(high) sources to public (low) sinks. For a concurrent system, it is
desirable to have compositional analysis methods that allow for
analyzing each thread independently and that nevertheless guarantee
that the parallel composition of successfully analyzed threads
satisfies a global security guarantee. However, such a compositional
analysis should not be overly pessimistic about what an environment
might do with shared resources. Otherwise, the analysis will reject
many intuitively secure programs.
The paper "Assumptions and Guarantees for Compositional
Noninterference" by Mantel et. al. presents one solution for this problem:
an approach for compositionally reasoning about non-interference in
concurrent programs via rely-guarantee-style reasoning. We present an
Isabelle/HOL formalization of the concepts and proofs of this approach.
notify = grewe@cs.tu-darmstadt.de
[Dependent_SIFUM_Type_Systems]
title = A Dependent Security Type System for Concurrent Imperative Programs
author = Toby Murray , Robert Sison<>, Edward Pierzchalski<>, Christine Rizkallah
notify = toby.murray@unimelb.edu.au
date = 2016-06-25
topic = Computer science/Security, Computer science/Programming languages/Type systems
abstract =
The paper "Compositional Verification and Refinement of Concurrent
Value-Dependent Noninterference" by Murray et. al. (CSF 2016) presents
a dependent security type system for compositionally verifying a
value-dependent noninterference property, defined in (Murray, PLAS
2015), for concurrent programs. This development formalises that
security definition, the type system and its soundness proof, and
demonstrates its application on some small examples. It was derived
from the SIFUM_Type_Systems AFP entry, by Sylvia Grewe, Heiko Mantel
and Daniel Schoepe, and whose structure it inherits.
extra-history =
Change history:
[2016-08-19]:
Removed unused "stop" parameter and "stop_no_eval" assumption from the sifum_security locale.
(revision dbc482d36372)
[2016-09-27]:
Added security locale support for the imposition of requirements on the initial memory.
(revision cce4ceb74ddb)
[Dependent_SIFUM_Refinement]
title = Compositional Security-Preserving Refinement for Concurrent Imperative Programs
author = Toby Murray , Robert Sison<>, Edward Pierzchalski<>, Christine Rizkallah
notify = toby.murray@unimelb.edu.au
date = 2016-06-28
topic = Computer science/Security
abstract =
The paper "Compositional Verification and Refinement of Concurrent
Value-Dependent Noninterference" by Murray et. al. (CSF 2016) presents
a compositional theory of refinement for a value-dependent
noninterference property, defined in (Murray, PLAS 2015), for
concurrent programs. This development formalises that refinement
theory, and demonstrates its application on some small examples.
extra-history =
Change history:
[2016-08-19]:
Removed unused "stop" parameters from the sifum_refinement locale.
(revision dbc482d36372)
[2016-09-02]:
TobyM extended "simple" refinement theory to be usable for all bisimulations.
(revision 547f31c25f60)
[Relational-Incorrectness-Logic]
title = An Under-Approximate Relational Logic
author = Toby Murray
topic = Computer science/Programming languages/Logics, Computer science/Security
date = 2020-03-12
notify = toby.murray@unimelb.edu.au
abstract =
Recently, authors have proposed under-approximate logics for reasoning
about programs. So far, all such logics have been confined to
reasoning about individual program behaviours. Yet there exist many
over-approximate relational logics for reasoning about pairs of
programs and relating their behaviours. We present the first
under-approximate relational logic, for the simple imperative language
IMP. We prove our logic is both sound and complete. Additionally, we
show how reasoning in this logic can be decomposed into non-relational
reasoning in an under-approximate Hoare logic, mirroring Beringer’s
result for over-approximate relational logics. We illustrate the
application of our logic on some small examples in which we provably
demonstrate the presence of insecurity.
[Strong_Security]
title = A Formalization of Strong Security
author = Sylvia Grewe , Alexander Lux , Heiko Mantel , Jens Sauer
date = 2014-04-23
topic = Computer science/Security, Computer science/Programming languages/Type systems
abstract = Research in information-flow security aims at developing methods to
identify undesired information leaks within programs from private
sources to public sinks. Noninterference captures this
intuition. Strong security from Sabelfeld and Sands
formalizes noninterference for concurrent systems.
We present an Isabelle/HOL formalization of strong security for
arbitrary security lattices (Sabelfeld and Sands use
a two-element security lattice in the original publication).
The formalization includes
compositionality proofs for strong security and a soundness proof
for a security type system that checks strong security for programs
in a simple while language with dynamic thread creation.
Our formalization of the security type system is abstract in the
language for expressions and in the semantic side conditions for
expressions. It can easily be instantiated with different syntactic
approximations for these side conditions. The soundness proof of
such an instantiation boils down to showing that these syntactic
approximations imply the semantic side conditions.
notify = grewe@cs.tu-darmstadt.de
[WHATandWHERE_Security]
title = A Formalization of Declassification with WHAT-and-WHERE-Security
author = Sylvia Grewe , Alexander Lux