KIT | KIT-Bibliothek | Impressum | Datenschutz

Dynamic Logic with Trace Semantics

Beckert, Bernhard ORCID iD icon 1; Bruns, Daniel 1
1 Karlsruher Institut für Technologie (KIT)

Abstract:

Dynamic logic is an established instrument for program verification and for reasoning about the semantics of programs and programming languages. In this paper, we define an extension of dynamic logic, called Dynamic Trace Logic (DTL), which combines the expressiveness of program logics such as dynamic logic with that of temporal logic. And we present a sound and relatively complete sequent calculus for proving validity of DTL formulae. Due to its expressiveness, DTL can serve as a basis for proving functional and information-flow properties in concurrent programs, among other applications.


Volltext §
DOI: 10.5445/IR/1000034593
Scopus
Zitationen: 10
Cover der Publikation
Zugehörige Institution(en) am KIT Institut für Theoretische Informatik (ITI)
Kompetenzzentrum für angewandte Sicherheitstechnologie (KASTEL)
Publikationstyp Proceedingsbeitrag
Publikationsjahr 2013
Sprache Englisch
Identifikator ISBN: 978-3-642-38573-5
ISSN: 0302-9743
urn:nbn:de:swb:90-345936
KITopen-ID: 1000034593
HGF-Programm 46.12.03 (POF II, LK 01)
Erschienen in Automated Deduction - CADE-24 : 24th International Conference on Automated Deduction, Lake Placid, NY, USA, June 9-14, 2013, Proceedings. Ed.: M.P. Bonacina
Verlag Springer-Verlag
Seiten 315 - 329
Serie Lecture Notes in Computer Science ; 7898
Projektinformation KASTEL I (BMBF, 01BY1172 / 16BY1172)
Nachgewiesen in Scopus
KIT – Die Forschungsuniversität in der Helmholtz-Gemeinschaft
KITopen Landing Page