Skip to main content

Lightweight Verification of Hyperproperties

Publication Type
Year of Publication
Conference/Journal Name
The 21th International Symposium on Automated Technology for Verification and Analysis (ATVA)
Page Numbers
Hyperproperties have been widely used to express system properties like noninterference, observational determinism, conformance, robustness, etc. However, the model checking problem for hyperproperties is challenging due to its inherent complexity of verifying properties across sets of traces and suffers from scalability issues. Previously, statistical approaches have proven effective in tackling the scalability of model checking for temporal logic. In this work, we have attempted to combine these two concepts to propose a tractable solution to model checking of hyperproperties expressed as HyperLTL on models involving nondeterminism. We have implemented our approach in \tool{PLASMA} and experimented with a range of case studies to showcase its effectiveness.