KIT | KIT-Bibliothek | Impressum | Datenschutz

Deductive Verification of Concurrent Programs

Bruns, Daniel

Verification of concurrent programs still poses one of the major challenges in computer science. Several techniques to tackle this problem have been proposed. However, they often do not scale. We present an adaptation of the rely/guarantee methodology in dynamic logic. Rely/guarantee uses functional specification to symbolically describe the behavior of concurrently running threads: while each thread guarantees adherence to a specified property at any point in time, all other threads can rely on this property being established. This allows to regard threads largely in isolation--only w.r.t. an environment constrained by these specifications. While rely/guarantee based approaches often suffer from a considerable specification overhead, we complement functional thread specifications with frame conditions. We will explain our approach using a simple, but concurrent programing language. Besides the usual constructs for sequential programs, it caters for dynamic thread creation. We define semantics of concurrent programs w.r.t. an underspecified deterministic scheduling function. To formally reason about programs of this language, we introduce a novel multi-modal logic, Concurrent Dynamic Trace Logic (CDTL). ... mehr

Volltext §
DOI: 10.5445/IR/1000045641
Cover der Publikation
Zugehörige Institution(en) am KIT Institut für Theoretische Informatik (ITI)
Publikationstyp Forschungsbericht/Preprint
Publikationsjahr 2015
Sprache Englisch
Identifikator ISSN: 2190-4782
KITopen-ID: 1000045641
Verlag Karlsruher Institut für Technologie (KIT)
Umfang 57 S.
Serie Karlsruhe Reports in Informatics ; 2015,3
KIT – Die Forschungsuniversität in der Helmholtz-Gemeinschaft
KITopen Landing Page