direkt zum Inhalt springen

direkt zum Hauptnavigationsmenü

Sie sind hier

TU Berlin

Page Content


Formal Verification with Isabelle/HOL in Practice: Finding a Bug in the GCC Scheduler
Citation key gesellensetter07formal
Author Lars Gesellensetter and Sabine Glesner and Elke Salecker
Title of Book 12th International Workshop on Formal Methods for Industrial Critical Systems (FMICS 2007)
Year 2007
Abstract 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.
Bibtex Type of Publication Conference Article
Link to original publication Download Bibtex entry

Zusatzinformationen / Extras

Quick Access:

Schnellnavigation zur Seite über Nummerneingabe