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.