|
Archive of
Formal
Proofs
The Archive of Formal Proofs is a collection of proof libraries, examples,
and larger scientific developments, mechanically checked in the theorem prover
Isabelle. It is organized in the way
of a scientific journal, is indexed by dblp and has an ISSN: 2150-914x. Submissions are refereed. The preferred citation style
is available [here].
This is the development version of the archive, referring to a recent
Isabelle development version. Some entries may not be in a working state, see
the status page for more information.
The main archive is available from the front page.
|
2016 |
2016-09-09:
Iptables Semantics
Author:
Cornelius Diekmann and
Lars Hupel
|
2016-09-06:
Stone Algebras
Author:
Walter Guttmann
|
2016-09-06:
A Variant of the Superposition Calculus
Author:
Nicolas Peltier
|
2016-09-01:
Stirling's formula
Author:
Manuel Eberl
|
2016-08-31:
Routing
Author:
Julius Michaelis and
Cornelius Diekmann
|
2016-08-24:
Simple Firewall
Author:
Cornelius Diekmann,
Julius Michaelis and
Max Haslbeck
|
2016-08-18:
Infeasible Paths Elimination by Symbolic Execution Techniques: Proof of Correctness and Preservation of Paths
Author:
Romain Aissat,
Frederic Voisin and
Burkhart Wolff
|
2016-08-12:
Formalizing the Edmonds-Karp Algorithm
Author:
Peter Lammich and
S. Reza Sefidgar
|
2016-08-08:
The Imperative Refinement Framework
Author:
Peter Lammich
|
2016-08-07:
Ptolemy's Theorem
Author:
Lukas Bulwahn
|
2016-07-17:
Surprise Paradox
Author:
Joachim Breitner
|
2016-07-14:
Pairing Heap
Author:
Hauke Brinkop and
Tobias Nipkow
|
2016-07-06:
Multivariate Polynomials
Author:
Alexander Maletzky and
Fabian Immler
|
2016-07-05:
A Framework for Verifying Depth-First Search Algorithms
Author:
Peter Lammich and
René Neumann
|
2016-07-01:
Chamber Complexes, Coxeter Systems, and Buildings
Author:
Jeremy Sylvestre
|
2016-06-30:
The Z Property
Author:
Bertram Felgenhauer,
Julian Nagele,
Vincent van Oostrom and
Christian Sternagel
|
2016-06-30:
The Resolution Calculus for First-Order Logic
Author:
Anders Schlichtkrull
|
2016-06-28:
IP Addresses
Author:
Cornelius Diekmann,
Julius Michaelis and
Lars Hupel
|
2016-06-28:
Compositional Security-Preserving Refinement for Concurrent Imperative Programs
Author:
Toby Murray,
Robert Sison,
Edward Pierzchalski and
Christine Rizkallah
|
2016-06-26:
Category Theory with Adjunctions and Limits
Author:
Eugene W. Stark
|
2016-06-26:
Cardinality of Multisets
Author:
Lukas Bulwahn
|
2016-06-25:
A Dependent Security Type System for Concurrent Imperative Programs
Author:
Toby Murray,
Robert Sison,
Edward Pierzchalski and
Christine Rizkallah
|
2016-06-21:
Catalan Numbers
Author:
Manuel Eberl
|
2016-06-18:
Program Construction and Verification Components Based on Kleene Algebra
Author:
Victor B. F. Gomes and
Georg Struth
|
2016-06-13:
Conservation of CSP Noninterference Security under Concurrent Composition
Author:
Pasquale Noce
|
2016-06-09:
Finite Machine Word Library
Author:
Joel Beeren,
Matthew Fernandez,
Xin Gao,
Gerwin Klein,
Rafal Kolanski,
Japheth Lim,
Corey Lewis,
Daniel Matichuk and
Thomas Sewell
|
2016-05-31:
Tree Decomposition
Author:
Christoph Dittmann
|
2016-05-24:
Cardinality of Equivalence Relations
Author:
Lukas Bulwahn
|
2016-05-24:
POSIX Lexing with Derivatives of Regular Expressions
Author:
Fahad Ausaf,
Roy Dyckhoff and
Christian Urban
|
2016-05-20:
Perron-Frobenius Theorem for Spectral Radius Analysis
Author:
Jose Divasón,
Ondřej Kunčar,
René Thiemann and
Akihisa Yamada
|
2016-05-20:
The meta theory of the Incredible Proof Machine
Author:
Joachim Breitner and
Denis Lohner
|
2016-05-18:
A Constructive Proof for FLP
Author:
Benjamin Bisping,
Paul-David Brodmann,
Tim Jungnickel,
Christina Rickmann,
Henning Seidler,
Anke Stüber,
Arno Wilhelm-Weidner,
Kirstin Peters and
Uwe Nestmann
|
2016-05-09:
A Formal Proof of the Max-Flow Min-Cut Theorem for Countable Networks
Author:
Andreas Lochbihler
|
2016-05-05:
Randomised Social Choice Theory
Author:
Manuel Eberl
|
2016-05-04:
Spivey's Generalized Recurrence for Bell Numbers
Author:
Lukas Bulwahn
|
2016-05-04:
The Incompatibility of SD-Efficiency and SD-Strategy-Proofness
Author:
Manuel Eberl
|
2016-05-02:
Gröbner Bases Theory
Author:
Fabian Immler and
Alexander Maletzky
|
2016-04-28:
No Faster-Than-Light Observers
Author:
Mike Stannett and
István Németi
|
2016-04-27:
A formalisation of the Cocke-Younger-Kasami algorithm
Author:
Maksym Bortin
|
2016-04-27:
Algorithms for Reduced Ordered Binary Decision Diagrams
Author:
Julius Michaelis,
Maximilian Haslbeck,
Peter Lammich and
Lars Hupel
|
2016-04-26:
Conservation of CSP Noninterference Security under Sequential Composition
Author:
Pasquale Noce
|
2016-04-12:
Kleene Algebras with Domain
Author:
Victor B. F. Gomes,
Walter Guttmann,
Peter Höfner,
Georg Struth and
Tjark Weber
|
2016-03-11:
Propositional Resolution and Prime Implicates Generation
Author:
Nicolas Peltier
|
2016-03-08:
The Cartan Fixed Point Theorems
Author:
Lawrence C. Paulson
|
2016-03-08:
Timed Automata
Author:
Simon Wimmer
|
2016-03-01:
Linear Temporal Logic
Author:
Salomon Sickert
|
2016-02-17:
Analysis of List Update Algorithms
Author:
Maximilian P.L. Haslbeck and
Tobias Nipkow
|
2016-02-05:
Verified Construction of Static Single Assignment Form
Author:
Sebastian Ullrich and
Denis Lohner
|
2016-01-29:
Polynomial Interpolation
Author:
René Thiemann and
Akihisa Yamada
|
2016-01-29:
Polynomial Factorization
Author:
René Thiemann and
Akihisa Yamada
|
2016-01-20:
Knot Theory
Author:
T.V.H. Prathamesh
|
2016-01-18:
Tensor Product of Matrices
Author:
T.V.H. Prathamesh
|
2016-01-14:
Cardinality of Number Partitions
Author:
Lukas Bulwahn
|
2014 |
2014-11-28:
The Unified Policy Framework (UPF)
Author:
Achim D. Brucker,
Lukas Brügger and
Burkhart Wolff
|
2014-10-23:
Loop freedom of the (untimed) AODV routing protocol
Author:
Timothy Bourke and
Peter Höfner
|
2014-10-13:
Lifting Definition Option
Author:
René Thiemann
|
2014-10-10:
Stream Fusion in HOL with Code Generation
Author:
Andreas Lochbihler and
Alexandra Maximova
|
2014-10-09:
A Verified Compiler for Probability Density Functions
Author:
Manuel Eberl,
Johannes Hölzl and
Tobias Nipkow
|
2014-10-08:
Formalization of Refinement Calculus for Reactive Systems
Author:
Viorel Preoteasa
|
2014-10-03:
Certification Monads
Author:
Christian Sternagel and
René Thiemann
|
2014-10-03:
XML
Author:
Christian Sternagel and
René Thiemann
|
2014-09-25:
Imperative Insertion Sort
Author:
Christian Sternagel
|
2014-09-19:
The Sturm-Tarski Theorem
Author:
Wenda Li
|
2014-09-15:
The Cayley-Hamilton Theorem
Author:
Stephan Adelsberger,
Stefan Hetzl and
Florian Pollak
|
2014-09-09:
The Jordan-Hölder Theorem
Author:
Jakob von Raumer
|
2014-09-04:
Priority Queues Based on Braun Trees
Author:
Tobias Nipkow
|
2014-09-03:
Gauss-Jordan Algorithm and Its Applications
Author:
Jose Divasón and
Jesús Aransay
|
2014-08-29:
Vector Spaces
Author:
Holden Lee
|
2014-08-29:
Real-Valued Special Functions: Upper and Lower Bounds
Author:
Lawrence C. Paulson
|
2014-08-13:
Skew Heap
Author:
Tobias Nipkow
|
2014-08-12:
Splay Tree
Author:
Tobias Nipkow
|
2014-07-29:
Haskell's Show Class in Isabelle/HOL
Author:
Christian Sternagel and
René Thiemann
|
2014-07-18:
Formal Specification of a Generic Separation Kernel
Author:
Freek Verbeek,
Sergey Tverdyshev,
Oto Havle,
Holger Blasum,
Bruno Langenstein,
Werner Stephan,
Yakoub Nemouchi,
Abderrahmane Feliachi,
Burkhart Wolff and
Julien Schmaltz
|
2014-07-13:
pGCL for Isabelle
Author:
David Cock
|
2014-07-07:
Amortized Complexity Verified
Author:
Tobias Nipkow
|
2014-07-04:
Network Security Policy Verification
Author:
Cornelius Diekmann
|
2014-07-03:
Pop-Refinement
Author:
Alessandro Coglio
|
2014-06-12:
Decision Procedures for MSO on Words Based on Derivatives of Regular Expressions
Author:
Dmitriy Traytel and
Tobias Nipkow
|
2014-06-08:
Boolean Expression Checkers
Author:
Tobias Nipkow
|
2014-05-28:
The CAVA Automata Library
Author:
Peter Lammich
|
2014-05-28:
Converting Linear-Time Temporal Logic to Generalized Büchi Automata
Author:
Alexander Schimpf and
Peter Lammich
|
2014-05-28:
Verified Efficient Implementation of Gabow's Strongly Connected Components Algorithm
Author:
Peter Lammich
|
2014-05-28:
Promela Formalization
Author:
René Neumann
|
2014-05-28:
A Fully Verified Executable LTL Model Checker
Author:
Javier Esparza,
Peter Lammich,
René Neumann,
Tobias Nipkow,
Alexander Schimpf and
Jan-Georg Smaus
|
2014-05-23:
Noninterference Security in Communicating Sequential Processes
Author:
Pasquale Noce
|
2014-05-23:
Transitive closure according to Roy-Floyd-Warshall
Author:
Makarius Wenzel
|
2014-05-21:
Regular Algebras
Author:
Simon Foster and
Georg Struth
|
2014-04-28:
Formalisation and Analysis of Component Dependencies
Author:
Maria Spichkova
|
2014-04-23:
A Formalization of Assumptions and Guarantees for Compositional Noninterference
Author:
Sylvia Grewe,
Heiko Mantel and
Daniel Schoepe
|
2014-04-23:
A Formalization of Strong Security
Author:
Sylvia Grewe,
Alexander Lux,
Heiko Mantel and
Jens Sauer
|
2014-04-23:
A Formalization of Declassification with WHAT-and-WHERE-Security
Author:
Sylvia Grewe,
Alexander Lux,
Heiko Mantel and
Jens Sauer
|
2014-04-22:
Bounded-Deducibility Security
Author:
Andrei Popescu and
Peter Lammich
|
2014-04-16:
A shallow embedding of HyperCTL*
Author:
Markus N. Rabe,
Peter Lammich and
Andrei Popescu
|
2014-04-16:
Abstract Completeness
Author:
Jasmin Christian Blanchette,
Andrei Popescu and
Dmitriy Traytel
|
2014-04-13:
Discrete Summation
Author:
Florian Haftmann
|
2014-04-03:
Syntax and semantics of a GPU kernel programming language
Author:
John Wickerson
|
2014-03-11:
Probabilistic Noninterference
Author:
Andrei Popescu and
Johannes Hölzl
|
2014-03-08:
Mechanization of the Algebra for Wireless Networks (AWN)
Author:
Timothy Bourke
|
2014-02-18:
Mutually Recursive Partial Functions
Author:
René Thiemann
|
2014-02-13:
Properties of Random Graphs -- Subgraph Containment
Author:
Lars Hupel
|
2014-02-11:
Verification of Selection and Heap Sort Using Locales
Author:
Danijela Petrovic
|
2014-02-07:
Affine Arithmetic
Author:
Fabian Immler
|
2014-02-06:
Implementing field extensions of the form Q[sqrt(b)]
Author:
René Thiemann
|
2014-01-30:
Unified Decision Procedures for Regular Expression Equivalence
Author:
Tobias Nipkow and
Dmitriy Traytel
|
2014-01-28:
Secondary Sylow Theorems
Author:
Jakob von Raumer
|
2014-01-25:
Relation Algebra
Author:
Alasdair Armstrong,
Simon Foster,
Georg Struth and
Tjark Weber
|
2014-01-23:
Kleene Algebra with Tests and Demonic Refinement Algebras
Author:
Alasdair Armstrong,
Victor B. F. Gomes and
Georg Struth
|
2014-01-16:
Featherweight OCL: A Proposal for a Machine-Checked Formal Semantics for OCL 2.5
Author:
Achim D. Brucker,
Frédéric Tuong and
Burkhart Wolff
|
2014-01-11:
Sturm's Theorem
Author:
Manuel Eberl
|
2014-01-11:
Compositional Properties of Crypto-Based Components
Author:
Maria Spichkova
|
|