direkt zum Inhalt springen

direkt zum Hauptnavigationsmenü

Sie sind hier

TU Berlin

Inhalt des Dokuments

Publikationen

Formal Verification with Isabelle/HOL in Practice: Finding a Bug in the GCC Scheduler
Zitatschlüssel gesellensetter07formal
Autor Lars Gesellensetter and Sabine Glesner and Elke Salecker
Buchtitel 12th International Workshop on Formal Methods for Industrial Critical Systems (FMICS 2007)
Jahr 2007
Zusammenfassung Software bugs can cause tremendous financial loss and are a serious threat to life or physical condition in safety-critical areas. Formal software verification with theorem provers aims at ensuring that no errors are present but is too expensive to be employed for full-scale systems. We show that these costs can be reduced significantly by reusing proofs and by the checker approach. We demonstrate the applicability of our approach by a case study checking the correctness of the scheduler of the popular GCC compiler for a VLIW processor where we indeed found an error.
Typ der Publikation Conference Article
Link zur Originalpublikation [1] Download Bibtex Eintrag [2]
------ Links: ------

Zusatzinformationen / Extras

Direktzugang

Schnellnavigation zur Seite über Nummerneingabe

Copyright TU Berlin 2008