43 citations · 119 across the 29 of their papers we have counts for
21 papers · 1 filter
Tractable Hyperproperties for MDPs
Lina Gerlach, Tobias Winkler, Erika Ábrahám +2
Probabilistic hyperproperties describe probabilistic relations between multiple sets of executions in a stochastic system. Prominent examples include information-theoretic characte…
Efficient Probabilistic Model Checking for Relational Reachability (Extended Version)
Lina Gerlach, Tobias Winkler, Erika Ábrahám +2
Markov decision processes model systems subject to nondeterministic and probabilistic uncertainty. A plethora of verification techniques addresses variations of reachability proper…
Efficient Discovery of Actual Causality using Abstraction-Refinement
Arshia Rafieioskouei, Borzoo Bonakdarpour
Causality is the relationship where one event contributes to the production of another, with the cause being partly responsible for the effect and the effect partly dependent on th…
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…
Approximate Distributed Monitoring under Partial Synchrony: Balancing Speed and Accuracy
Borzoo Bonakdarpour, Anik Momtaz, Dejan Ničković +1
In distributed systems with processes that do not share a global clock, \emph{partial synchrony} is achieved by clock synchronization that guarantees bounded clock skew among all a…
Decentralized Predicate Detection over Partially Synchronous Continuous-Time Signals
Charles Koll, Anik Momtaz, Borzoo Bonakdarpour +1
We present the first decentralized algorithm for detecting predicates over continuous-time signals under partial synchrony. A distributed cyber-physical system (CPS) consists of a…
Introducing Asynchronicity to Probabilistic Hyperproperties
Lina Gerlach, Oyendrila Dobe, Erika Ábrahám +2
Probabilistic hyperproperties express probabilistic relations between different executions of systems with uncertain behavior. HyperPCTL allows to formalize such properties, where…
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…
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…
Probabilistic Hyperproperties with Nondeterminism
Erika Abraham, Ezio Bartocci, Borzoo Bonakdarpour +1
We study the problem of formalizing and checking probabilistic hyperproperties for models that allow nondeterminism in actions. We extend the temporal logic \HyperPCTL, which has b…
Gray-box Monitoring of Hyperproperties (Extended Version)
Sandro Stucki, César Sánchez, Gerardo Schneider +1
Many important system properties, particularly in security and privacy, cannot be verified statically. Therefore, runtime verification is an appealing alternative. Logics for hyper…
Statistical Verification of Hyperproperties for Cyber-Physical System
Yu Wang, Mojtaba Zarei, Borzoo Bonakdarpour +1
Many important properties of cyber-physical systems (CPS) are defined upon the relationship between multiple executions simultaneously in continuous time. Examples include probabil…
Statistical Model Checking for Hyperproperties
Yu Wang, Siddhartha Nalluri, Borzoo Bonakdarpour +1
Hyperproperties have shown to be a powerful tool for expressing and reasoning about information-flow security policies. In this paper, we investigate the problem of statistical mod…
HyperPCTL: A Temporal Logic for Probabilistic Hyperproperties
Erika Abraham, Borzoo Bonakdarpour
In this paper, we propose a new logic for expressing and reasoning about probabilistic hyperproperties. Hyperproperties characterize the relation between different independent exec…
Abstract Model Repair
George Chatzieleftheriou, Borzoo Bonakdarpour, Panagiotis Katsaros +1
Given a Kripke structure M and CTL formula , where M does not satisfy , the problem of Model Repair is to obtain a new model M' such that M' satisfies . Moreover, the chan…
Accelerated Runtime Verification of LTL Specifications with Counting Semantics
Ramy Medhat, Yogi Joshi, Borzoo Bonakdarpour +1
Runtime verification is an effective automated method for specification-based offline testing and analysis as well as online monitoring of complex systems. The specification langua…