A fixpoint logic and dependent effects for temporal property verification

Yoji Nanjo, Hiroshi Unno, Eric Koskinen, Tachio Terauchi

研究成果: Conference contribution

9 被引用数 (Scopus)

抄録

Existing approaches to temporal verification of higher-order functional programs have either sacrificed compositionality in favor of achieving automation or vice-versa. In this paper we present a dependent-refinement type & effect system to ensure that well-typed programs satisfy given temporal properties, and also give an algorithmic approach - -based on deductive reasoning over a fixpoint logic - -to typing in this system. The first contribution is a novel type-and-effect system capable of expressing dependent temporal effects, which are fixpoint logic predicates on event sequences and program values, extending beyond the (non-dependent) temporal effects used in recent proposals. Temporal effects facilitate compositional reasoning whereby the temporal behavior of program parts are summarized as effects and combined to form those of the larger parts. As a second contribution, we show that type checking and typability for the type system can be reduced to solving first-order fixpoint logic constraints. Finally, we present a novel deductive system for solving such constraints. The deductive system consists of rules for reasoning via invariants and well-founded relations, and is able to reduce formulas containing both least and greatest fixpoints to predicate-based reasoning.

本文言語English
ホスト出版物のタイトルProceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2018
出版社Institute of Electrical and Electronics Engineers Inc.
ページ759-768
ページ数10
ISBN(電子版)9781450355834, 9781450355834
DOI
出版ステータスPublished - 2018 7 9
イベント33rd Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2018 - Oxford, United Kingdom
継続期間: 2018 7 92018 7 12

出版物シリーズ

名前Proceedings - Symposium on Logic in Computer Science
ISSN(印刷版)1043-6871

Other

Other33rd Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2018
国/地域United Kingdom
CityOxford
Period18/7/918/7/12

ASJC Scopus subject areas

  • ソフトウェア
  • 数学 (全般)

フィンガープリント

「A fixpoint logic and dependent effects for temporal property verification」の研究トピックを掘り下げます。これらがまとまってユニークなフィンガープリントを構成します。

引用スタイル