Pierre Ganty

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.

Latest Work

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

• patapsco: Presburger Arithmetic To Automata Prober of State COmplexity. Active.
• ω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

• CAV 2026, 38th International Conference on Computer Aided Verification. (PC member)
• FROM 2025, 9th Working Formal Methods Symposium. (PC member)
• SAS 2025, 32nd Static Analysis Symposium. (PC member)
• 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
pierre.ganty@imdea.org

Copyright © 2025 Pierre Ganty