抄録
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 |
| 巻 | Part F138033 |
| 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 9 → 2018 7 12 |
Other
| Other | 33rd Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2018 |
|---|---|
| 国 | United Kingdom |
| 市 | Oxford |
| 期間 | 18/7/9 → 18/7/12 |
Fingerprint
ASJC Scopus subject areas
- Software
- Mathematics(all)
これを引用
A fixpoint logic and dependent effects for temporal property verification. / Nanjo, Yoji; Unno, Hiroshi; Koskinen, Eric; Terauchi, Tachio.
Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2018. 巻 Part F138033 Institute of Electrical and Electronics Engineers Inc., 2018. p. 759-768.研究成果: Conference contribution
}
TY - GEN
T1 - A fixpoint logic and dependent effects for temporal property verification
AU - Nanjo, Yoji
AU - Unno, Hiroshi
AU - Koskinen, Eric
AU - Terauchi, Tachio
PY - 2018/7/9
Y1 - 2018/7/9
N2 - 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.
AB - 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.
KW - Dependent refinement types
KW - Dependent temporal effects
KW - Fixpoint logic
KW - Higher-order programs
KW - Temporal verification
UR - http://www.scopus.com/inward/record.url?scp=85051110769&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=85051110769&partnerID=8YFLogxK
U2 - 10.1145/3209108.3209204
DO - 10.1145/3209108.3209204
M3 - Conference contribution
VL - Part F138033
SP - 759
EP - 768
BT - Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2018
PB - Institute of Electrical and Electronics Engineers Inc.
ER -