[Club2] Invitation: Compiler Verification for a Data Format DSL @ Wed Mar 18, 2015 14:00 - 15:00 (Club2)

[julianbrunner at gmail.com]

You have been invited to the following event.

Title: Compiler Verification for a Data Format DSL
Speaker: Sudeep Kanav
Type: Master's Thesis Presentation

Abstract:

This work deals with the verification of serialization and de-serialization  
code, which are important functions of a file system.
NICTA, in its Trustworthy File Systems project, is developing a verified  
high performance flash file system, for which the team has developed two  
domain-specific languages, i) DDSL for file system data formats and ii)  
CDSL for code implementing the actual file system logic (control code). In  
DDSL, the user can describe the physical on-disk representation of a  
logical data structure and gets automatically generated code, for  
serialization and de-serialization of this data structure, in CDSL. User is  
supposed to write the control code in CDSL. Both the generated and hand  
written CDSL code combined are then used to generate C code implementing  
the specification.

This thesis aims at verification of the code generation for serialization  
and de-serialization functions. I formalized a carefully chosen subset of  
DDSL which is able to express simple data formats, and its compiler. Then I  
formalized the notion of correctness for serialization and de-serialization  
functions, and prove that successful execution of these functions establish  
corresponding correctness predicates. In the course of proving the  
correctness of the compiler, I had to extend the CDSL formalization.
When: Wed Mar 18, 2015 14:00 - 15:00 Berlin
Where: MI 00.09.038 (Turing)
Calendar: Club2
Who:
     * Julian Brunner - creator
     * club2 at mailbroy.informatik.tu-muenchen.de
     * sudeep.kanav at tum.de

Event details:  
https://www.google.com/calendar/event?action=VIEW&eid=Z2dsYm0zZ3BvZHA5NGtzZGJkYWRjOHRsMTggY2x1YjJAbWFpbGJyb3kuaW5mb3JtYXRpay50dS1tdWVuY2hlbi5kZQ&tok=NTIjc2U2ZWJlM3RvZmY0Y2g1bm11bmlibTVtOThAZ3JvdXAuY2FsZW5kYXIuZ29vZ2xlLmNvbWZhYTc0NTRhOWQyMjI0NmY5NTljNmIwOGVhZTIxY2Q2YWFjMTQ0ZDc&ctz=Europe/Berlin&hl=en

Invitation from Google Calendar: https://www.google.com/calendar/

You are receiving this courtesy email at the account  
club2 at mailbroy.informatik.tu-muenchen.de because you are an attendee of  
this event.

To stop receiving future updates for this event, decline this event.  
Alternatively you can sign up for a Google account at  
https://www.google.com/calendar/ and control your notification settings for  
your entire calendar.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://mailmanbroy.informatik.tu-muenchen.de/pipermail/club2/attachments/20150313/70e1e786/attachment-0001.html>
-------------- next part --------------
A non-text attachment was scrubbed...
Name: not available
Type: text/calendar
Size: 2816 bytes
Desc: not available
URL: <https://mailmanbroy.informatik.tu-muenchen.de/pipermail/club2/attachments/20150313/70e1e786/attachment-0001.ics>
-------------- next part --------------
A non-text attachment was scrubbed...
Name: invite.ics
Type: application/ics
Size: 2873 bytes
Desc: not available
URL: <https://mailmanbroy.informatik.tu-muenchen.de/pipermail/club2/attachments/20150313/70e1e786/attachment-0001.bin>