2 citations · 4 across the 6 of their papers we have counts for
4 papers · 1 filter
Syntax-Guided Automated Program Repair for Hyperproperties
Raven Beutner, Tzu-Han Hsu, Borzoo Bonakdarpour +1
We study the problem of automatically repairing infinite-state software programs w.r.t. temporal hyperproperties. As a first step, we present a repair approach for the temporal log…
Bounded Model Checking for Asynchronous Hyperproperties
Tzu-Han Hsu, Borzoo Bonakdarpour, Bernd Finkbeiner +1
Many types of attacks on confidentiality stem from the nondeterministic nature of the environment that computer programs operate in (e.g., schedulers and asynchronous communication…
Efficient Loop Conditions for Bounded Model Checking Hyperproperties
Tzu-Han Hsu, César Sánchez, Sarai Sheinvald +1
Bounded model checking (BMC) is an effective technique for hunting bugs by incrementally exploring the state space of a system. To reason about infinite traces through a finite str…
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…