[Club2] Aktualisierte Einladung: A Verified Imperative Implementation of B-Trees - Mi 3. Mär. 2021 03:00 - 03:30 (MEZ) (club2 at mailbroy.informatik.tu-muenchen.de)

[piller at in.tum.de]

Dieser Termin wurde geändert.

Titel: A Verified Imperative Implementation of B-Trees
Speaker: Nils Mündler Type: Bachelor's Thesis  
Presentation Abstract: In this thesis, we use the interactive theorem  
prover Isabelle/HOL toverify an imperative implementation of the classical  
B-tree data structure.Theimplementation supports set membership and  
insertion queries with efficientbinary search for intra-node navigation.  
This is accomplished by firstspecifying the structure abstractly in the  
functional modeling language HOL andproving functional correctness. Using  
manual refinement, we derive an imperativeimplementation in  
Imperative/HOL.  We show the validity of this refinement using the  
separation logicutilities from the Isabelle Refinement Framework. The code  
can be exported to the programming languages SML and Scala. Weexamine the  
runtime of all operations indirectly by reproducing results of  
thelogarithmic relationship between height and the number of nodes.  
Consideringdevelopment time and lines of code, our approach compares well  
to other approachesat mechanized verifications of the B-tree data  
structure.  (geändert)
Wann: Mi 3. Mär. 2021 03:00 – 03:30 Mitteleuropäische Zeit - Berlin
Wo: https://tinyurl.com/ls21coffee
Kalender: club2 at mailbroy.informatik.tu-muenchen.de
Wer
     * piller at in.tum.de- Veranstalter
     * club2 at mailbroy.informatik.tu-muenchen.de
     * n.muendler at posteo.net

Termininformationen:  
https://calendar.google.com/calendar/event?action=VIEW&eid=N21ldnJsNTk4aDRnMmg4ZHBoa2dnOXZ2Z20gY2x1YjJAbWFpbGJyb3kuaW5mb3JtYXRpay50dS1tdWVuY2hlbi5kZQ&tok=NTIjc2U2ZWJlM3RvZmY0Y2g1bm11bmlibTVtOThAZ3JvdXAuY2FsZW5kYXIuZ29vZ2xlLmNvbWQ5MDJjYzdkOWM1YzdhOTg5MDAzODEwYmU1OTc0NWYzYmViMTkwMjg&ctz=Europe%2FBerlin&hl=de&es=0

Einladung von Google Kalender: https://calendar.google.com/calendar/

Sie erhalten diese E-Mail unter club2 at mailbroy.informatik.tu-muenchen.de,  
da Sie ein Gast bei diesem Termin sind.

Lehnen Sie diesen Termin ab, um keine weiteren Informationen zu diesem  
Termin zu erhalten. Sie können auch unter  
https://calendar.google.com/calendar/ ein Google-Konto erstellen und Ihre  
Benachrichtigungseinstellungen für Ihren gesamten Kalender steuern.

Wenn Sie diese Einladung weiterleiten, kann jeder Empfänger eine Antwort an  
den Organisator senden und zur Gästeliste hinzugefügt werden. Außerdem  
könnte er weitere Nutzer einladen und Ihre Antwort ändern. Weitere  
Informationen: https://support.google.com/calendar/answer/37135#forwarding
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://mailman46.in.tum.de/pipermail/club2/attachments/20210222/eb15ada2/attachment.htm>
-------------- next part --------------
A non-text attachment was scrubbed...
Name: not available
Type: text/calendar
Size: 2692 bytes
Desc: not available
URL: <https://mailman46.in.tum.de/pipermail/club2/attachments/20210222/eb15ada2/attachment.ics>
-------------- next part --------------
A non-text attachment was scrubbed...
Name: invite.ics
Type: application/ics
Size: 2743 bytes
Desc: not available
URL: <https://mailman46.in.tum.de/pipermail/club2/attachments/20210222/eb15ada2/attachment.bin>