Local temporal reasoning

Eric Koskinen, Tachio Terauchi

研究成果: Conference contribution

9 引用 (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
外部発表Yes
イベント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

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
Vienna
期間14/7/1414/7/18

Fingerprint

Temporal Reasoning
Temporal logic
Specifications
Safety
Trace
Higher Order
Liveness
Temporal Logic
Type Systems
Termination
Refinement
Reasoning
Specification
Target
Software

ASJC Scopus subject areas

  • Computational Theory and Mathematics
  • Applied Mathematics

これを引用

Koskinen, E., & Terauchi, T. (2014). Local temporal reasoning. : 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 [59] Association for Computing Machinery. https://doi.org/10.1145/2603088.2603138

Local temporal reasoning. / Koskinen, Eric; Terauchi, Tachio.

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, 2014. 59.

研究成果: Conference contribution

Koskinen, E & Terauchi, T 2014, Local temporal reasoning. : 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., 59, Association for Computing Machinery, 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, 14/7/14. https://doi.org/10.1145/2603088.2603138
Koskinen E, Terauchi T. Local temporal reasoning. : 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. 2014. 59 https://doi.org/10.1145/2603088.2603138
Koskinen, Eric ; Terauchi, Tachio. / Local temporal reasoning. 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, 2014.
@inproceedings{e4cb8014b3354352bb0e5b0adc797621,
title = "Local temporal reasoning",
abstract = "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.",
keywords = "Formal verification, Higher-order programs, Model checking, Program analysis, Temporal logic",
author = "Eric Koskinen and Tachio Terauchi",
year = "2014",
doi = "10.1145/2603088.2603138",
language = "English",
isbn = "9781450328869",
booktitle = "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",
publisher = "Association for Computing Machinery",

}

TY - GEN

T1 - Local temporal reasoning

AU - Koskinen, Eric

AU - Terauchi, Tachio

PY - 2014

Y1 - 2014

N2 - 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.

AB - 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.

KW - Formal verification

KW - Higher-order programs

KW - Model checking

KW - Program analysis

KW - Temporal logic

UR - http://www.scopus.com/inward/record.url?scp=84905977424&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=84905977424&partnerID=8YFLogxK

U2 - 10.1145/2603088.2603138

DO - 10.1145/2603088.2603138

M3 - Conference contribution

AN - SCOPUS:84905977424

SN - 9781450328869

BT - 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

PB - Association for Computing Machinery

ER -