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

Full work available at URL https://doi.org/10.1007/978-3-031-13185-1_17

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

• 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
• scientific article; zbMATH DE number 4124989 (Why is no real title available?)
• scientific article; zbMATH DE number 7730626 (Why is no real title available?)
• 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

(23)

• Verification of quantitative hyperproperties using trace enumeration relations
• Hyperhierarchy of semantics -- a formal framework for hyperproperties verification
• Verifying bounded subset-closed hyperproperties
• HyperATL*: A Logic for Hyperproperties in Multi-Agent Systems
• Automated hypersafety verification
• Software Verification of Hyperproperties Beyond k-Safety
• Efficient loop conditions for bounded model checking hyperproperties
• AutoHyper: explicit-state model checking for HyperLTL
• Second-order hyperproperties
• Deductive controller synthesis for probabilistic hyperproperties
• Deciding hyperproperties combined with functional specifications
• Alignment complete relational Hoare logics for some and all
• Centralized vs decentralized monitors for hyperproperties
• Centralized vs. decentralized monitors for hyperproperties
• Temporal hyperproperties for population protocols
• Symbolic execution for refuting hyperproperties
• Predicate abstraction for hyperliveness verification
• Preface of the special issue on the conference on computer-aided verification 2022
• Cartesian reachability logic: a language-parametric logic for verifying k-safety properties
• Model checking omega-regular hyperproperties with AutoHyperQ
• HyperLTL satisfiability is highly undecidable, \(\mathrm{HyperCTL}^*\) is even harder
• Extensions of HyperLTL for asynchronous hyperproperties
• Formalization of Hyper Hoare Logic: A Logic to (Dis-)Prove Program 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)