Formale Semantik
Zur Zeit arbeite ich an einer formalen, operationalen Semantik für
eine umfangreiche Teilsprache von Java einschließlich Threads
sowohl für Java-Quelltext als auch für -Bytecode. Die
Formalisierung im Theorembeweiser
Isabelle/HOL,
die auf der Jinja-Semantik von T. Nipkow und G. Klein basiert, wird als
typsicher bewiesen. Ein ebenfalls formalisierter und zu verifizierender
Complier, der Quelltextprogramme in verhaltensäquivalente
Bytecode-Programme übersetzt, gehört weiterhin dazu.
Der aktuelle Stand der Formalisierung ist im
Archive of Formal Proofs
unter dem Projekttitel
Jinja with Threads
zum Download erhältlich.
Temporale Pfadbedingungen
Weiterhin beschäftige ich mich mit temporalen Pfadbedingungen für
Programm- und Systemabhängigkeitsgraphen. Als Weiterentwicklung der
Booleschen Pfadbedingungen erhöhen sie nicht nur wesentlich die
Präzision bei der Informationsflusskontrolle mittels Slicing, sondern
können durch eine Anbindung an Model Checker ganze Programmsequenzen
automatisch generieren, für die ein entsprechender Informationsfluss
zu Tage tritt.
