3 papers
cs.LO2026
Logics for Context-free Hyperproperties
Sarah Winter, Martin Zimmermann
We introduce a novel logic for the specification of context-free hyperproperties, which capture, e.g., the flow of information in security-critical recursive systems. Intuitively,…
cs.LO2025
Prophecies all the Way: Game-based Model-Checking for HyperQPTL beyond
Sarah Winter, Martin Zimmermann
Model-checking HyperLTL, a temporal logic expressing properties of sets of traces with applications to information-flow based security and privacy, has a decidable, but TOWER-compl…
cs.LO2024
Tracy, Traces, and Transducers: Computable Counterexamples and Explanations for HyperLTL Model-Checking
Sarah Winter, Martin Zimmermann
HyperLTL model-checking enables the automated verification of information-flow properties for security-critical systems. However, it only provides a binary answer. Here, we introdu…