Algorithms for model checking HyperLTL and HyperCTL^*

DOI10.1007/978-3-319-21690-4_3zbMATH Open1381.68161OpenAlexW1213177963MaRDI QIDQ1702908FDOQ1702908

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

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

Mathematics Subject Classification ID

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

Cited In (38)

• Propositional Dynamic Logic for Hyperproperties
• Timed hyperproperties
• CoCon: a conference management system with formally verified document confidentiality
• Program Repair for Hyperproperties
• HyperATL*: A Logic for Hyperproperties in Multi-Agent Systems
• Model checking hyperproperties for Markov decision processes
• A temporal logic for asynchronous hyperproperties
• Constraint-based relational verification
• Model checking algorithms for hyperproperties (invited paper)
• Verifying hyperliveness
• Software Verification of Hyperproperties Beyond k-Safety
• Automated hypersafety verification
• Model checking data flows in concurrent network updates
• 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
• On verifying timed hyperproperties
• Title not available (Why is that?)
• 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
• Title not available (Why is that?)
• Second-order hyperproperties
• Team semantics for the specification and verification of 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)