A fixpoint logic and dependent effects for temporal property verification

DOI10.1145/3209108.3209204zbMATH Open1497.68317OpenAlexW2811195459WikidataQ130838823 ScholiaQ130838823MaRDI QIDQ5145353FDOQ5145353

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

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

zbMATH Keywords

fixpoint logictemporal verificationhigher-order programsdependent refinement typesdependent temporal effects

Mathematics Subject Classification ID

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

Cited In (6)

• Temporal refinements for guarded recursive types
• Automated temporal verification for algebraic effects
• Complementary Criteria for Testing Temporal Logic Properties
• Being Correct Is Not Enough: Efficient Verification Using Robust Linear Temporal Logic
• Fold/Unfold Transformations for Fixpoint Logic
• Temporal verification of programs via first-order fixpoint logic

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)