85 citations · 262 across the 21 of their papers we have counts for
31 papers
Temporal Hyperproperties for Population Protocols
Nicolas Waldburger, Chana Weil-Kennedy, Pierre Ganty +1
Hyperproperties are properties over sets of traces (or runs) of a system, as opposed to properties of just one trace. They were introduced in 2010 and have been much studied since,…
A Myhill-Nerode style Characterization for Timed Automata With Integer Resets
Kyveli Doveri, Pierre Ganty, B. Srivathsan
The well-known Nerode equivalence for finite words plays a fundamental role in our understanding of the class of regular languages. The equivalence leads to the Myhill-Nerode theor…
A Uniform Framework for Language Inclusion Problems
Kyveli Doveri, Pierre Ganty, Chana Weil-Kennedy
We present a uniform approach for solving language inclusion problems. Our approach relies on a least fixpoint characterization and a quasiorder to compare words of the "smaller" l…
Proceedings of the 13th International Symposium on Games, Automata, Logics and Formal Verification
Pierre Ganty, Dario Della Monica
This volume contains the proceedings of the 13th International Symposium on Games, Automata, Logic and Formal Verification (GandALF 2022). The aim of GandALF 2022 symposium is to b…
FORQ-based Language Inclusion Formal Testing
Kyveli Doveri, Pierre Ganty, Nicolas Mazzocchi
We propose a novel algorithm to decide the language inclusion between (nondeterministic) Büchi automata, a PSPACE-complete problem. Our approach, like others before, leverage a not…
Computing Reachable Simulations
Pierre Ganty, Nicolas Manini, Francesco Ranzato
We study the problem of computing the reachable principals of simulation preorder and the reachable blocks of simulation equivalence. Following a theoretical investigation of the d…
Proceedings 12th International Symposium on Games, Automata, Logics, and Formal Verification
Pierre Ganty, Davide Bresolin
This volume contains the proceedings of the 12th International Symposium on Games, Automata, Logic and Formal Verification (GandALF 2021). The aim of GandALF 2021 symposium is to b…
A Congruence-Based Perspective on Finite Tree Automata
Pierre Ganty, Elena Gutiérrez, Pedro Valero
We provide new insights on the determinization and minimization of tree automata using congruences on trees. From this perspective, we study a Brzozowski's style minimization algor…
A Quasiorder-based Perspective on Residual Automata
Pierre Ganty, Elena Gutiérrez, Pedro Valero
In this work, we define a framework of automata constructions based on quasiorders over words to provide new insights on the class of residual automata. We present a new residualiz…
CacheQuery: Learning Replacement Policies from Hardware Caches
Pepe Vila, Pierre Ganty, Marco Guarnieri +1
We show how to infer deterministic cache replacement policies using off-the-shelf automata learning and program synthesis techniques. For this, we construct and chain two abstracti…
A Congruence-based Perspective on Automata Minimization Algorithms
Pierre Ganty, Elena Gutiérrez, Pedro Valero
In this work we use a framework of finite-state automata constructions based on equivalences over words to provide new insights on the relation between well-known methods for compu…
Complete Abstractions for Checking Language Inclusion
Pierre Ganty, Francesco Ranzato, Pedro Valero
We study the language inclusion problem where is regular or context-free. Our approach relies on abstract interpretation and checks whether an overapproxi…
Regular Expression Search on Compressed Text
Pierre Ganty, Pedro Valero
We present an algorithm for searching regular expression matches in compressed text. The algorithm reports the number of matching lines in the uncompressed text in time linear in t…
The Parikh Property for Weighted Context-Free Grammars
Pierre Ganty, Elena Gutiérrez
Parikh's Theorem states that every context-free grammar (CFG) is equivalent to some regular CFG when the ordering of symbols in the words is ignored. The same is not true for the s…
Verification of Immediate Observation Population Protocols
Javier Esparza, Pierre Ganty, Rupak Majumdar +1
Population protocols (Angluin et al., PODC, 2004) are a formal model of sensor networks consisting of identical mobile devices. Two devices can interact and thereby change their st…
Sound up-to techniques and Complete abstract domains
Filippo Bonchi, Pierre Ganty, Roberto Giacobazzi +1
Abstract interpretation is a method to automatically find invariants of programs or pieces of code whose semantics is given via least fixed-points. Up-to techniques have been intro…
Tree dimension in verification of constrained Horn clauses
Bishoksan Kafle, John P. Gallagher, Pierre Ganty
In this paper, we show how the notion of tree dimension can be used in the verification of constrained Horn clauses (CHCs). The dimension of a tree is a numerical measure of its br…
Parikh Image of Pushdown Automata
Pierre Ganty, Elena Gutiérrez
We compare pushdown automata (PDAs for short) against other representations. First, we show that there is a family of PDAs over a unary alphabet with states and …
A Language-theoretic View on Network Protocols
Pierre Ganty, Boris Köpf, Pedro Valero
Input validation is the first line of defense against malformed or malicious inputs. It is therefore critical that the validator (which is often part of the parser) is free of bugs…
Bounded-oscillation Pushdown Automata
Pierre Ganty, Damir Valput
We present an underapproximation for context-free languages by filtering out runs of the underlying pushdown automaton depending on how the stack height evolves over time. In parti…
Solving non-linear Horn clauses using a linear Horn clause solver
Bishoksan Kafle, John P. Gallagher, Pierre Ganty
In this paper we show that checking satisfiability of a set of non-linear Horn clauses (also called a non-linear Horn clause program) can be achieved using a solver for linear Horn…
Decomposition by tree dimension in Horn clause verification
Bishoksan Kafle, John P. Gallagher, Pierre Ganty
In this paper we investigate the use of the concept of tree dimension in Horn clause analysis and verification. The dimension of a tree is a measure of its non-linearity - for exam…
Model Checking Parameterized Asynchronous Shared-Memory Systems
Antoine Durand-Gasselin, Javier Esparza, Pierre Ganty +1
We characterize the complexity of liveness verification for parameterized systems consisting of a leader process and arbitrarily many anonymous and identical contributor processes.…
Interprocedural Reachability for Flat Integer Programs
Pierre Ganty, Radu Iosif
We study programs with integer data, procedure calls and arbitrary call graphs. We show that, whenever the guards and updates are given by octagonal relations, the reachability pro…