[Club2] Einladung: A Reasoning Infrastructure for CompCert's Cminor in Isabe... - Mi 5. Mai 2021 13:30 - 14:00 (MESZ) (club2 at mailbroy.informatik.tu-muenchen.de)
piller at in.tum.de
piller at in.tum.de
Thu Apr 29 07:28:12 CEST 2021
Sie wurden zum folgenden Termin eingeladen.
Titel: A Reasoning Infrastructure for CompCert's Cminor in Isabelle/HOL
Vortragender: Maximilian KirchmeierType: Master's Thesis Presentation
Abstract: CompCertis a compiler for a large subset of ISO C99, formally
verified using the Coqproof assistant. With mythesis, I have attempted
to connect CompCert to the Isabelle/HOL universe, inorder to make it
possible for future Isabelle/HOL projects to use CompCert as aback-end for
their own verified-compilation efforts. To accomplish this, I
haveformalized Cminor (one of CompCert's intermediate languages) and built
aserialization-pathway to export Cminor programs from Isabelle and
subsequentlycompile them in CompCert. Additionally, I have set up an
separation-logicinfrastructure allowing reasoning about (basic) Cminor
programs. The resultsof these efforts will be presented in this talk.
Wann: Mi 5. Mai 2021 13:30 – 14:00 Mitteleuropäische Zeit - Berlin
Wo: https://bbb.rbg.tum.de/max-tmg-kwp
Kalender: club2 at mailbroy.informatik.tu-muenchen.de
Wer
* piller at in.tum.de- Veranstalter
* club2 at mailbroy.informatik.tu-muenchen.de
* haslbema at in.tum.de
* p.lammich at utwente.nl
* m.kirchmeier at tum.de
Termininformationen:
https://calendar.google.com/calendar/event?action=VIEW&eid=NXN1cnI2NjZkN2tqc21xZWZybDAyNjcwa3QgY2x1YjJAbWFpbGJyb3kuaW5mb3JtYXRpay50dS1tdWVuY2hlbi5kZQ&tok=NTIjc2U2ZWJlM3RvZmY0Y2g1bm11bmlibTVtOThAZ3JvdXAuY2FsZW5kYXIuZ29vZ2xlLmNvbTNkZTY3NmFhMzFhM2UzNDgzMDU1NmQ0OGE5YTAxNGUzZjU1ZDM2ZTE&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/20210429/d8c32251/attachment.htm>
-------------- next part --------------
A non-text attachment was scrubbed...
Name: not available
Type: text/calendar
Size: 2765 bytes
Desc: not available
URL: <https://mailman46.in.tum.de/pipermail/club2/attachments/20210429/d8c32251/attachment.ics>
-------------- next part --------------
A non-text attachment was scrubbed...
Name: invite.ics
Type: application/ics
Size: 2816 bytes
Desc: not available
URL: <https://mailman46.in.tum.de/pipermail/club2/attachments/20210429/d8c32251/attachment.bin>
More information about the Club2
mailing list