Die Dozenten der Informatik-Institute der Technischen Universität Braunschweig laden im Rahmen des Informatik-Kolloquiums zu folgendem Vortrag ein:
Prof. Dr. Reiner Hähnle, Chalmers University of Technology, Göteborg: Deductive Program Specialisation & Compilation
Beginn: 23.05.2011, 17:00 Uhr Ort: TU Braunschweig, Informatikzentrum, Mühlenpfordtstraße 23, 1. OG, Hörsaal M 160 Webseite: http://www.ibr.cs.tu-bs.de/cal/kolloq/2011-05-23-haehnle.html Kontakt: Dr.-Ing. Ina Schaefer
Symbolic execution of programs is a versatile software analysis technique that recently enjoyed much renewed interest. Traditional usage of symbolic execution in a logic-based setting includes formal verification and model checking, however, symbolic execution engines for Java or bytecode provide also a basis of glass-box test case generation, visualisation of program dynamics, or resource analysis. In this talk we present yet another take on symbolic execution: we show that symbolic execution, when viewed as an advanced forward analysis performed on the abstract syntax tree of a program, can be combined with first-order reasoning, partial evaluation, and usage analysis to implement provably correct program specialization and compilation.