Software Verification of Hyperproperties Beyond k-Safety

DOI10.1007/978-3-031-13185-1_17MaRDI QIDQ6487322zbMATH OpenFDO

Authors Raven Beutner, Bernd Finkbeiner

Publication date 7 December 2022

Copyright license Creative Commons Attribution 4.0 International

Mathematics Subject Classification ID

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

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

Cites work

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

Cited in

(11)

• HyperATL*: A Logic for Hyperproperties in Multi-Agent Systems
• Verification of quantitative hyperproperties using trace enumeration relations
• Software Verification of Hyperproperties Beyond k-Safety
• 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)