KIT | KIT-Bibliothek | Impressum | Datenschutz

Deductive Verification of Concurrent Programs and its Application to Secure Information Flow for Java

Grahl, Daniel

Abstract:
Formal verification of concurrent programs still poses a major challenge in computer science. Our approach is an adaptation of the modular rely/guarantee methodology in dynamic logic. Besides functional properties, we investigate language-based security. Our verification approach extends naturally to multi-threaded Java and we present an implementation in the KeY verification system. We propose natural extensions to JML regarding both confidentiality properties and multi-threaded programs.

Open Access Logo


Volltext §
DOI: 10.5445/IR/1000050695
Cover der Publikation
Zugehörige Institution(en) am KIT Institut für Theoretische Informatik (ITI)
Publikationstyp Hochschulschrift
Publikationsjahr 2015
Sprache Englisch
Identifikator urn:nbn:de:swb:90-506951
KITopen-ID: 1000050695
Verlag KIT, Karlsruhe
Art der Arbeit Dissertation
Fakultät Fakultät für Informatik (INFORMATIK)
Institut Institut für Theoretische Informatik (ITI)
Prüfungsdaten 29.10.2015
Referent/Betreuer Prof. B. Beckert
KIT – Die Forschungsuniversität in der Helmholtz-Gemeinschaft
KITopen Landing Page