IMDEA initiative

Home > People

Pierre Ganty

PhD - Université Libre de Bruxelles, Belgium

Associate Research Professor

Pierre Ganty IMDEA Software Institute
Edificio IMDEA Software
Campus Montegancedo UPM
28223-Pozuelo de Alarcón, Madrid

Office: 356
Telephone: +34-91-101-2202 ext 4106
Fax: +34-91-101-1358

ACM DL Author-ize serviceAlgorithmic verification of asynchronous programs with Rupak Majumdar. ACM Transactions on Programming Languages and Systems (TOPLAS). See also the arxiv report.
  • Bounded Underapproximations with Benjamin Monmege and Rupak Majumdar. Invitation to FMSD CAV 2010 Special Issue. See also the arxiv report.
  • Approximating Petri Net Reachability Along Context-free Traces with Mohamed-Faouzi Atig. FSTTCS 2011. See also the arXiv report.
  • Complexity Analysis of the Backward Coverability Algorithm for VASS with Laura Bozzelli. RP 2011.
  • Parikh's Theorem: A Simple and Direct Automaton Construction with Javier Esparza, Stefan Kiefer and Michael Luttenberger. IPL.
  • Short bio

    Pierre joined the IMDEA Software Institute Institute in September 2009 after completing a nearly two years postdoc at the University of California at Los Angeles, USA. He holds a joint PhD degree in Computer Science from the Université Libre de Bruxelles, Belgium and from the Universitá Degli Studi di Genova, Italy that he obtained late 2007.
    Further details in my CV. [15-Dec-2012]

    Research Interests (no order)

    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.


    Here is a PDF file of my publications (papers can be downloaded from the file). [15-Dec-2012]

    Collaborating with me

    If you are interested in an internship or PhD at the IMDEA Software Institute Institute that closely relate to my research interests, send me an email and fill in the appropriate forms available from the Open Positions entry in the left menu.


    • MIST: Algorithmic analyses of counter systems.
    • 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 POPL'11. (Main contributor: Tomáš Poch)
    • ABP2NTS: A translator from asynchronous boolean programs to Petri Nets expressed in the NTS language. (Main contributor: Bishesh Adhikari). Available on request.


    • ATVA 2014, 12th International Symposium on Automated Technology for Verification and Analysis. (PC member)
    • ICALP 2014, 41st International Colloquium on Automata, Languages and Programming. (PC member)
    • RP 2013, 7th International workshop on Reachability Problems. (PC member)
    • VMCAI 2013, 14th International Symposium on Verification, Model Checking and Abstract Interpretation. (PC member)
    • Infinity 2012, 14th International Workshop on Verification of Infinite-State Systems. (PC member)
    • Bytecode 2011, 6th Workshop on Bytecode Semantics, Verification, Analysis and Transformation (PC co-chair)
    • APNOC 2010, 2nd Workshop on Abstractions for Petri Nets and Other Models of Concurrency. (PC member)

    Updated: $Date: 2013-03-06 22:13:10 +0100 (Wed, 06 Mar 2013) $
    Copyright © 2013 Pierre Ganty