Interleaved Programs and Rely-Guarantee Reasoning with ITL

This paper presents a logic that extends basic ITL with explicit, interleaved programs. The calculus is based on symbolic execution, as previously described. We extend this former work here, by integrating the logic with higher-order logic, adding recursive procedures and rules to reason about fairn...

Full description

Saved in:
Bibliographic Details
Main Authors: Schellhorn, G., Tofan, B., Ernst, G., Reif, W.
Format: Conference Proceeding
Language:English
Subjects:
Calculus
Cognition
Compositional Reasoning
Computer languages
Concurrency
Interval Temporal Logic
Rely-Guarantee Reasoning
Schedules
Semantics
Vectors
Citations: Items that cite this one
Online Access:Request full text
Tags: Add Tag
No Tags, Be the first to tag this record!
Description
Summary:This paper presents a logic that extends basic ITL with explicit, interleaved programs. The calculus is based on symbolic execution, as previously described. We extend this former work here, by integrating the logic with higher-order logic, adding recursive procedures and rules to reason about fairness. Further, we show how rules for rely-guarantee reasoning can be derived and outline the application of some features to verify concurrent programs in practice. The logic is implemented in the interactive verification environment KIV.
ISSN:1530-1311
2332-6468
DOI:10.1109/TIME.2011.12