EVA STAR Trefferanzeige

Volltext Engel_Christian_pdfa.pdf1.pdf (1,7 MB)
URN (für Zitat) http://nbn-resolving.org/urn:nbn:de:swb:90-140874
Titel Deductive Verification of Safety-Critical Java Programs
Autor Engel, Christian
Institution Fakultät für Informatik (INFORMATIK)
Institut für Theoretische Informatik (ITI)
Dokumenttyp Buch
Verlag Karlsruhe
Jahr 2009
Hochschulschrift Dissertation
Fakultät für Informatik (INFORMATIK)
Institut für Theoretische Informatik (ITI)
Prüfungsdaten: 13.11.2009
Referent/Betreuer: Prof. P. Schmitt
Abstract This work investigates the application of deductive verification techniques to safety critical Java programs, in particular RTSJ programs. A focus is put on the formalization of the RTSJ memory model in dynamic logic, the utilization of a region-based memory model for ensuring non-interference and a design-by-contract based approach for the formal specification and verification of worst case memory consumption.