(2019) Program Repair for Hyperproperties.
In: Automated Technology for Verification and Analysis - 17th International Symposium, ATVA 2019, Taipei, Taiwan, October 28-31, 2019, Proceedings.
Conference:
ATVA International Symposium on Automated Technology for Verification and Analysis
|
Text
BF19.pdf Download (418kB) | Preview |
Official URL: https://doi.org/10.1007/978-3-030-31784-3\_25
Abstract
We study the repair problem for hyperproperties specified in the temporal logic HyperLTL. Hyperproperties are system properties that relate multiple computation traces. This class of properties includes information flow policies like noninterference and observational determinism. The repair problem is to find, for a given Kripke structure, a substructure that satisfies a given specification. We show that the repair problem is decidable for HyperLTL specifications and finite-state Kripke structures. We provide a detailed complexity analysis for different fragments of HyperLTL and different system types: tree-shaped, acyclic, and general Kripke structures.
| Item Type: | Conference or Workshop Item (A Paper) (Paper) |
|---|---|
| Conference: | ATVA International Symposium on Automated Technology for Verification and Analysis |
| Depositing User: | Bernd Finkbeiner |
| Date Deposited: | 25 May 2020 11:40 |
| Last Modified: | 11 May 2021 13:55 |
| Primary Research Area: | NRA2: Reliable Security Guarantees |
| URI: | https://publications.cispa.saarland/id/eprint/3082 |
Actions
Actions (login required)
 |
View Item |