Program Repair for Hyperproperties

DOI10.1007/978-3-030-31784-3_25MaRDI QIDQ3297603zbMATH OpenOpenAlexFDO

Authors Borzoo Bonakdarpour, Bernd Finkbeiner

Publication date 20 July 2020

Published in Automated Technology for Verification and Analysis (Search for Journal in Brave)

Full work available at URL https://arxiv.org/abs/2101.08257

Mathematics Subject Classification ID

Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Specification and verification (program logics, model checking, etc.) (68Q60) Temporal logic (03B44)

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.

Recommendations

• Toward a theory of program repair
• Automated program repair using formal verification techniques
• Runtime enforcement of hyperproperties
• Specification-based program repair using SAT
• Program repair without regret

Cites work

• scientific article; zbMATH DE number 3639144 (Why is no real title available?)
• scientific article; zbMATH DE number 6851935 (Why is no real title available?)
• Algorithms for model checking HyperLTL and HyperCTL^*
• Automated Technology for Verification and Analysis
• Computer Aided Verification
• Control problems in a temporal logic framework
• Counting quantifiers, successor relations, and logarithmic space
• HyperPCTL: A Temporal Logic for Probabilistic Hyperproperties
• Model checking quantitative hyperproperties
• Monitoring hyperproperties
• Rewriting-based runtime verification for alternation-free HyperLTL
• Supervisory Control of Discrete Event Systems with CTL* Temporal Logic Specifications
• Synthesis from hyperproperties
• The correlation between the complexities of the nonhierarchical and hierarchical versions of graph problems
• Verifying hyperliveness
• Weak Kripke structures and LTL

Cited in

(11)

• Model checking hyperproperties for Markov decision processes
• Assume, guarantee or repair
• Ensuring average recovery with adversarial scheduler
• Automatic addition of conflicting properties
• Bounded model checking for hyperproperties
• Parameter synthesis for probabilistic hyperproperties
• Explaining Hyperproperty Violations
• Runtime enforcement of hyperproperties
• Program repair without regret
• Computer Aided Verification
• Finite-word hyperlanguages

This page was built for publication: Program Repair for Hyperproperties

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3297603)