Institute of Computer Languages
Compilers and Languages Group

Talks 2005 - Egon Börger

The Compilers and Languages Group invites you to a talk given by

Prof. Dr. Egon Börger

Dipartimento di Informatica University di Pisa, Italien on

Adding a Semantical Foundation for Program Correctness to Hoare's Verifying Compiler Challenge

Date:	Tuesday, September 20th, 2005
Time:	11:00 (s.t.)
Location:	TU Wien, Elektrotechnik, EI HS 2 Pichelmayer Hörsaal, Gusshausstrasse 25-29 (voraussichtlich)

Abstract:

In JACM 50.1 (2003) T. Hoare proposes the construction of a verifiying compiler as "a grand challenge for computing research". The concept of such a compiler is focussed on the correctness of programs: syntactical software representations of computer-based systems, to-be-compiled by the verifying compiler. In this talk we outline an approach to relate what the verifying compiler verifies to the definition and analysis (experimental validation and mathematical verification) of the application-content of programs. The underlying Abstract State Machines method for high-level system design and analysis bridges the gap between informal requirements and detailed code by combining application-centric experimentally validatable system modeling with mathematically verifiable refinements of abstract models to compiler-verifiable code.

We illustrate the approach by work on compiler verification for languages like Prolog, Occam, Java, C#.

About Prof. Dr. Egon Börger:

Egon Börger: from 1965-1971 studied philosophy, logic and mathematics in Paris (Sorbonne), Louvain (Belgium) and Muenster (Germany). Doctoral degree (1971) and Habilitation (1976) in mathematics from the university of Muenster. Lecturer and professor in logic and computer science at the universities of Salerno (Italy) 1972-1976, Muenster 1976-1978, Dortmund (Germany) 1978-1985, Udine (Italy) 1982/83 and since 1985 Pisa (Italy). Guest researcher in numerous universities in Europe and US and at IBM Scientific Center (Heidelberg), Siemens Corporate Research (Munich), Microsoft Research (Redmond) and SAP Research (Karlsruhe). (Co)Author of four books and of over 100 research papers in logic and computer science. Current research interest in rigorous methods and their industrial application for the design and the analysis of hardware/software systems.