85 citations · 262 across the 21 of their papers we have counts for
9 papers · 1 filter
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,…
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…
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…
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…
Parameterized Verification of Asynchronous Shared-Memory Systems
Javier Esparza, Pierre Ganty, Rupak Majumdar
We characterize the complexity of the safety verification problem for parameterized systems consisting of a leader process and arbitrarily many anonymous and identical contributors…
Proving Termination Starting from the End
Pierre Ganty, Samir Genaim
We present a novel technique for proving program termination which introduces a new dimension of modularity. Existing techniques use the program to incrementally construct a termin…
Algorithmic Verification of Asynchronous Programs
Pierre Ganty, Rupak Majumdar
Asynchronous programming is a ubiquitous systems programming idiom to manage concurrent interactions with the environment. In this style, instead of waiting for time-consuming oper…