TITEL: Adding a Semantical Foundation for Program Correctness to Hoare's Verifying Compiler Challenge =================================================================== 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#. ==================================================================== Kurzbiographie zu Professor 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. ====================================================================