CISPA
Browse

Explaining Hyperproperty Violations

Download (483.54 kB)
Version 2 2023-12-11, 20:15
Version 1 2023-11-29, 18:20
conference contribution
posted on 2023-12-11, 20:15 authored by Norine Coenen, Raimund Dachselt, Bernd FinkbeinerBernd Finkbeiner, Hadar Frenkel, Christopher Hahn, Tom Horak, Niklas MetzgerNiklas Metzger, Julian SiberJulian Siber
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.

History

Preferred Citation

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

Primary Research Area

  • Reliable Security Guarantees

Name of Conference

Computer Aided Verification (CAV)

Legacy Posted Date

2022-05-06

Open Access Type

  • Unknown

BibTeX

@inproceedings{cispa_all_3663, title = "Explaining Hyperproperty Violations", author = "Coenen, Norine and Dachselt, Raimund and Finkbeiner, Bernd and Frenkel, Hadar and Hahn, Christopher and Horak, Tom and Metzger, Niklas and Siber, Julian", booktitle="{Computer Aided Verification (CAV)}", year="2022", }

Usage metrics

    Categories

    No categories selected

    Exports

    RefWorks
    BibTeX
    Ref. manager
    Endnote
    DataCite
    NLM
    DC