Explaining Hyperproperty Violations

Coenen, Norine and Dachselt, Raimund and Finkbeiner, Bernd and Frenkel, Hadar and Hahn, Christopher and Horak, Tom and Metzger, Niklas and Siber, Julian
(2022) Explaining Hyperproperty Violations.
In: 34th International Conference on Computer Aided Verification (CAV 22).
Conference: CAV Computer Aided Verification
(Submitted)

[img]
Preview
 Text
Explaining_hyperproperty_violations.pdf
Download (495kB) | Preview

Abstract

Hyperproperties relate multiple computation traces to each other. Model checkers for hyperproperties thus return, in case a system model violates the specification, a set of traces as a counterexample. Fixing the erroneous relations between traces in the system that led to the counterexample is a difficult manual effort that highly benefits from additional explanations. In this paper, we present an explanation method for counterexamples to hyperproperties described in the specification logic HyperLTL. We extend Halpern and Pearl's definition of actual causality to sets of traces witnessing the violation of a HyperLTL formula, which allows us to identify the events that caused the violation. We report on the implementation of our method and show that it significantly improves on previous approaches for analyzing counterexamples returned by HyperLTL model checkers.

Item Type: Conference or Workshop Item (A Paper) (Paper)
Divisions: Bernd Finkbeiner (Reactive Systems Group, RSG)
Conference: CAV Computer Aided Verification
Depositing User: Christopher Hahn
Date Deposited: 06 May 2022 08:57
Last Modified: 06 May 2022 08:57
Primary Research Area: NRA2: Reliable Security Guarantees
URI: https://publications.cispa.saarland/id/eprint/3663

Actions

Actions (login required)

View Item View Item
CISPA is powered by EPrints 3 which is developed by the School of Electronics and Computer Science at the University of Southampton. More information and software credits.