Title :
Extending ITL with Interleaved Programs for Interactive Verification
Author :
Schellhorn, Gerhard
Author_Institution :
Inst. for Software & Syst. Eng., Univ. of Augsburg, Augsburg, Germany
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;
Conference_Titel :
Temporal Representation and Reasoning (TIME), 2011 Eighteenth International Symposium on
Conference_Location :
Lubeck
Print_ISBN :
978-1-4577-1242-5
DOI :
10.1109/TIME.2011.31
