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

DOI10.1145/3373718.3394766MaRDI QIDQ5145688zbMATH OpenOpenAlexWikidataFDO

Authors 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

zbMATH Keywords

program verificationcomputabilityfixed-point logicanalytical hierarchybranching-time propertyconstrained Horn clause

Mathematics Subject Classification ID

Computer science (68-XX)

Recommendations

• Algorithmic properties of branching-time logics
• On the Complexity of Branching-Time Logics
• Learning to verify branching time properties
• scientific article; zbMATH DE number 3907752
• 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

Cited in

(2)

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

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)