[Club2] 21.06.2010 -- Verification of BDD algorithms by refinement of trees

[Florian Haftmann]

Mon 21.06.2010 15:00:00 / Alan Turing (00.09.055)
-------------------------------------------------

Mathieu Giorgino: Verification of BDD algorithms by refinement of trees

We present our last case study in mechanical verification of graph
manipulating algorithms: We prove the correctness of a family of
algorithms constructing Binary Decision Diagrams in a monadic style. It
distinguishes itself from previous verification efforts in two respects:
Firstly, building the BDD structure is guided by a primitive recursive
descent which makes the proof of termination trivial. Secondly, the
development is modular: it is parametrized by primitives manipulating
high-level hash tables that can be realized by several implementations.

-- 

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/20100617/c05334dc/attachment.asc>