Paper Info
Title
Program Repair for Hyperproperties.
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.
Year
DOI
Venue
2019
10.1007/978-3-030-31784-3_25
ATVA
Field
DocType
Citations 
Kripke structure,Information flow (information theory),Determinism,Computer science,Theoretical computer science,Decidability,Temporal logic,Substructure,Computation
Conference
2
PageRank 
References 
Authors
0.36
0
2
Name
Order
Citations
PageRank
Borzoo Bonakdarpour149045.02
Bernd Finkbeiner266669.95