Algorithms for model checking HyperLTL and HyperCTL^*

DOI10.1007/978-3-319-21690-4_3MaRDI QIDQ1702908zbMATH OpenOpenAlexFDO

Authors Bernd Finkbeiner, Markus Rabe, César Sánchez

Publication date 1 March 2018

Full work available at URL https://doi.org/10.1007/978-3-319-21690-4_3

Mathematics Subject Classification ID

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

Recommendations

• Model checking algorithms for hyperproperties (invited paper)
• Bounded model checking for hyperproperties
• Model-Checking HyperLTL for Pushdown Systems
• HyperPCTL model checking by probabilistic decomposition
• Model checking quantitative hyperproperties

Cited in

(38)

• Team semantics for the specification and verification of hyperproperties
• Timed hyperproperties
• Propositional Dynamic Logic for Hyperproperties
• CoCon: a conference management system with formally verified document confidentiality
• Model checking hyperproperties for Markov decision processes
• Program Repair for Hyperproperties
• A temporal logic for asynchronous hyperproperties
• Constraint-based relational verification
• HyperATL*: A Logic for Hyperproperties in Multi-Agent Systems
• Model checking algorithms for hyperproperties (invited paper)
• Model checking data flows in concurrent network updates
• Verifying hyperliveness
• Software Verification of Hyperproperties Beyond k-Safety
• Automated hypersafety verification
• Model-Checking HyperLTL for Pushdown Systems
• Rewriting-based runtime verification for alternation-free HyperLTL
• Monitoring hyperproperties
• Compositional model checking for multi-properties
• Finite-word hyperlanguages
• Good-for-Game QPTL: An Alternating Hodges Semantics
• Bounded model checking for hyperproperties
• Efficient loop conditions for bounded model checking hyperproperties
• Explaining Hyperproperty Violations
• Runtime enforcement of hyperproperties
• AutoHyper: explicit-state model checking for HyperLTL
• Bounded model checking for asynchronous hyperproperties
• CoSMed: a confidentiality-verified social media platform
• scientific article; zbMATH DE number 7471703 (Why is no real title available?)
• On verifying timed hyperproperties
• Synthesis from hyperproperties
• HyperPCTL model checking by probabilistic decomposition
• Is Your Software on Dope?
• Information Flow Guided Synthesis
• Statistical Model Checking for Probabilistic Hyperproperties of Real-Valued Signals
• Temporal team semantics revisited
• Stack-aware hyperproperties
• scientific article; zbMATH DE number 1361475 (Why is no real title available?)
• Second-order hyperproperties

This page was built for publication: Algorithms for model checking HyperLTL and HyperCTL\(^*\)

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