Visualizing Game-Based Certificates for Hyperproperty Verification
Fuente:
arXiv
Gespeichert in:
| Hauptverfasser: | , , |
|---|---|
| Format: | Preprint |
| Veröffentlicht: |
2025
|
| Schlagworte: | |
| Online-Zugang: | |
| Tags: |
Tag hinzufügen
Keine Tags, Fügen Sie den ersten Tag hinzu!
|
| _version_ | 1866915107589586944 |
|---|---|
| author | Beutner, Raven Finkbeiner, Bernd Göbl, Angelina |
| author_facet | Beutner, Raven Finkbeiner, Bernd Göbl, Angelina |
| contents | Hyperproperties relate multiple executions of a system and are commonly used to specify security and information-flow policies. While many verification approaches for hyperproperties exist, providing a convincing certificate that the system satisfies a given property is still a major challenge. In this paper, we propose strategies as a suitable form of certificate for hyperproperties specified in a fragment of the temporal logic HyperLTL. Concretely, we interpret the verification of a HyperLTL property as a game between universal and existential quantification, allowing us to leverage strategies for the existential quantifiers as certificates. We present HyGaViz, a browser-based visualization tool that lets users interactively explore an (automatically synthesized) witness strategy by taking control over universally quantified executions. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2501_10184 |
| institution | arXiv |
| publishDate | 2025 |
| record_format | arxiv |
| spellingShingle | Visualizing Game-Based Certificates for Hyperproperty Verification Beutner, Raven Finkbeiner, Bernd Göbl, Angelina Logic in Computer Science Hyperproperties relate multiple executions of a system and are commonly used to specify security and information-flow policies. While many verification approaches for hyperproperties exist, providing a convincing certificate that the system satisfies a given property is still a major challenge. In this paper, we propose strategies as a suitable form of certificate for hyperproperties specified in a fragment of the temporal logic HyperLTL. Concretely, we interpret the verification of a HyperLTL property as a game between universal and existential quantification, allowing us to leverage strategies for the existential quantifiers as certificates. We present HyGaViz, a browser-based visualization tool that lets users interactively explore an (automatically synthesized) witness strategy by taking control over universally quantified executions. |
| title | Visualizing Game-Based Certificates for Hyperproperty Verification |
| topic | Logic in Computer Science |
| url | https://arxiv.org/abs/2501.10184 |