| 2026 | DLT | Closure Operations on Picture Languages and Their Relation to Floor Plans. | Stefano Crespi-Reghizzi, Antonio Restivo, Pierluigi San Pietro |
| 2026 | FORTE | Tarzan: A Region-Based Library for Forward and Backward Reachability of Timed Automata. | Andrea Manini, Matteo G. Rossi, Pierluigi San Pietro |
| 2026 | TASE | Timed Games Under Environmental Interference with Real-Time Objectives. | Andrea Manini, Matteo G. Rossi, Pierluigi San Pietro |
| 2025 | TASE | Random Testing of Model Checkers for Timed Automata with Automated Oracle Generation. | Andrea Manini, Matteo G. Rossi, Pierluigi San Pietro |
| 2024 | SOFSEM | Row-Column Combination of Dyck Words. | Stefano Crespi-Reghizzi, Antonio Restivo, Pierluigi San Pietro |
| 2021 | DLT | Reducing Local Alphabet Size in Recognizable Picture Languages. | Stefano Crespi-Reghizzi, Antonio Restivo, Pierluigi San Pietro |
| 2021 | ICSE | Improved Bounded Model Checking of Timed Automata. | Robert L. Smith, Marcello M. Bersani, Matteo Rossi, Pierluigi San Pietro |
| 2021 | LATA | Homomorphic Characterization of Tree Languages Based on Comma-Free Encoding. | Stefano Crespi-Reghizzi, Pierluigi San Pietro |
| 2018 | DLT | Deque Languages, Automata and Planar Graphs. | Stefano Crespi-Reghizzi, Pierluigi San Pietro |
| 2016 | ICSE | Efficient large-scale trace checking using mapreduce. | Marcello M. Bersani, Domenico Bianculli, Carlo Ghezzi, Srdan Krstic, Pierluigi San Pietro |
| 2016 | LATA | The Missing Case in Chomsky-Schtzenberger Theorem. | Stefano Crespi-Reghizzi, Pierluigi San Pietro |
| 2014 | FASE | SMT-Based Checking of SOLOIST over Sparse Traces. | Marcello Maria Bersani, Domenico Bianculli, Carlo Ghezzi, Srdan Krstic, Pierluigi San Pietro |
| 2014 | MFCS | A Logical Characterization of Timed (non-)Regular Languages. | Marcello M. Bersani, Matteo Rossi, Pierluigi San Pietro |
| 2013 | TIME | A Tool for Deciding the Satisfiability of Continuous-Time Metric Temporal Logic. | Marcello M. Bersani, Matteo Rossi, Pierluigi San Pietro |
| 2010 | TIME | Bounded Reachability for Temporal Logic over Constraint Systems. | Marcello M. Bersani, Achille Frigeri, Angelo Morzenti, Matteo Pradella, Matteo Rossi, Pierluigi San Pietro |
| 2009 | FM | A Metric Encoding for Bounded Model Checking. | Matteo Pradella, Angelo Morzenti, Pierluigi San Pietro |
| 2008 | ICA3PP | Finding Synchronization-Free Parallelism Represented with Trees of Dependent Operations. | Wlodzimierz Bielecki, Anna Beletska, Marek Palkowski, Pierluigi San Pietro |
| 2008 | ICCSA | Finding Synchronization-Free Slices of Operations in Arbitrarily Nested Loops. | Anna Beletska, Wlodzimierz Bielecki, Krzysztof Siedlecki, Pierluigi San Pietro |
| 2008 | ICTAC | Benchmarking Model- and Satisfiability-Checking on Bi-infinite Time. | Matteo Pradella, Angelo Morzenti, Pierluigi San Pietro |
| 2008 | LATA | Consensual Definition of Languages by Regular Sets. | Stefano Crespi-Reghizzi, Pierluigi San Pietro |
| 2007 | ICSE | Trio2Promela: A Model Checker for Temporal Metric Specifications. | Domenico Bianculli, Angelo Morzenti, Matteo Pradella, Pierluigi San Pietro, Paola Spoletini |
| 2007 | ISPDC | Extracting Coarse-Grained Parallelism in Program Loops with the Slicing Framework. | Anna Beletska, Wlodzimierz Bielecki, Pierluigi San Pietro |
| 2003 | CAV | Dense Counter Machines and Verification Problems. | Gaoyan Xie, Zhe Dang, Oscar H. Ibarra, Pierluigi San Pietro |
| 2003 | COCOON | Automatic Verification of Multi-queue Discrete Timed Automata. | Pierluigi San Pietro, Zhe Dang |
| 2003 | FM | Model-Checking TRIO Specifications in SPIN. | Angelo Morzenti, Matteo Pradella, Pierluigi San Pietro, Paola Spoletini |
| 2002 | SMC | Software procurement and methods for specification and validation in the railway transportation industry. | Umberto Foschi, Mauro Giuliani, Angelo Morzenti, Matteo Pradella, Pierluigi San Pietro |
| 2001 | CC | Alias Analysis by Means of a Model Checker. | Vincenzo Martena, Pierluigi San Pietro |
| 2001 | ICSE | A Scalable Formal Method for Design and Automatic Checking of User Interfaces. | Jean Berstel, Stefano Crespi-Reghizzi, Gilles Roussel, Pierluigi San Pietro |
| 2001 | STACS | On Presburger Liveness of Discrete Timed Automata. | Zhe Dang, Pierluigi San Pietro, Richard A. Kemmerer |
| 1996 | ISSTA | Generating Functional Test Cases in-the-large for Time-critical Systems from Logic-based Specifications. | Sandro Morasca, Angelo Morzenti, Pierluigi San Pietro |
| 1993 | ER | Reuse of Object-Oriented Requirements Specifications. | Silvana Castano, Valeria De Antonellis, Pierluigi San Pietro |
| 1991 | ECOOP | An Object-Oriented Logic Language for Modular System Specification. | Angelo Morzenti, Pierluigi San Pietro |