Explaining Hyperproperty Violations

DOI10.1007/978-3-031-13185-1_20zbMath1514.68127MaRDI QIDQ6487323

Norine Coenen, Niklas Metzger, Bernd Finkbeiner, Raimund Dachselt, Hadar Frenkel, Christopher Hahn, Julian Siber, Unnamed Author

Publication date: 7 December 2022

Mathematics Subject Classification ID

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

Related Items (2)

Temporal causality in reactive systems ⋮ Explaining Hyperproperty Violations

Cites Work

• Unnamed Item
• Unnamed Item
• PySAT: a Python toolkit for prototyping with SAT oracles
• Algorithms for model checking HyperLTL and HyperCTL\(^*\)
• Uppaal in a nutshell
• Checking finite traces using alternating automata
• Monitoring hyperproperties
• Bounded model checking for hyperproperties
• Runtime enforcement of hyperproperties
• Causality analysis and fault ascription in component-based systems
• Synthesis from hyperproperties
• Causality Checking for Complex System Models
• Is Your Software on Dope?
• Secure information flow by self-composition
• Program Repair for Hyperproperties
• DESIGN AND SYNTHESIS OF SYNCHRONIZATION SKELETONS USING BRANCHING TIME TEMPORAL LOGIC
• Whodunit? Causal Analysis for Counterexamples
• Explaining Counterexamples Using Causality
• A generalization of Berger’s almost \frac{1}4-pinched manifolds theorem. I
• The First-Order Logic of Hyperproperties
• Team semantics for the specification and verification of hyperproperties
• Alternating automata: Unifying truth and validity checking for temporal logics
• What causes a system to satisfy a specification?
• Causes and Explanations: A Structural-Model Approach. Part I: Causes
• Causes and Explanations: A Structural-Model Approach. Part II: Explanations
• Tools and Algorithms for the Construction and Analysis of Systems
• Computer Aided Verification
• Tools and Algorithms for the Construction and Analysis of Systems
• The Keys to Decidable HyperLTL Satisfiability: Small Models or Very Simple Formulas
• Bounded model checking using satisfiability solving
• Model checking quantitative hyperproperties
• Verifying hyperliveness
• HyperLTL Satisfiability Is Σ₁¹-Complete, HyperCTL* Satisfiability Is Σ₁²-Complete.
• Explaining Hyperproperty Violations

This page was built for publication: Explaining Hyperproperty Violations