Last update: December, 2024

Pierre Ganty

from 2019

I am an associate Research Professor at the IMDEA Software Institute doing research in the fields of verification, language theory and automata theory. You can find more about my research output on DBLP, Google Scholar, ORCID, and GitHub.

News

The language inclusion algorithm for Büchi automata introduced in our CAV’22 paper is part of Spot since version 2.12. Relevant details here.

Latest Work

Venue	Title
FSTTCS 2024	A Myhill-Nerode style Characterization for Timed Automata With Integer Resets ‣ arXiv report
RP 2024	Computing Reachable Simulations on Transition Systems
SPIN 2024	Learning the State Machine Behind a Modal Text Editor: The (Neo)Vim Case Study ‣ alternatively
Javier60	A Uniform Framework for Language Inclusion Problems ‣ arXiv report
TACAS 2023	Antichains Algorithms for the Inclusion Problem Between ω-VPL
CAV 2022	FORQ-based Language Inclusion Formal Testing ‣ arXiv report
Fundamenta Informaticæ	A Congruence-Based Perspective on Finite Tree Automata

Complete list (dblp)

Short Bio

Pierre joined the IMDEA Software Institute in September 2009 after completing a nearly two years postdoc at the UCLA. He holds a joint PhD degree in Computer Science from the Université Libre de Bruxelles and from the Università Degli Studi di Genova, Italy that he obtained late 2007.

Further details in my CV.

Research Interests

Algorithmic verification techniques: design, complexity study and implementation. Verification of software systems with infinitely many states: unbounded control and/or data. Algorithmic model based bug finding techniques. Abstract Interpretation. Automatic refinement of abstract domains. Automata theory and Formal Languages. Petri nets.

Team Members

Nicolas Manini (PhD student since October 2021)

Former Members

Chana Weil-Kennedy (Postdoc March 2023–October 2024)
Nicolas Amat (Postdoc December 2023–August 2024, shared with Alessio Mansutti)
Kyveli Doveri (PhD obtained in February 2024)
‣ Thesis: A Uniform Approach to Language Containment Problems, Alternate Link
Louis-Marie Dando (Postdoc October 2021–June 2023)
Nicolas Mazzocchi (Postdoc December 2020–December 2021)
Elena Gutiérrez (PhD obtained in September 2020)
‣ Thesis: New Perspectives on Classical Automata Constructions, Alternate Link
Pedro Valero (PhD obtained in July 2020)
‣ Thesis: On the Use of Quasiorders in Formal Language Theory, Alternate Link

Software

ωVPLInc: A ω-visibly pushdown language inclusion checker. Active.
forklift: A ω-regular language inclusion checker. Active. (forklift subsumes bait).
bait: Another ω-regular language inclusion checker. Active but subsumed by forklift.
zearch: zearch is a regular expression engine that takes in input a regular expression and a grammar-based compressed text and reports (by counting or printing) lines of the uncompressed text contain a match for the regular expression. Dormant.
HTTPValidator: An Input Validator for HTTP based on Context-free Languages. Dormant.
MIST: Algorithmic analyses of counter systems. Active.
Vanocka: Pattern-based verification of multithreaded programs. Algorithmic analysis of multithreaded programs that communicates through shared memory. It implements the pattern-based verification technique described in our POPL 2011 paper. Dormant.

Recent and Upcoming Service

CONCUR 2025, 36th International Conference on Concurrency Theory. (PC member)
RP 2025, 19th International Conference on Reachability Problems. (PC co-chair)
LICS 2024, 39th Annual ACM/IEEE Symposium on Logic in Computer Science. (PC member)
FoSSaCS 2024, 27th International Conference on Foundations of Software Science and Computation Structures. (PC member)
CONCUR 2023, 34th International Conference on Concurrency Theory. (PC member)
CAV 2023, 35th International Conference on Computer-Aided Verification. (PC member)

Contact

IMDEA Software Institute
Edificio IMDEA Software
Campus Montegancedo UPM
28223-Pozuelo de Alarcón, Madrid
Telephone: +34-91-101-2202 ext 4106