Personal tools

Zertifizierte Analysen

From PUMA Graduiertenkolleg

Jump to: navigation, search

Zusammenfassung

Gerade Programmanalysen und Optimierungen, die die Verlässlichkeit und/oder Effizienz von Code erhöhen sollen, sollten selbst nachweislich korrekt sein. Die Idee dieses Teilprojekts besteht darin, Verifikationsverfahren selbst auf die Implementierung von Analysatoren anzuwenden. Dadurch liefern wir hier einen Beitrag zur Realisierung eines verifizierten Compilers liefern. Allgemein erwarten wir jedoch, dass an Analysetools, die zur Zertifizierung anderer Programme eingesetzt werden sollen, generell erhöhte Anforderungen gestellt werden, zu deren Erfüllung der Verifikationsaufwand gerechtfertigt erscheint.


Themen