43 citations · 119 across the 29 of their papers we have counts for
5 papers · 1 filter
HyperQB: A Bounded Model Checker for Hyperproperties
Tzu-Han Hsu, Milad Rabizadeh, Kenneth Rogale +4
We introduce the tool HyperQB 2.0, the first highly efficient push-button bounded model checker (BMC) for hyperproperties. HyperQB takes as input a model in NuSMV or Verilog and a…
A Temporal Logic for Asynchronous Hyperproperties
Jan Baumeister, Norine Coenen, Borzoo Bonakdarpour +2
Hyperproperties are properties of computational systems that require more than one trace to evaluate, e.g., many information-flow security and concurrency requirements. Where a tra…
Controller Synthesis for Hyperproperties
Borzoo Bonakdarpour, Bernd Finkbeiner
We investigate the problem of controller synthesis for hyperproperties specified in the temporal logic HyperLTL. Hyperproperties are system properties that relate multiple executio…
Program Repair for Hyperproperties
Borzoo Bonakdarpour, Bernd Finkbeiner
We study the repair problem for hyperproperties specified in the temporal logic HyperLTL. Hyperproperties are system properties that relate multiple computation traces. This class…
The Complexity of Monitoring Hyperproperties
Borzoo Bonakdarpour, Bernd Finkbeiner
We study the runtime verification of hyperproperties, expressed in the temporal logic HyperLTL, as a means to inspect a system with respect to security polices. Runtime monitors fo…