A fixpoint logic and dependent effects for temporal property verification

DOI10.1145/3209108.3209204MaRDI QIDQ5145353zbMATH OpenOpenAlexWikidataFDO

Authors Yoji Nanjo, Hiroshi Unno, Eric Koskinen, Tachio Terauchi

Publication date 20 January 2021

Published in Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1145/3209108.3209204

zbMATH Keywords

dependent refinement typesdependent temporal effectsfixpoint logichigher-order programstemporal verification

Mathematics Subject Classification ID

Logic in computer science (03B70) Specification and verification (program logics, model checking, etc.) (68Q60)

Recommendations

• Local temporal reasoning
• Temporal refinements for guarded recursive types
• Temporal verification of higher-order functional programs
• Programming Languages and Systems
• A new refinement type system for automated \(\nu\text{HFL}_\mathbb{Z}\) validity checking

Cited in

(8)

• Temporal refinements for guarded recursive types
• Complementary Criteria for Testing Temporal Logic Properties
• Local temporal reasoning
• Being Correct Is Not Enough: Efficient Verification Using Robust Linear Temporal Logic
• Fold/unfold transformations for fixpoint logic
• Automated temporal verification for algebraic effects
• Temporal verification of programs via first-order fixpoint logic
• Infinitary refinement types for temporal properties in Scott domains

This page was built for publication: A fixpoint logic and dependent effects for temporal property verification

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5145353)