DocumentCode
2141087
Title
Extending ITL with Interleaved Programs for Interactive Verification
Author
Schellhorn, Gerhard
Author_Institution
Inst. for Software & Syst. Eng., Univ. of Augsburg, Augsburg, Germany
fYear
2011
fDate
12-14 Sept. 2011
Firstpage
7
Lastpage
7
Abstract
The talk presents extensions of ITL that make it a powerful logic to reason about interleaved programs with recursive procedures. The extensions have been implemented in the interactive theorem prover KIV.
Keywords
reasoning about programs; temporal logic; theorem proving; ITL; KIV; interactive theorem prover; interactive verification; interleaved program; interval temporal logic; recursive procedure; Artificial intelligence; Calculus; Cognition; Compounds; Hardware; Semantics; Software; Compositional Reasoning; Concurrency; Interval Temporal Logic; Rely-Guarantee Reasoning;
fLanguage
English
Publisher
ieee
Conference_Titel
Temporal Representation and Reasoning (TIME), 2011 Eighteenth International Symposium on
Conference_Location
Lubeck
ISSN
1530-1311
Print_ISBN
978-1-4577-1242-5
Type
conf
DOI
10.1109/TIME.2011.31
Filename
6065221
Link To Document