Rewriting-based runtime verification for alternation-free HyperLTL

DOI10.1007/978-3-662-54580-5_5MaRDI QIDQ3303921zbMATH OpenOpenAlexFDO

Authors Noel Brett, Umair Siddique, Borzoo Bonakdarpour

Publication date 5 August 2020

Published in Tools and Algorithms for the Construction and Analysis of Systems (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-662-54580-5_5

zbMATH Keywords

Boolean expressionexecution traceinformation flowsecurity levelsecurity policy

Mathematics Subject Classification ID

Temporal logic (03B44) Specification and verification (program logics, model checking, etc.) (68Q60)

Recommendations

• Monitoring hyperproperties
• Runtime enforcement of hyperproperties
• Temporal hyperproperties
• Algorithms for model checking HyperLTL and HyperCTL^*
• Model checking algorithms for hyperproperties (invited paper)

Cites work

• Information flow inference for ML
• Temporal verification of reactive systems: response

Cited in

(18)

• Monitoring hyperproperties
• Bounded model checking for hyperproperties
• Model checking hyperproperties for Markov decision processes
• Gray-box monitoring of hyperproperties with an application to privacy
• Monitorable hyperproperties of nonterminating systems
• Synthesis from hyperproperties
• Program Repair for Hyperproperties
• Conformance relations and hyperproperties for doping detection in time and space
• Constraint-based monitoring of hyperproperties
• Finite-word hyperlanguages
• Runtime Verification: Passing on the Baton
• Opportunistic monitoring of multithreaded programs
• Efficient loop conditions for bounded model checking hyperproperties
• Gray-box monitoring of hyperproperties
• Centralized vs decentralized monitors for hyperproperties
• Centralized vs. decentralized monitors for hyperproperties
• Parameter synthesis for probabilistic hyperproperties
• HyperLTL satisfiability is highly undecidable, \(\mathrm{HyperCTL}^*\) is even harder

Describes a project that uses

Uses Software

• JFlow
• TaintDroid

This page was built for publication: Rewriting-based runtime verification for alternation-free HyperLTL

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