Nick Benton

(Microsoft Research, Cambridge),

"Proving high-level properties of low-level code"

(Vortrag im Rahmen der "Distinguished Lecture Series" des Max Planck Instituts für Software-Systeme)

The foundations both of first-order imperative languages and of higher-order functional ones have been fairly well understood since the 1970s. But good models and reasoning principles for the mix of higher-order features and dynamically allocated mutable storage have proved hard to find, although most programming languages, from machine code to C# and ML, feature just such a combination. A number of exciting logical and semantic developments, including separation, relational program logics and step-indexing, have now started to let us model, specify and verify programs in these languages. At the same time, advances in mechanized reasoning (both automatic theorem provers and proof assistants) are making it more feasible to apply our theories to realistic programs and systems. In this talk, I'll survey some of these theoretical ideas and show how we have applied them in machine-formalized proofs of compiler correctness, addressing the question of just what it means for a piece of machine code to implement correctly a phrase of a typed high-level language.

Zeit:	Mittwoch, 24. Februar 2010, 15:30 Uhr
Ort:	Saarbrücken, Gebäude MPI-SWS, Raum 019
Hinweis:	Der Vortrag wird live an die TU Kaiserslautern Gebäude 49 Raum 206 übertragen.