A Fixpoint Logic and Dependent Effects for Temporal Property Verification

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

Tachio Terauchi, Eric Koskinen, Hiroshi Unno, Yoji Nanjo

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

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)