We develop algebras for aggregation and minimisation for weight
matrices and for edge weights in graphs. We verify the correctness of
Prim's and Kruskal's minimum spanning tree algorithms based
on these algebras. We also show numerous instances of these algebras
-based on linearly ordered commutative semigroups.
BSD License
Topics
+based on linearly ordered commutative semigroups.
BSD License
Change history
+
December 9, 2020
+ moved Hoare logic to HOL-Hoare, moved spanning trees to Relational_Minimum_Spanning_Trees
+(revision dbb9bfaf4283)
+
Applicative functors augment computations with effects by lifting function application to types which model the effects. As the structure of the computation cannot depend on the effects, applicative expressions can be analysed statically. This allows us to lift universally quantified equations to the effectful types, as observed by Hinze. Thus, equational reasoning over effectful computations can be reduced to pure types.
This entry provides a package for registering applicative functors and two proof methods for lifting of equations over applicative functors. The first method normalises applicative expressions according to the laws of applicative functors. This way, equations whose two sides contain the same list of variables can be lifted to every applicative functor.
To lift larger classes of equations, the second method exploits a number of additional properties (e.g., commutativity of effects) provided the properties have been declared for the concrete applicative functor at hand upon registration.
We declare several types from the Isabelle library as applicative functors and illustrate the use of the methods with two examples: the lifting of the arithmetic type class hierarchy to streams and the verification of a relabelling function on binary trees. We also formalise and verify the normalisation algorithm used by the first proof method.
BSD License
Change history
+
June 10, 2016
+ implemented automatic derivation of lifted combinator reductions;
+support arbitrary lifted relations using relators;
+improved compatibility with locale interpretation
+(revision ec336f354f37)
+
We present the first formal verification of approximation algorithms
for NP-complete optimization problems: vertex cover, set cover, independent set,
center selection, load balancing, and bin packing. The proofs correct incompletenesses
in existing proofs and improve the approximation ratio in one case.
A detailed description of our work (excluding center selection) has been published in the proceedings of
-IJCAR 2020.
\ No newline at end of file
diff --git a/web/entries/BTree.html b/web/entries/BTree.html
--- a/web/entries/BTree.html
+++ b/web/entries/BTree.html
@@ -1,205 +1,210 @@
A Verified Imperative Implementation of B-Trees - Archive of Formal Proofs
In this work, we use the interactive theorem prover Isabelle/HOL to
verify an imperative implementation of the classical B-tree data
structure invented by Bayer and McCreight [ACM 1970]. The
implementation supports set membership, insertion and deletion queries with
efficient binary search for intra-node navigation. This is
accomplished by first specifying the structure abstractly in the
functional modeling language HOL and proving functional correctness.
Using manual refinement, we derive an imperative implementation in
Imperative/HOL. We show the validity of this refinement using the
separation logic utilities from the
Isabelle Refinement Framework . The code can be exported to
the programming languages SML, OCaml and Scala. We examine the runtime of all
operations indirectly by reproducing results of the logarithmic
relationship between height and the number of nodes. The results are
discussed in greater detail in the corresponding Bachelor's
-Thesis.
BSD License
Topics
+Thesis.
BSD License
Change history
+
May 2, 2021
+ Add implementation and proof of correctness of imperative deletion operations.
+Further add the option to export code to OCaml.
+
+
\ No newline at end of file
diff --git a/web/entries/Bicategory.html b/web/entries/Bicategory.html
--- a/web/entries/Bicategory.html
+++ b/web/entries/Bicategory.html
@@ -1,204 +1,219 @@
Bicategories - Archive of Formal Proofs
Taking as a starting point the author's previous work on
developing aspects of category theory in Isabelle/HOL, this article
gives a compatible formalization of the notion of
"bicategory" and develops a framework within which formal
proofs of facts about bicategories can be given. The framework
includes a number of basic results, including the Coherence Theorem,
the Strictness Theorem, pseudofunctors and biequivalence, and facts
about internal equivalences and adjunctions in a bicategory. As a
driving application and demonstration of the utility of the framework,
it is used to give a formal proof of a theorem, due to Carboni,
Kasangian, and Street, that characterizes up to biequivalence the
bicategories of spans in a category with pullbacks. The formalization
effort necessitated the filling-in of many details that were not
evident from the brief presentation in the original paper, as well as
identifying a few minor corrections along the way.
Revisions made subsequent to the first version of this article added
additional material on pseudofunctors, pseudonatural transformations,
modifications, and equivalence of bicategories; the main thrust being
to give a proof that a pseudofunctor is a biequivalence if and only
if it can be extended to an equivalence of bicategories.
-
BSD License
Topics
+
BSD License
Change history
+
July 22, 2021
+ Added new material: "concrete bicategories" and "bicategory of categories".
+(revision 49d3aa43c180)
+
+
November 4, 2020
+ Added new material on equivalence of bicategories, with associated changes.
+(revision 472cb2268826)
+
+
+
February 15, 2020
+ Move ConcreteCategory.thy from Bicategory to Category3 and use it systematically.
+Make other minor improvements throughout.
+(revision a51840d36867)
+
+
This is a formalization of bounded-deducibility security (BD
security), a flexible notion of information-flow security applicable
to arbitrary transition systems. It generalizes Sutherland's
classic notion of nondeducibility by factoring in declassification
bounds and trigger, whereas nondeducibility states that, in a
system, information cannot flow between specified sources and sinks,
BD security indicates upper bounds for the flow and triggers under
-which these upper bounds are no longer guaranteed.
BSD License
Topics
+which these upper bounds are no longer guaranteed.
BSD License
Change history
+
August 12, 2021
+ Generalised BD Security from I/O automata to nondeterministic
+transition systems, with the former retained as an instance of the
+latter (renaming locale BD_Security to BD_Security_IO).
+Generalise unwinding conditions to allow making more than one
+transition at a time when constructing alternative traces.
+Add results about the expressivity of declassification triggers vs.
+bounds, due to Thomas Bauereiss (added as author).
+
\ No newline at end of file
diff --git a/web/entries/Category3.html b/web/entries/Category3.html
--- a/web/entries/Category3.html
+++ b/web/entries/Category3.html
@@ -1,251 +1,278 @@
Category Theory with Adjunctions and Limits - Archive of Formal Proofs
This article attempts to develop a usable framework for doing category
theory in Isabelle/HOL. Our point of view, which to some extent
differs from that of the previous AFP articles on the subject, is to
try to explore how category theory can be done efficaciously within
HOL, rather than trying to match exactly the way things are done using
a traditional approach. To this end, we define the notion of category
in an "object-free" style, in which a category is represented by a
single partial composition operation on arrows. This way of defining
categories provides some advantages in the context of HOL, including
the ability to avoid the use of records and the possibility of
defining functors and natural transformations simply as certain
functions on arrows, rather than as composite objects. We define
various constructions associated with the basic notions, including:
dual category, product category, functor category, discrete category,
free category, functor composition, and horizontal and vertical
composite of natural transformations. A "set category" locale is
defined that axiomatizes the notion "category of all sets at a type
and all functions between them," and a fairly extensive set of
properties of set categories is derived from the locale assumptions.
The notion of a set category is used to prove the Yoneda Lemma in a
general setting of a category equipped with a "hom embedding," which
maps arrows of the category to the "universe" of the set category. We
also give a treatment of adjunctions, defining adjunctions via left
and right adjoint functors, natural bijections between hom-sets, and
unit and counit natural transformations, and showing the equivalence
of these definitions. We also develop the theory of limits, including
representations of functors, diagrams and cones, and diagonal
functors. We show that right adjoint functors preserve limits, and
that limits can be constructed via products and equalizers. We
characterize the conditions under which limits exist in a set
category. We also examine the case of limits in a functor category,
ultimately culminating in a proof that the Yoneda embedding preserves
limits.
Revisions made subsequent to the first version of this article added
material on equivalence of categories, cartesian categories,
categories with pullbacks, categories with finite limits, and
cartesian closed categories. A construction was given of the category
of hereditarily finite sets and functions between them, and it was
shown that this category is cartesian closed.
-
BSD License
Topics
+
BSD License
Change history
+
July 22, 2021
+ Minor changes to sublocale declarations related to functor/natural transformation to
+avoid issues with global interpretations reported 2/2/2021 by Filip Smola.
+(revision 49d3aa43c180)
+
+
November 4, 2020
+ Minor modifications and extensions made in conjunction with the addition
+of new material to Bicategory.
+(revision 472cb2268826)
+
+
+
July 10, 2020
+ Added new material, mostly centered around cartesian categories.
+(revision 06640f317a79)
+
+
+
February 15, 2020
+ Move ConcreteCategory.thy from Bicategory to Category3 and use it systematically.
+Make other minor improvements throughout.
+(revision a51840d36867)
+
+
+
May 29, 2018
+ Revised axioms for the category locale. Introduced notation for composition and "in hom".
+(revision 8318366d4575)
+
+
\ No newline at end of file
diff --git a/web/entries/Coinductive.html b/web/entries/Coinductive.html
--- a/web/entries/Coinductive.html
+++ b/web/entries/Coinductive.html
@@ -1,216 +1,269 @@
Coinductive - Archive of Formal Proofs
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.
BSD License
Topics
+
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.
BSD License
Change history
+
April 3, 2014
+ 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)
+
+
September 20, 2013
+ stream theory uses type and operations from HOL/BNF/Examples/Stream
+(revision 692809b2b262)
+
+
+
March 13, 2013
+ construct codatatypes with the BNF package and adjust the definitions and proofs,
+setup for lifting and transfer packages
+(revision f593eda5b2c0)
+
+
+
June 27, 2012
+ new codatatype stream with operations (with contributions by Peter Gammie)
+(revision dd789a56473c)
+
+
+
July 20, 2011
+ new codatatype resumption
+(revision 811364c776c7)
+
+
+
February 1, 2011
+ lazy implementation of coinductive (terminated) lists for the code generator
+(revision 6034973dce83)
+
+
+
August 17, 2010
+ Koenig's lemma as an example application for coinductive lists
+(revision f81ce373fa96)
+
+
\ No newline at end of file
diff --git a/web/entries/Complx.html b/web/entries/Complx.html
--- a/web/entries/Complx.html
+++ b/web/entries/Complx.html
@@ -1,214 +1,218 @@
COMPLX: A Verification Framework for Concurrent Imperative Programs - Archive of Formal Proofs
COMPLX: AVerification Framework for Concurrent Imperative Programs
We propose a concurrency reasoning framework for imperative programs,
based on the Owicki-Gries (OG) foundational shared-variable
concurrency method. Our framework combines the approaches of
Hoare-Parallel, a formalisation of OG in Isabelle/HOL for a simple
while-language, and Simpl, a generic imperative language embedded in
Isabelle/HOL, allowing formal reasoning on C programs. We define the
Complx language, extending the syntax and semantics of Simpl with
support for parallel composition and synchronisation. We additionally
define an OG logic, which we prove sound w.r.t. the semantics, and a
verification condition generator, both supporting involved low-level
imperative constructs such as function calls and abrupt termination.
We illustrate our framework on an example that features exceptions,
guards and function calls. We aim to then target concurrent operating
systems, such as the interruptible eChronos embedded operating system
-for which we already have a model-level OG proof using Hoare-Parallel.
BSD License
Topics
+for which we already have a model-level OG proof using Hoare-Parallel.
BSD License
Change history
+
January 13, 2017
+ Improve VCG for nested parallels and sequential sections
+(revision 30739dbc3dcb)
+
@article{Complx-AFP,
author = {Sidney Amani and June Andronick and Maksym Bortin and Corey Lewis and Christine Rizkallah and Joseph Tuong},
title = {COMPLX: A Verification Framework for Concurrent Imperative Programs},
journal = {Archive of Formal Proofs},
month = {November},
year = {2016},
note = {\url{https://isa-afp.org/entries/Complx.html},
Formal proof development},
ISSN = {2150-914x},
}
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.
BSD License
Change history
March 5, 2018
add two application examples: depth-first search and 2SAT (revision e5e1a1da2411)
July 8, 2014
add support for going from partial functions to mappings (revision 7a6fc957e8ed)
+
September 20, 2013
+ provide generators for canonical type class instantiations
+(revision 159f4401f4a8 by René Thiemann)
+
+
July 11, 2013
add pretty printing for sets (revision 7f3f52c5f5fa)
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.
BSD License
Topics
+theory, and demonstrates its application on some small examples.
BSD License
Change history
+
September 2, 2016
+ TobyM extended "simple" refinement theory to be usable for all bisimulations.
+(revision 547f31c25f60)
+
+
August 19, 2016
+ Removed unused "stop" parameters from the sifum_refinement locale.
+(revision dbc482d36372)
+
+
@article{Dependent_SIFUM_Refinement-AFP,
author = {Toby Murray and Robert Sison and Edward Pierzchalski and Christine Rizkallah},
title = {Compositional Security-Preserving Refinement for Concurrent Imperative Programs},
journal = {Archive of Formal Proofs},
month = {June},
year = {2016},
note = {\url{https://isa-afp.org/entries/Dependent_SIFUM_Refinement.html},
Formal proof development},
ISSN = {2150-914x},
}
\ No newline at end of file
diff --git a/web/entries/Dependent_SIFUM_Type_Systems.html b/web/entries/Dependent_SIFUM_Type_Systems.html
--- a/web/entries/Dependent_SIFUM_Type_Systems.html
+++ b/web/entries/Dependent_SIFUM_Type_Systems.html
@@ -1,192 +1,201 @@
A Dependent Security Type System for Concurrent Imperative Programs - Archive of Formal Proofs
ADependent Security Type System for Concurrent Imperative Programs
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.
BSD License
Topics
+and Daniel Schoepe, and whose structure it inherits.
BSD License
Change history
+
September 27, 2016
+ Added security locale support for the imposition of requirements on the initial memory.
+(revision cce4ceb74ddb)
+
+
August 19, 2016
+ Removed unused "stop" parameter and "stop_no_eval" assumption from the sifum_security locale.
+(revision dbc482d36372)
+
+
@article{Dependent_SIFUM_Type_Systems-AFP,
author = {Toby Murray and Robert Sison and Edward Pierzchalski and Christine Rizkallah},
title = {A Dependent Security Type System for Concurrent Imperative Programs},
journal = {Archive of Formal Proofs},
month = {June},
year = {2016},
note = {\url{https://isa-afp.org/entries/Dependent_SIFUM_Type_Systems.html},
Formal proof development},
ISSN = {2150-914x},
}
\ No newline at end of file
diff --git a/web/entries/DiscretePricing.html b/web/entries/DiscretePricing.html
--- a/web/entries/DiscretePricing.html
+++ b/web/entries/DiscretePricing.html
@@ -1,179 +1,187 @@
Pricing in discrete financial models - Archive of Formal Proofs
We have formalized the computation of fair prices for derivative
products in discrete financial models. As an application, we derive a
way to compute fair prices of derivative products in the
Cox-Ross-Rubinstein model of a financial market, thus completing the
work that was presented in this paper.
+ Renamed discr_mkt predicate to stk_strict_subs and got rid of predicate A for a more natural definition of the type discrete_market;
+renamed basic quantity processes for coherent notation;
+renamed value_process into val_process and closing_value_process to cls_val_process;
+relaxed hypothesis of lemma CRR_market_fair_price.
+Added functions to price some basic options.
+(revision 0b813a1a833f)
+
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.
BSD License
Topics
+
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.
BSD License
Change history
+
November 20, 2020
+ Additional theory Natural_Mergesort that developes an efficient mergesort
+algorithm without key-functions for educational purposes.
+
+
September 19, 2018
+ Theory Efficient_Mergesort replaces theory Efficient_Sort but keeping the old
+name Efficient_Sort.
+
+
+
September 17, 2018
+ Added theory Efficient_Mergesort that works exclusively with the mutual
+induction schemas generated by the function package.
+
+
\ No newline at end of file
diff --git a/web/entries/Featherweight_OCL.html b/web/entries/Featherweight_OCL.html
--- a/web/entries/Featherweight_OCL.html
+++ b/web/entries/Featherweight_OCL.html
@@ -1,218 +1,229 @@
Featherweight OCL: A Proposal for a Machine-Checked Formal Semantics for OCL 2.5 - Archive of Formal Proofs
Featherweight OCL: AProposal for a Machine-Checked Formal Semantics for OCL 2.5
The Unified Modeling Language (UML) is one of the few
modeling languages that is widely used in industry. While
UML is mostly known as diagrammatic modeling language
(e.g., visualizing class models), it is complemented by a
textual language, called Object Constraint Language
(OCL). The current version of OCL is based on a four-valued
logic that turns UML into a formal language. Any type
comprises the elements "invalid" and "null" which are
propagated as strict and non-strict, respectively.
Unfortunately, the former semi-formal semantics of this
specification language, captured in the "Annex A" of the
OCL standard, leads to different interpretations of corner
cases. We formalize the core of OCL: denotational
definitions, a logical calculus and operational rules that
allow for the execution of OCL expressions by a mixture of
term rewriting and code compilation. Our formalization
reveals several inconsistencies and contradictions in the
current version of the OCL standard. Overall, this document
is intended to provide the basis for a machine-checked text
"Annex A" of the OCL standard targeting at tool
-implementors.
@article{Featherweight_OCL-AFP,
author = {Achim D. Brucker and Frédéric Tuong and Burkhart Wolff},
title = {Featherweight OCL: A Proposal for a Machine-Checked Formal Semantics for OCL 2.5},
journal = {Archive of Formal Proofs},
month = {January},
year = {2014},
note = {\url{https://isa-afp.org/entries/Featherweight_OCL.html},
Formal proof development},
ISSN = {2150-914x},
}
\ No newline at end of file
diff --git a/web/entries/FinFun.html b/web/entries/FinFun.html
--- a/web/entries/FinFun.html
+++ b/web/entries/FinFun.html
@@ -1,198 +1,212 @@
Code Generation for Functions as Data - Archive of Formal Proofs
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.
BSD License
Topics
+
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.
BSD License
Change history
+
March 7, 2012
+ replace sets as FinFuns by predicates as FinFuns because the set type constructor has been reintroduced
+(revision b7aa87989f3a)
+
+
November 4, 2010
+ new conversion function from FinFun to list of elements in the domain
+(revision 0c167102e6ed)
+
+
+
August 13, 2010
+ new concept domain of a FinFun as a FinFun
+(revision 34b3517cbc09)
+
+
\ No newline at end of file
diff --git a/web/entries/Game_Based_Crypto.html b/web/entries/Game_Based_Crypto.html
--- a/web/entries/Game_Based_Crypto.html
+++ b/web/entries/Game_Based_Crypto.html
@@ -1,209 +1,213 @@
Game-based cryptography in HOL - Archive of Formal Proofs
In this AFP entry, we show how to specify game-based cryptographic
security notions and formally prove secure several cryptographic
constructions from the literature using the CryptHOL framework. Among
others, we formalise the notions of a random oracle, a pseudo-random
function, an unpredictable function, and of encryption schemes that are
indistinguishable under chosen plaintext and/or ciphertext attacks. We
prove the random-permutation/random-function switching lemma, security
of the Elgamal and hashed Elgamal public-key encryption scheme and
correctness and security of several constructions with pseudo-random
functions.
Our proofs follow the game-hopping style advocated by
Shoup and Bellare and Rogaway, from which most of the examples have
been taken. We generalise some of their results such that they can be
reused in other proofs. Thanks to CryptHOL's integration with
Isabelle's parametricity infrastructure, many simple hops are easily
-justified using the theory of representation independence.
BSD License
Topics
+justified using the theory of representation independence.
BSD License
Change history
+
September 28, 2018
+ added the CryptHOL tutorial for game-based cryptography
+(revision 489a395764ae)
+
\ No newline at end of file
diff --git a/web/entries/GewirthPGCProof.html b/web/entries/GewirthPGCProof.html
--- a/web/entries/GewirthPGCProof.html
+++ b/web/entries/GewirthPGCProof.html
@@ -1,172 +1,176 @@
Formalisation and Evaluation of Alan Gewirth's Proof for the Principle of Generic Consistency in Isabelle/HOL - Archive of Formal Proofs
Formalisation and Evaluation of Alan Gewirth's Proof for the Principle of Generic Consistency in Isabelle/HOL
An ambitious ethical theory ---Alan Gewirth's "Principle of
Generic Consistency"--- is encoded and analysed in Isabelle/HOL.
Gewirth's theory has stirred much attention in philosophy and
ethics and has been proposed as a potential means to bound the impact
-of artificial general intelligence.
BSD License
Topics
+of artificial general intelligence.
BSD License
Change history
+
April 9, 2019
+ added proof for a stronger variant of the PGC and examplary inferences
+(revision 88182cb0a2f6)
+
@article{GewirthPGCProof-AFP,
author = {David Fuenmayor and Christoph Benzmüller},
title = {Formalisation and Evaluation of Alan Gewirth's Proof for the Principle of Generic Consistency in Isabelle/HOL},
journal = {Archive of Formal Proofs},
month = {October},
year = {2018},
note = {\url{https://isa-afp.org/entries/GewirthPGCProof.html},
Formal proof development},
ISSN = {2150-914x},
}
\ No newline at end of file
diff --git a/web/entries/JinjaThreads.html b/web/entries/JinjaThreads.html
--- a/web/entries/JinjaThreads.html
+++ b/web/entries/JinjaThreads.html
@@ -1,379 +1,452 @@
Jinja with Threads - Archive of Formal Proofs
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.
BSD License
Topics
+
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.
BSD License
Change history
+
October 20, 2017
+ add an atomic compare-and-swap operation for volatile fields
+(revision a6189b1d6b30)
+
+
May 16, 2013
+ support for non-deterministic memory allocators
+(revision cc3344a49ced)
+
+
+
November 21, 2012
+ type safety proof for the Java memory model,
+allow spurious wake-ups
+(revision 76063d860ae0)
+
+
+
February 16, 2012
+ added example programs
+(revision bf0b06c8913d)
+
+
+
July 21, 2011
+ 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)
+
+
\ No newline at end of file
diff --git a/web/entries/LTL.html b/web/entries/LTL.html
--- a/web/entries/LTL.html
+++ b/web/entries/LTL.html
@@ -1,202 +1,206 @@
Linear Temporal Logic - Archive of Formal Proofs
This theory provides a formalisation of linear temporal logic (LTL)
and unifies previous formalisations within the AFP. This entry
establishes syntax and semantics for this logic and decouples it from
existing entries, yielding a common environment for theories reasoning
about LTL. Furthermore a parser written in SML and an executable
-simplifier are provided.
BSD License
Topics
+simplifier are provided.
BSD License
Change history
+
March 12, 2019
+ Support for additional operators, implementation of common equivalence relations,
+definition of syntactic fragments of LTL and the minimal disjunctive normal form.
+
\ No newline at end of file
diff --git a/web/entries/MFMC_Countable.html b/web/entries/MFMC_Countable.html
--- a/web/entries/MFMC_Countable.html
+++ b/web/entries/MFMC_Countable.html
@@ -1,213 +1,227 @@
A Formal Proof of the Max-Flow Min-Cut Theorem for Countable Networks - Archive of Formal Proofs
AFormal Proof of the Max-Flow Min-Cut Theorem for Countable Networks
This article formalises a proof of the maximum-flow minimal-cut
theorem for networks with countably many edges. A network is a
directed graph with non-negative real-valued edge labels and two
dedicated vertices, the source and the sink. A flow in a network
assigns non-negative real numbers to the edges such that for all
vertices except for the source and the sink, the sum of values on
incoming edges equals the sum of values on outgoing edges. A cut is a
subset of the vertices which contains the source, but not the sink.
Our theorem states that in every network, there is a flow and a cut
such that the flow saturates all the edges going out of the cut and is
zero on all the incoming edges. The proof is based on the paper
The Max-Flow Min-Cut theorem for countable networks by
Aharoni et al. Additionally, we prove a characterisation of the
lifting operation for relations on discrete probability distributions,
which leads to a concise proof of its distributivity over relation
-composition.
BSD License
Topics
+composition.
BSD License
Change history
+
August 13, 2021
+ generalize the derivation of the characterisation for the relator of discrete probability distributions to work for the bounded and unbounded MFMC theorem
+(revision 3c85bb52bbe6)
+
+
December 19, 2020
+ simpler proof of linkability for bounded unhindered bipartite webs, leading to a simpler proof for networks with bounded out-capacities
+(revision 93ca33f4d915)
+
+
+
September 6, 2017
+ derive characterisation for the lifting operation on discrete distributions from finite version of the max-flow min-cut theorem
+(revision a7a198f5bab0)
+
+
\ No newline at end of file
diff --git a/web/entries/MFOTL_Monitor.html b/web/entries/MFOTL_Monitor.html
--- a/web/entries/MFOTL_Monitor.html
+++ b/web/entries/MFOTL_Monitor.html
@@ -1,204 +1,208 @@
Formalization of a Monitoring Algorithm for Metric First-Order Temporal Logic - Archive of Formal Proofs
Formalization of a Monitoring Algorithm for Metric First-Order Temporal Logic
A monitor is a runtime verification tool that solves the following
problem: Given a stream of time-stamped events and a policy formulated
in a specification language, decide whether the policy is satisfied at
every point in the stream. We verify the correctness of an executable
monitor for specifications given as formulas in metric first-order
temporal logic (MFOTL), an expressive extension of linear temporal
logic with real-time constraints and first-order quantification. The
verified monitor implements a simplified variant of the algorithm used
in the efficient MonPoly monitoring tool. The formalization is
presented in a RV
2019 paper, which also compares the output of the verified
monitor to that of other monitoring tools on randomly generated
inputs. This case study revealed several errors in the optimized but
-unverified tools.
BSD License
Topics
+unverified tools.
BSD License
Change history
+
August 13, 2020
+ added the formalization of the abstract slicing framework and joint data
+slicer (revision b1639ed541b7)
+
\ No newline at end of file
diff --git a/web/entries/Modal_Logics_for_NTS.html b/web/entries/Modal_Logics_for_NTS.html
--- a/web/entries/Modal_Logics_for_NTS.html
+++ b/web/entries/Modal_Logics_for_NTS.html
@@ -1,211 +1,215 @@
Modal Logics for Nominal Transition Systems - Archive of Formal Proofs
We formalize a uniform semantic substrate for a wide variety of
process calculi where states and action labels can be from arbitrary
nominal sets. A Hennessy-Milner logic for these systems is defined,
and proved adequate for bisimulation equivalence. A main novelty is
the construction of an infinitary nominal data type to model formulas
with (finitely supported) infinite conjunctions and actions that may
contain binding names. The logic is generalized to treat different
bisimulation variants such as early, late and open in a systematic
-way.
BSD License
Topics
+way.
BSD License
Change history
+
January 29, 2017
+ Formalization of weak bisimilarity added
+(revision c87cc2057d9c)
+
@article{Modal_Logics_for_NTS-AFP,
author = {Tjark Weber and Lars-Henrik Eriksson and Joachim Parrow and Johannes Borgström and Ramunas Gutkovas},
title = {Modal Logics for Nominal Transition Systems},
journal = {Archive of Formal Proofs},
month = {October},
year = {2016},
note = {\url{https://isa-afp.org/entries/Modal_Logics_for_NTS.html},
Formal proof development},
ISSN = {2150-914x},
}
Building on the formalization of basic category theory set out in the
author's previous AFP article, the present article formalizes
some basic aspects of the theory of monoidal categories. Among the
notions defined here are monoidal category, monoidal functor, and
equivalence of monoidal categories. The main theorems formalized are
MacLane's coherence theorem and the constructions of the free
monoidal category and free strict monoidal category generated by a
given category. The coherence theorem is proved syntactically, using
a structurally recursive approach to reduction of terms that might
have some novel aspects. We also give proofs of some results given by
Etingof et al, which may prove useful in a formal setting. In
particular, we show that the left and right unitors need not be taken
as given data in the definition of monoidal category, nor does the
definition of monoidal functor need to take as given a specific
isomorphism expressing the preservation of the unit object. Our
definitions of monoidal category and monoidal functor are stated so as
to take advantage of the economy afforded by these facts.
Revisions made subsequent to the first version of this article added
material on cartesian monoidal categories; showing that the underlying
category of a cartesian monoidal category is a cartesian category, and
that every cartesian category extends to a cartesian monoidal
category.
-
BSD License
Topics
+
BSD License
Change history
+
July 10, 2020
+ Added new material on cartesian monoidal categories.
+(revision 06640f317a79)
+
\ No newline at end of file
diff --git a/web/entries/Monomorphic_Monad.html b/web/entries/Monomorphic_Monad.html
--- a/web/entries/Monomorphic_Monad.html
+++ b/web/entries/Monomorphic_Monad.html
@@ -1,184 +1,189 @@
Effect polymorphism in higher-order logic - Archive of Formal Proofs
The notion of a monad cannot be expressed within higher-order logic
(HOL) due to type system restrictions. We show that if a monad is used
with values of only one type, this notion can be formalised in HOL.
Based on this idea, we develop a library of effect specifications and
implementations of monads and monad transformers. Hence, we can
abstract over the concrete monad in HOL definitions and thus use the
same definition for different (combinations of) effects. We illustrate
the usefulness of effect polymorphism with a monadic interpreter for a
-simple language.
BSD License
Topics
+simple language.
BSD License
Change history
+
February 15, 2018
+ added further specifications and implementations of non-determinism;
+more examples
+(revision bc5399eea78e)
+
\ No newline at end of file
diff --git a/web/entries/Native_Word.html b/web/entries/Native_Word.html
--- a/web/entries/Native_Word.html
+++ b/web/entries/Native_Word.html
@@ -1,227 +1,249 @@
Native Word - Archive of Formal Proofs
This entry makes machine words and machine arithmetic available for code generation from Isabelle/HOL. It provides a common abstraction that hides the differences between the different target languages. The code generator maps these operations to the APIs of the target languages. Apart from that, we extend the available bit operations on types int and integer, and map them to the operations in the target languages.
BSD License
Topics
+
This entry makes machine words and machine arithmetic available for code generation from Isabelle/HOL. It provides a common abstraction that hides the differences between the different target languages. The code generator maps these operations to the APIs of the target languages. Apart from that, we extend the available bit operations on types int and integer, and map them to the operations in the target languages.
BSD License
Change history
+
July 15, 2018
+ added cast operators for default-size words (revision fc1f1fb8dd30)
+
+
September 2, 2017
+ added 64-bit words (revision c89f86244e3c)
+
+
+
October 6, 2014
+ proper test setup with compilation and execution of tests in all target languages
+(revision 5d7a1c9ae047)
+
+
+
March 31, 2014
+ added words of default size in the target language (by Peter Lammich)
+(revision 25caf5065833)
+
+
+
November 6, 2013
+ added conversion function between native words and characters
+(revision fd23d9a7fe3a)
+
+
We present a unified theory for verifying network security policies.
A security policy is represented as directed graph.
To check high-level security goals, security invariants over the policy are
expressed. We cover monotonic security invariants, i.e. prohibiting more does not harm
security. We provide the following contributions for the security invariant theory.
Secure auto-completion of scenario-specific knowledge, which eases usability.
Security violations can be repaired by tightening the policy iff the
security invariants hold for the deny-all policy.
An algorithm to compute a security policy.
A formalization of stateful connection semantics in network security mechanisms.
An algorithm to compute a secure stateful implementation of a policy.
An executable implementation of all the theory.
Examples, ranging from an aircraft cabin data network to the analysis
of a large real-world firewall.
More examples: A fully automated translation of high-level security goals to both
firewall and SDN configurations (see Examples/Distributed_WebApp.thy).
C. Diekmann, S.-A. Posselt, H. Niedermayer, H. Kinkelin, O. Hanka, and G. Carle.
Verifying Security Policies using Host Attributes.
In FORTE, 34th IFIP International Conference on Formal Techniques for Distributed Objects,
Components and Systems, Berlin, Germany, June 2014.
C. Diekmann, L. Hupel, and G. Carle. Directed Security Policies:
A Stateful Network Implementation.
In J. Pang and Y. Liu, editors, Engineering Safety and Security Systems,
volume 150 of Electronic Proceedings in Theoretical Computer Science,
pages 20-34, Singapore, May 2014. Open Publishing Association.
-
BSD License
Topics
+
BSD License
Change history
+
April 14, 2015
+ Added Distributed WebApp example and improved graphviz visualization
+(revision 4dde08ca2ab8)
+
\ No newline at end of file
diff --git a/web/entries/Optics.html b/web/entries/Optics.html
--- a/web/entries/Optics.html
+++ b/web/entries/Optics.html
@@ -1,196 +1,205 @@
Optics - Archive of Formal Proofs
Lenses provide an abstract interface for manipulating data types
through spatially-separated views. They are defined abstractly in
terms of two functions, get, the return a value
from the source type, and put that updates the
value. We mechanise the underlying theory of lenses, in terms of an
algebraic hierarchy of lenses, including well-behaved and very
well-behaved lenses, each lens class being characterised by a set of
lens laws. We also mechanise a lens algebra in Isabelle that enables
their composition and comparison, so as to allow construction of
complex lenses. This is accompanied by a large library of algebraic
laws. Moreover we also show how the lens classes can be applied by
-instantiating them with a number of Isabelle data types.
BSD License
Topics
+instantiating them with a number of Isabelle data types.
BSD License
Change history
+
March 2, 2020
+ Added partial bijective and symmetric lenses.
+Improved alphabet command generating additional lenses and results.
+Several additional lens relations, including observational equivalence.
+Additional theorems throughout.
+Adaptations for Isabelle 2020.
+(revision 44e2e5c)
+
+
\ No newline at end of file
diff --git a/web/entries/Perron_Frobenius.html b/web/entries/Perron_Frobenius.html
--- a/web/entries/Perron_Frobenius.html
+++ b/web/entries/Perron_Frobenius.html
@@ -1,218 +1,227 @@
Perron-Frobenius Theorem for Spectral Radius Analysis - Archive of Formal Proofs
Perron-Frobenius Theorem for Spectral Radius Analysis
The spectral radius of a matrix A is the maximum norm of all
eigenvalues of A. In previous work we already formalized that for a
complex matrix A, the values in An grow polynomially in n
if and only if the spectral radius is at most one. One problem with
the above characterization is the determination of all
complex eigenvalues. In case A contains only non-negative
real values, a simplification is possible with the help of the
Perron–Frobenius theorem, which tells us that it suffices to consider only
the real eigenvalues of A, i.e., applying Sturm's method can
decide the polynomial growth of An.
We formalize
the Perron–Frobenius theorem based on a proof via Brouwer's fixpoint
theorem, which is available in the HOL multivariate analysis (HMA)
library. Since the results on the spectral radius is based on matrices
in the Jordan normal form (JNF) library, we further develop a
connection which allows us to easily transfer theorems between HMA and
JNF. With this connection we derive the combined result: if A is a
non-negative real matrix, and no real eigenvalue of A is strictly
-larger than one, then An is polynomially bounded in n.
BSD License
Topics
+larger than one, then An is polynomially bounded in n.
BSD License
Change history
+
May 17, 2018
+ prove conjecture of CPP'18 paper: Jordan blocks of spectral radius have maximum size
+(revision ffdb3794e5d5)
+
+
October 18, 2017
+ added Perron-Frobenius theorem for irreducible matrices with generalization
+(revision bda1f1ce8a1c)
+
+
\ No newline at end of file
diff --git a/web/entries/Probabilistic_While.html b/web/entries/Probabilistic_While.html
--- a/web/entries/Probabilistic_While.html
+++ b/web/entries/Probabilistic_While.html
@@ -1,185 +1,189 @@
Probabilistic while loop - Archive of Formal Proofs
This AFP entry defines a probabilistic while operator based on
sub-probability mass functions and formalises zero-one laws and variant
rules for probabilistic loop termination. As applications, we
implement probabilistic algorithms for the Bernoulli, geometric and
arbitrary uniform distributions that only use fair coin flips, and
-prove them correct and terminating with probability 1.
BSD License
Topics
+prove them correct and terminating with probability 1.
BSD License
Change history
+
February 2, 2018
+ Added a proof that probabilistic conditioning can be implemented by repeated sampling.
+(revision 305867c4e911)
+
We give a simple relation-algebraic semantics of read and write
operations on associative arrays. The array operations seamlessly
integrate with assignments in the Hoare-logic library. Using relation
algebras and Kleene algebras we verify the correctness of an
array-based implementation of disjoint-set forests with a naive union
-operation and a find operation with path compression.
BSD License
Topics
+operation and a find operation with path compression.
BSD License
Change history
+
June 19, 2021
+ added path halving, path splitting, relational Peano structures, union by rank
+(revision 98c7aa03457d)
+
\ No newline at end of file
diff --git a/web/entries/Stone_Relation_Algebras.html b/web/entries/Stone_Relation_Algebras.html
--- a/web/entries/Stone_Relation_Algebras.html
+++ b/web/entries/Stone_Relation_Algebras.html
@@ -1,187 +1,191 @@
Stone Relation Algebras - Archive of Formal Proofs
We develop Stone relation algebras, which generalise relation algebras
by replacing the underlying Boolean algebra structure with a Stone
algebra. We show that finite matrices over extended real numbers form
an instance. As a consequence, relation-algebraic concepts and methods
can be used for reasoning about weighted graphs. We also develop a
fixpoint calculus and apply it to compare different definitions of
-reflexive-transitive closures in semirings.
BSD License
Topics
+reflexive-transitive closures in semirings.
BSD License
Change history
+
July 5, 2017
+ generalised extended reals to linear orders
+(revision b8e703159177)
+
\ No newline at end of file
diff --git a/web/entries/Szpilrajn.html b/web/entries/Szpilrajn.html
--- a/web/entries/Szpilrajn.html
+++ b/web/entries/Szpilrajn.html
@@ -1,168 +1,171 @@
Order Extension and Szpilrajn's Extension Theorem - Archive of Formal Proofs
This entry is concerned with the principle of order extension, i.e. the extension of an order relation to a total order relation.
To this end, we prove a more general version of Szpilrajn's extension theorem employing terminology from the book "Consistency, Choice, and Rationality" by Bossert and Suzumura.
-We also formalize theorem 2.7 of their book.
BSD License
Topics
+We also formalize theorem 2.7 of their book.
BSD License
Change history
+
March 22, 2021
+ (by Lukas Stevens) generalise Szpilrajn's extension theorem and add material from the book "Consistency, Choice, and Rationality"
+