A fixpoint logic and dependent effects for temporal property verification

Yoji Nanjo, Hiroshi Unno, Eric Koskinen, Tachio Terauchi

    研究成果: Conference contribution

    3 引用 (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
    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 92018 7 12

    Other

    Other33rd Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2018
    United Kingdom
    Oxford
    期間18/7/918/7/12

    Fingerprint

    Fixpoint
    Automation
    Logic
    Dependent
    Reasoning
    Deductive System
    Compositionality
    Constraint Solving
    Predicate Logic
    Type Systems
    Predicate
    Refinement
    Higher Order
    First-order
    Invariant

    ASJC Scopus subject areas

    • Software
    • Mathematics(all)

    これを引用

    Nanjo, Y., Unno, H., Koskinen, E., & Terauchi, T. (2018). A fixpoint logic and dependent effects for temporal property verification. : Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2018 (巻 Part F138033, pp. 759-768). Institute of Electrical and Electronics Engineers Inc.. https://doi.org/10.1145/3209108.3209204

    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

    Nanjo, Y, Unno, H, Koskinen, E & Terauchi, T 2018, A fixpoint logic and dependent effects for temporal property verification. : Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2018. 巻. Part F138033, Institute of Electrical and Electronics Engineers Inc., pp. 759-768, 33rd Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2018, Oxford, United Kingdom, 18/7/9. https://doi.org/10.1145/3209108.3209204
    Nanjo Y, Unno H, Koskinen E, Terauchi T. A fixpoint logic and dependent effects for temporal property verification. : 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 https://doi.org/10.1145/3209108.3209204
    Nanjo, Yoji ; Unno, Hiroshi ; Koskinen, Eric ; Terauchi, Tachio. / A fixpoint logic and dependent effects for temporal property verification. 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. pp. 759-768
    @inproceedings{622fa107b4ec4ad49738e89aec730a7a,
    title = "A fixpoint logic and dependent effects for temporal property verification",
    abstract = "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.",
    keywords = "Dependent refinement types, Dependent temporal effects, Fixpoint logic, Higher-order programs, Temporal verification",
    author = "Yoji Nanjo and Hiroshi Unno and Eric Koskinen and Tachio Terauchi",
    year = "2018",
    month = "7",
    day = "9",
    doi = "10.1145/3209108.3209204",
    language = "English",
    volume = "Part F138033",
    pages = "759--768",
    booktitle = "Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2018",
    publisher = "Institute of Electrical and Electronics Engineers Inc.",

    }

    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 -