Rewriting-Based Runtime Verification for Alternation-Free HyperLTL

DOI10.1007/978-3-662-54580-5_5zbMath1452.68114OpenAlexW2603022255MaRDI QIDQ3303921

Borzoo Bonakdarpour, Noel Brett, Umair Siddique

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

information flowsecurity policyBoolean expressionsecurity levelexecution trace

Mathematics Subject Classification ID

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

Related Items (9)

Gray-box monitoring of hyperproperties with an application to privacy ⋮ Monitorable hyperproperties of nonterminating systems ⋮ Unnamed Item ⋮ Program Repair for Hyperproperties ⋮ Monitoring hyperproperties ⋮ Finite-word hyperlanguages ⋮ Bounded model checking for hyperproperties ⋮ Synthesis from hyperproperties ⋮ Model checking hyperproperties for Markov decision processes

Uses Software

• JFlow
• TaintDroid

Cites Work

• Temporal Verification of Reactive Systems: Response
• Information flow inference for ML

This page was built for publication: Rewriting-Based Runtime Verification for Alternation-Free HyperLTL