Explaining Hyperproperty Violations
Research output: Contribution to book/Conference proceedings/Anthology/Report › Conference contribution › Contributed › peer-review
Contributors
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.
Details
Original language | English |
---|---|
Title of host publication | Computer Aided Verification |
Editors | Sharon Shoham, Yakir Vizel |
Publisher | Springer Science and Business Media B.V. |
Pages | 407-429 |
Number of pages | 23 |
ISBN (electronic) | 978-3-031-13185-1 |
ISBN (print) | 978-3-031-13184-4 |
Publication status | Published - 2022 |
Peer-reviewed | Yes |
Publication series
Series | Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) |
---|---|
Volume | 13371 LNCS |
ISSN | 0302-9743 |
Conference
Title | 34th International Conference on Computer Aided Verification, CAV 2022 |
---|---|
Duration | 7 - 10 August 2022 |
City | Haifa |
Country | Israel |
External IDs
ORCID | /0000-0002-2176-876X/work/159171489 |
---|