[Club2] Mon Oct. 4th 2011, 10:00: Functional Binomial Queues in Isabelle/HOL

[Florian Haftmann]

On Mon Oct. 4th 2011, 10 o'clock René Neumann will give a talk on his
guided research "Functional Binomial Queues in Isabelle/HOL" in the
seminar room Alan Turing (00.09.055).

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. We show the proven parts within the needed constraints and also
elaborate on the discovered problems and obstacles.

-- 

Home:
http://www.in.tum.de/~haftmann

PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de

-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 262 bytes
Desc: OpenPGP digital signature
URL: <https://mailmanbroy.informatik.tu-muenchen.de/mailman/private/club2/attachments/20100927/688b5ad8/attachment.asc>