Search Results

System administrators, network engineers, and IT managers can learn much about the vulnerabilities of an organization’s cyber system by constructing and analyzing analytical attack graphs (AAGs). An AAG consists of logical rule nodes, fact nodes, ...

Android apps typically include many functionalities that not all users require. These result in software bloat that increases possible attack surface and app size. Common functionalities that users may not require are related to permissions that they ...

The size of Android applications is getting larger to fulfill the requirements of various users. However, not all the features of the applications are needed and desired by a specific user. The unnecessary and non-desired features can increase the attack ...

Non-well-separation (NWS) is a known quality issue in specifications for reactive synthesis. The problem of NWS occurs when the synthesized system can avoid satisfying its guarantees by preventing the environment from being able to satisfy its ...

Android applications are getting bigger with an increasing number of features. However, not all the features are needed by a specific user. The unnecessary features can increase the attack surface and cost additional resources (e.g., storage and memory). ...

Temporal specifications are essential inputs for verification and synthesis. Despite their importance, temporal specifications are challenging to write, which might limit their use by software engineers. To this day, almost no quality attributes of ...

Reactive synthesis is an automated procedure to obtain a correct-by-construction reactive system from its temporal logic specification. Despite its attractiveness and major research progress in the past decades, reactive synthesis is still in early-...

Reactive synthesis is an automated procedure to obtain a correct-by-construction reactive system from its temporal logic specification. Two of the main challenges in bringing reactive synthesis to practice are its very high worst-case complexity and ...

Specifications for reactive systems synthesis consist of assumptions and guarantees. However, some specifications may include unnecessary assumptions, i.e., assumptions that are not necessary for realizability. While the controllers that are ...

Reactive synthesis is an automated procedure to obtain a correct-by-construction reactive system from its temporal logic specification. While the synthesized system is guaranteed to be correct w.r.t. the specification, the specification itself may be ...

Reactive synthesis is an automated procedure to obtain a correct-by-construction reactive system from its temporal logic specification. GR(1) is an expressive fragment of LTL that enables efficient synthesis and has been recently used in different ...

$\omega$-regular energy games are two-player $\omega$-regular games augmented with a requirement to avoid the exhaustion of a finite resource, e.g., battery or disk space. $\omega$-regular energy games can be reduced to $\omega$-regular games by encoding the energy level ...$$$$$$$$$$

We introduce Spectra, a new specification language for reactive systems, specifically tailored for the context of reactive synthesis. The meaning of Spectra is defined by a translation to a kernel language. Spectra comes with the Spectra Tools, a ...

Reactive synthesis is an automated procedure to obtain a correct-by-construction reactive system from its temporal logic specification. GR(1) is an expressive assume-guarantee fragment of LTL that enables efficient synthesis and has been recently ...

Spectra is a formal specification language specifically tailored for use in the context of reactive synthesis, an automated procedure to obtain a correct-by-construction reactive system from its temporal logic specification. Spectra comes with the ...

This document describes the artifact that accompanies the ICSE'21 paper "Unrealizable Cores for Reactive Systems Specifications". The artifact includes the specifications that were used in the experiments that are described in the paper. It further ...

One of the main challenges of reactive synthesis, an automated procedure to obtain a correct-by-construction reactive system, is to deal with unrealizable specifications. One means to deal with unrealizability, in the context of GR(1), an expressive ...

Reactive synthesis is an automated procedure to obtain a correct-by-construction reactive system from its temporal logic specification. GR(1) is an expressive assume-guarantee fragment of LTL that enables efficient synthesis and has been recently used in ...

Vacuity is a well-known quality issue in formal specifications, studied mostly in the context of model checking. Inherent vacuity is a type of vacuity that applies to specifications, without the context of a model. GR(1) is an expressive assume-...

Many works infer finite-state models from execution logs. Large models are more accurate but also more difficult to present and understand. Small models are easier to present and understand but are less accurate.

In this work we investigate the tradeoff ...