Gray-box monitoring of hyperproperties with an application to privacy

DOI10.1007/S10703-020-00358-WzbMATH Open1502.68187OpenAlexW3126303719MaRDI QIDQ2147690FDOQ2147690

Gerardo Schneider, Sandro Stucki, Borzoo Bonakdarpour, César Sánchez

Publication date: 20 June 2022

Published in: Formal Methods in System Design (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/s10703-020-00358-w

zbMATH Keywords

securityruntime verificationprivacyLTLmonitorabilitydata minimizationhyperLTLhyperproperty

Mathematics Subject Classification ID

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

Cites Work

• A brief account of runtime verification
• Symbolic execution and program testing
• A survey of challenges for runtime verification from advanced application domains (beyond software)
• Rewriting-Based Runtime Verification for Alternation-Free HyperLTL

Cited In (2)

• Efficient loop conditions for bounded model checking hyperproperties
• Monitorable hyperproperties of nonterminating systems

Uses Software

• JML
• z3
• KeY
• GitHub

This page was built for publication: Gray-box monitoring of hyperproperties with an application to privacy

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