[Club2] 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]

Sie wurden zum folgenden Termin eingeladen.

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
       to verify an imperative implementation of the classical B-tree       
data structure.
       The implementation supports set membership and insertion 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 and       
Scala.
       We examine the runtime of all operations indirectly by  
reproducing      results
       of the logarithmic relationship between height and the number of       
nodes.
       Considering development time and lines of code,
       our approach compares well to other approaches at mechanized
       verifications of the B-tree data structure.
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/aa58deca/attachment.htm>
-------------- next part --------------
A non-text attachment was scrubbed...
Name: not available
Type: text/calendar
Size: 2781 bytes
Desc: not available
URL: <https://mailman46.in.tum.de/pipermail/club2/attachments/20210222/aa58deca/attachment.ics>
-------------- next part --------------
A non-text attachment was scrubbed...
Name: invite.ics
Type: application/ics
Size: 2833 bytes
Desc: not available
URL: <https://mailman46.in.tum.de/pipermail/club2/attachments/20210222/aa58deca/attachment.bin>