On Computability of Logical Approaches to Branching-Time Property Verification of Programs

DOI10.1145/3373718.3394766OpenAlexW3029393106WikidataQ130947770 ScholiaQ130947770MaRDI QIDQ5145688FDOQ5145688

Takeshi Tsukada

Publication date: 21 January 2021

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

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

Recommendations

• Algorithmic properties of branching-time logics
• On the Complexity of Branching-Time Logics
• Learning to verify branching time properties
• [[:Publication:3685173|Title not available (Why is that?)]]
• A New Approach to Bounded Model Checking for Branching Time Logics
• Towards a theory of time-bounded verification
• Deciding full branching time logic by program transformation
• On the proof complexity of logics of bounded branching
• Modalities for model checking: Branching time logic strikes back
• Extending co-logic programs for branching-time model checking

zbMATH Keywords

program verificationcomputabilityfixed-point logicanalytical hierarchybranching-time propertyconstrained Horn clause

Mathematics Subject Classification ID

Computer science (68-XX)

Cited In (2)

• On higher-order reachability games vs may reachability
• An overview of the HFL model checking project

This page was built for publication: On Computability of Logical Approaches to Branching-Time Property Verification of Programs

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