Email Gateway (Aug 19 2022 at 15:40): Email Gateway (Aug 19 2022 at 15:40):From: Tobias Nipkow <nipkow@in.tum.de>
The Archive of Formal proofs is now available for Isabelle2014 at http://afp.sf.net.
The following development entries are now available as release versions from the
front page:
Skew Heap
Tobias Nipkow
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.
http://afp.sourceforge.net/entries/Skew_Heap.shtml
Splay Tree
Tobias Nipkow
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. The amortized complexity of splay trees is analyzed in
the AFP entry Amortized Complexity.
http://afp.sourceforge.net/entries/Splay_Tree.shtml
Amortized Complexity Verified
Tobias Nipkow
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 two non-trivial ones: skew heaps and splay trees. In the same
spirit we show that the move-to-front algorithm for the list update problem is
2-competitive.
A preliminary paper describing this research has been presented at the Isabelle
Workshop 2014.
http://afp.sourceforge.net/entries/Amortized_Complexity.shtml
Haskell's Show-Class in Isabelle/HOL
Christian Sternagel and René Thiemann
We implemented a type-class for pretty-printing, similar to Haskell's
Show-class. Moreover, we provide instantiations for Isabelle/HOL’s standard
types like bool, prod, sum, nats, ints, and rats. It is further possible, to
automatically derive pretty-printer for arbitrary user defined datatypes similar
to Haskell's "deriving Show".
http://afp.sourceforge.net/entries/Show.shtml
Formal Specification of a Generic Separation Kernel
Freek Verbeek, Sergey Tverdyshev, Oto Havle, Holger Blasum, Bruno Langenstein,
Werner Stephan, Yakoub Nemouchi, Abderrahmane Feliachi, Burkhart Wolff and
Julien Schmaltz
Intransitive noninterference has been a widely studied topic in the last few
decades. Several well-established methodologies apply interactive theorem
proving to formulate a noninterference theorem over abstract academic models. In
joint work with several industrial and academic partners throughout Europe, we
are helping in the certification process of PikeOS, an industrial separation
kernel developed at SYSGO. In this process, established theories could not be
applied. We present a new generic model of separation kernels and a new theory
of intransitive noninterference. The model is rich in detail, making it suitable
for formal verification of realistic and industrial systems such as PikeOS.
Using a refinement-based theorem proving approach, we ensure that proofs remain
manageable.
http://afp.sourceforge.net/entries/CISC-Kernel.shtml
Email Gateway (Aug 19 2022 at 15:40):From: Christian Sternagel <c.sternagel@gmail.com>
The download link, although labeled afp-2014-08-29.tar.gz does still
point to afp-2014-07-18.tar.gz.
cheers
chris
Last updated: Apr 23 2024 at 20:15 UTC