AutoHyper: explicit-state model checking for HyperLTL

DOI10.1007/978-3-031-30823-9_8MaRDI QIDQ6535349zbMATH OpenFDO

Authors Raven Beutner, Bernd Finkbeiner

Publication date 13 December 2023

Copyright license Creative Commons Attribution 4.0 International

Full work available at URL https://doi.org/10.1007/978-3-031-30823-9_8

Mathematics Subject Classification ID

Temporal logic (03B44) Specification and verification (program logics, model checking, etc.) (68Q60)

Recommendations

• Algorithms for model checking HyperLTL and HyperCTL^*
• Verifying hyperliveness
• Model checking algorithms for hyperproperties (invited paper)
• Model-Checking HyperLTL for Pushdown Systems

Cites work

• A new solution of Dijkstra's concurrent programming problem
• Algorithms for model checking HyperLTL and HyperCTL^*
• Bounded model checking for hyperproperties
• Efficient reduction of nondeterministic automata with application to language inclusion testing
• FORQ-Based Language Inclusion Formal Testing
• From Nondeterministic B\"uchi and Streett Automata to Deterministic Parity Automata
• From Spot 2.0 to Spot 2.10: What’s New?
• scientific article; zbMATH DE number 177248 (Why is no real title available?)
• scientific article; zbMATH DE number 1796153 (Why is no real title available?)
• scientific article; zbMATH DE number 1903365 (Why is no real title available?)
• scientific article; zbMATH DE number 2102695 (Why is no real title available?)
• scientific article; zbMATH DE number 5585443 (Why is no real title available?)
• scientific article; zbMATH DE number 7730605 (Why is no real title available?)
• scientific article; zbMATH DE number 7730626 (Why is no real title available?)
• HyperATL*: A Logic for Hyperproperties in Multi-Agent Systems
• Is Your Software on Dope?
• Secure information flow by self-composition
• Software Verification of Hyperproperties Beyond k-Safety
• Temporal causality in reactive systems
• Verification, Model Checking, and Abstract Interpretation
• Verifying hyperliveness

Cited in

(10)

• Model-Checking HyperLTL for Pushdown Systems
• Verifying hyperliveness
• Automated hypersafety verification
• Second-order hyperproperties
• Symbolic execution for refuting hyperproperties
• Predicate abstraction for hyperliveness verification
• Counterfactuals modulo temporal logics
• Model checking omega-regular hyperproperties with AutoHyperQ
• HyperLTL satisfiability is highly undecidable, \(\mathrm{HyperCTL}^*\) is even harder
• Complexity of model checking second-order hyperproperties on finite structures

This page was built for publication: AutoHyper: explicit-state model checking for HyperLTL

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