HomeProjectsResearchToolsDocumentsPBM Viewero kama pona lon lipu miTyp2HTML
OverviewTalksPublicationsTree BorrowsPhD
2025
We consider the verification of parameterized networks of replicated processes whose architecture is described by hyperedge-replacement graph grammars. We present a counting abstraction able to produce, from a graph grammar describing a parameterized system, a finite set of Petri nets that over-approximate the behaviors of the original system. Moreover, we identify a decidable fragment, for which the coverability problem is in 2EXPTIME and PSPACE-hard.
CAV
(Zagreb)
Accepted
Counting Abstraction and Decidability for the Verification of Structured Parameterized Networks
with Arnaud Sangnier, Radu Iosif
The Rust programming language is well known for its ownership-based type system, which offers strong guarantees like memory safety and data race freedom. However, Rust also provides unsafe escape hatches, for which safety is not guaranteed automatically and must instead be manually upheld by the programmer. This creates a tension. On the one hand, compilers would like to exploit the strong guarantees of the type system in order to unlock powerful intraprocedural optimizations. On the other hand, those optimizations are easily invalidated by “badly behaved” unsafe code. To ensure correctness of such optimizations, it thus becomes necessary to clearly define what unsafe code is “badly behaved”. We present Tree Borrows, a set of rules improving on prior work to achieve this goal.
PLDI
(Seoul)
Accepted
Tree Borrows
with Derek Dreyer, Johannes Hostert, Ralf Jung
We consider the parametric reachability problem (PRP) for families of networks described by vertex-replacement (VR) graph grammars, where network nodes run replicas of finite-state processes that communicate via binary handshaking. We show that the PRP problem for VR grammars can be effectively reduced to the PRP problem for hyperedge-replacement (HR) grammars at the cost of introducing extra edges for routing messages.
NETYS
(Rabat)
Soon
Verifying Parameterized Networks Specified by Vertex Replacement Graph Grammars
with Marius Bozga, Arnaud Sangnier, Radu Iosif
2022
In this paper, we study the notion of mending, i.e. given a partial solution to a graph problem, we investigate how much effort is needed to turn it into a proper solution. For example, if we have a partial coloring of a graph, how hard is it to turn it into a proper coloring?
OPODIS
(Brussels)
Mending Partial Solutions with Few Changes
with Darya Melnyk, Jukka Suomela