CISPA
Browse

Program Repair for Hyperproperties

Download (408.66 kB)
conference contribution
posted on 2023-11-29, 18:12 authored by Borzoo Bonakdarpour, Bernd FinkbeinerBernd Finkbeiner
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.

History

Preferred Citation

Borzoo Bonakdarpour and Bernd Finkbeiner. Program Repair for Hyperproperties. In: International Symposium on Automated Technology for Verification and Analysis (ATVA). 2019.

Primary Research Area

  • Reliable Security Guarantees

Name of Conference

International Symposium on Automated Technology for Verification and Analysis (ATVA)

Legacy Posted Date

2020-05-25

Open Access Type

  • Unknown

BibTeX

@inproceedings{cispa_all_3082, title = "Program Repair for Hyperproperties", author = "Bonakdarpour, Borzoo and Finkbeiner, Bernd", booktitle="{International Symposium on Automated Technology for Verification and Analysis (ATVA)}", year="2019", }

Usage metrics

    Categories

    No categories selected

    Exports

    RefWorks
    BibTeX
    Ref. manager
    Endnote
    DataCite
    NLM
    DC