direkt zum Inhalt springen

direkt zum Hauptnavigationsmenü

Sie sind hier

TU Berlin

Inhalt des Dokuments


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 Download Bibtex Eintrag

Zusatzinformationen / Extras


Schnellnavigation zur Seite über Nummerneingabe