Techniques for the Verification of Dynamically Typed Programs

26. Oktober 2016, 14:15

Organisator:  Dipl.-Inform. Björn Engelmann

Ort:  Gebäude A03, Raum 2-209

M i t t e i l u n g 

Im Rahmen der Disputation seines Promotionsverfahrens hält Herr Dipl.-Inform. Björn Engelmann, seinen öffentlichen Vortrag zum Thema

„Techniques for the Verification of Dynamically Typed Programs“

am Mittwoch, den 26. Oktober 2016, um 14.15 Uhr im Gebäude A03, Raum 2-209.

Abstract: 

Dynamically-typed object-oriented languages enable programmers to write elegant, reusable and extensible programs. However, due to their inherent lack of static type information, the current methodology for program verification is not directly applicable to these languages. In this thesis, we aim to provide adequate verification techniques for dynamically-typed programs. To this end, we

• introduce the first sound and complete program logic for a dynamically-typed object-oriented language,
• investigate the role type information plays in program verification,
• provide a semi-automatic method to derive type information (and thus proof type safety) for dynamically-typed programs,
• introduce consensual typing, a typing discipline integrating type inference with formal verification and generalizing both soft- and gradual typing, and
• show that type-safe dynamically-typed programs can be verified just like statically-typed ones.

Mit der Teilnahme von Zuhörerinnen und Zuhörern an der anschließenden Prüfung bis 15.45 Uhr ist Herr Engelmann einverstanden.

gez. Prof. Dr.-Ing. A. Hahn