Local temporal reasoning

Eric Koskinen, Tachio Terauchi

研究成果: Conference contribution

15 被引用数 (Scopus)

抄録

We present the first method for reasoning about temporal logic properties of higher-order, infinite-data programs. By distinguishing between the finite traces and infinite traces in the specification, we obtain rules that permit us to reason about the temporal behavior of program parts via a type-and-effect system, which is then able to compose these facts together to prove the overall target property of the program. The type system alone is strong enough to derive many temporal safety properties using refinement types and temporal effects. We also show how existing techniques can be used as oracles to provide liveness information (e.g. termination) about program parts and that the type-and-effect system can combine this information with temporal safety information to derive nontrivial temporal properties. Our work has application toward verification of higher-order software, as well as modular strategies for procedural programs.

本文言語English
ホスト出版物のタイトルProceedings of the Joint Meeting of the 23rd EACSL Annual Conference on Computer Science Logic, CSL 2014 and the 29th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2014
出版社Association for Computing Machinery
ISBN(印刷版)9781450328869
DOI
出版ステータスPublished - 2014
外部発表はい
イベントJoint Meeting of the 23rd Annual EACSL Conference on Computer Science Logic, CSL 2014 and the 29th Annual ACM/ IEEE Symposium on Logic in Computer Science, LICS 2014 - Vienna, Austria
継続期間: 2014 7月 142014 7月 18

出版物シリーズ

名前Proceedings of the Joint Meeting of the 23rd EACSL Annual Conference on Computer Science Logic, CSL 2014 and the 29th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2014

Other

OtherJoint Meeting of the 23rd Annual EACSL Conference on Computer Science Logic, CSL 2014 and the 29th Annual ACM/ IEEE Symposium on Logic in Computer Science, LICS 2014
国/地域Austria
CityVienna
Period14/7/1414/7/18

ASJC Scopus subject areas

  • 計算理論と計算数学
  • 応用数学

フィンガープリント

「Local temporal reasoning」の研究トピックを掘り下げます。これらがまとまってユニークなフィンガープリントを構成します。

引用スタイル