Author name cluster

Andrzej Wąsowski

Possible papers associated with this exact author name in Arrow. This page groups case-insensitive exact name matches and is not a full identity disambiguation profile.

5 papers

1 author row

TCS Journal 2025 Journal Article

Compositional symbolic execution semantics

Erik Voogd
Åsmund Aqissiaq Arild Kløvstad
Einar Broch Johnsen
Andrzej Wąsowski

Symbolic execution is a program analysis technique to systematically explore all possible paths through a program. The technique can be formally explained by means of small-step transition systems that update symbolic states and compute a precondition corresponding to the taken execution path. In stateful transition systems behavior may depend on previous transitions, which complicates compositional reasoning about programs. To enable compositonal reasoning this paper defines a denotational semantics for symbolic execution. The proposed semantics views a program as a set of traces, each of which has a corresponding substitution — the composition of all its assignments — and a corresponding path condition — the conjunction of all its Boolean tests under appropriate substitution. We prove correspondence between the symbolic denotational semantics and a concrete semantics. We argue that the symbolic denotational semantics is a very natural framework to reason about symbolic execution, and use it to prove that symbolic execution computes (weakest) preconditions. We provide mechanizations in Coq for the main results.

Details DOI

TCS Journal 2015 Journal Article

Quantifying information leakage of randomized protocols

Fabrizio Biondi
Axel Legay
Pasquale Malacaria
Andrzej Wąsowski

The quantification of information leakage provides a quantitative evaluation of the security of a system. We propose the usage of Markovian processes to model deterministic and probabilistic systems. By using a methodology generalizing the lattice of information approach we model refined attackers capable to observe the internal behavior of the system, and quantify the information leakage of such systems. We also use our method to obtain an algorithm for the computation of channel capacity from our Markovian models. Finally, we show how to use the method to analyze timed and non-timed attacks on the Onion Routing protocol.

Details DOI

TCS Journal 2014 Journal Article

Robust synthesis for real-time systems

Kim G. Larsen
Axel Legay
Louis-Marie Traonouez
Andrzej Wąsowski

Specification theories for real-time systems allow reasoning about interfaces and their implementation models, using a set of operators that includes satisfaction, refinement, logical and parallel composition. To make such theories applicable throughout the entire design process from an abstract specification to an implementation, we need to reason about the possibility to effectively implement the theoretical specifications on physical systems, despite their limited precision. In the literature, this implementation problem has been linked to the robustness problem that analyzes the consequences of introducing small perturbations into formal models. We address this problem of robust implementations in timed specification theories. We first consider a fixed perturbation and study the robustness of timed specifications with respect to the operators of the theory. To this end we synthesize robust strategies in timed games. Finally, we consider the parametric robustness problem and propose a counter-example refinement heuristic for computing safe perturbation values.

Details DOI

I&C Journal 2013 Journal Article

Abstract Probabilistic Automata

Benoît Delahaye
Joost-Pieter Katoen
Kim G. Larsen
Axel Legay
Mikkel L. Pedersen
Falak Sher
Andrzej Wąsowski

Probabilistic Automata (PAs) are a widely-recognized mathematical framework for the specification and analysis of systems with non-deterministic and stochastic behaviors. This paper proposes Abstract Probabilistic Automata (APAs), that is a novel abstraction model for PAs. In APAs uncertainty of the non-deterministic choices is modeled by may/must modalities on transitions while uncertainty of the stochastic behavior is expressed by (underspecified) stochastic constraints. We have developed a complete abstraction theory for PAs, and also propose the first specification theory for them. Our theory supports both satisfaction and refinement operators, together with classical stepwise design operators. In addition, we study the link between specification theories and abstraction in avoiding the state-space explosion problem.

Details DOI

TCS Journal 2011 Journal Article

Constraint Markov Chains

Benoît Caillaud
Benoît Delahaye
Kim G. Larsen
Axel Legay
Mikkel L. Pedersen
Andrzej Wąsowski

Notions of specification, implementation, satisfaction, and refinement, together with operators supporting stepwise design, constitute a specification theory. We construct such a theory for Markov Chains (MCs) employing a new abstraction of a Constraint MC. Constraint MCs permit rich constraints on probability distributions and thus generalize prior abstractions such as Interval MCs. Linear (polynomial) constraints suffice for closure under conjunction (respectively parallel composition). This is the first specification theory for MCs with such closure properties. We discuss its relation to simpler operators for known languages such as probabilistic process algebra. Despite the generality, all operators and relations are computable.

Details DOI