Software Verification of Hyperproperties Beyond k-Safety

DOI10.1007/978-3-031-13185-1_17zbMATH Open1514.68122MaRDI QIDQ6487322FDOQ6487322

Authors: Raven Beutner, Bernd Finkbeiner 

Publication date: 7 December 2022

Recommendations

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

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60)

Cites Work

• Computer Aided Verification
• The existence of refinement mappings
• Title not available (Why is that?)
• Lazy abstraction
• Model-Checking HyperLTL for Pushdown Systems
• Secure information flow by self-composition
• Permissive strategies: from parity games to safety games
• Simple relational correctness proofs for static analyses and program transformations
• Reduction
• Algorithms for model checking HyperLTL and HyperCTL\(^*\)
• The power of symbolic automata and transducers
• Modular product programs
• Predicate abstraction for program verification
• Beyond 2-safety: asymmetric product programs for relational program verification
• A constraint-based approach to solving games on infinite graphs
• Verifying hyperliveness
• Property directed self composition
• Automated hypersafety verification
• A temporal logic for asynchronous hyperproperties
• Constraint-based relational verification
• Causality-based game solving
• Continuity analysis of programs
• Title not available (Why is that?)
• Solving Games Via Three-Valued Abstraction Refinement
• Software Verification of Hyperproperties Beyond k-Safety

Cited In (11)

• HyperATL*: A Logic for Hyperproperties in Multi-Agent Systems
• Software Verification of Hyperproperties Beyond k-Safety
• Verification of quantitative hyperproperties using trace enumeration relations
• Automated hypersafety verification
• Hyperhierarchy of semantics -- a formal framework for hyperproperties verification
• Verifying bounded subset-closed hyperproperties
• Efficient loop conditions for bounded model checking hyperproperties
• AutoHyper: explicit-state model checking for HyperLTL
• Deciding hyperproperties combined with functional specifications
• Second-order hyperproperties
• Deductive controller synthesis for probabilistic hyperproperties

This page was built for publication: Software Verification of Hyperproperties Beyond k-Safety

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