| 2024 | PEPM | A Historical Perspective on Program Transformation and Recent Developments (Invited Contribution). | Alberto Pettorossi, Maurizio Proietti, Fabio Fioravanti, Emanuele De Angelis |
| 2023 | LOPSTR | Constrained Horn Clauses Satisfiability via Catamorphic Abstractions. | Emanuele De Angelis, Fabio Fioravanti, Alberto Pettorossi, Maurizio Proietti |
| 2023 | PADL | Multiple Query Satisfiability of Constrained Horn Clauses. | Emanuele De Angelis, Fabio Fioravanti, Alberto Pettorossi, Maurizio Proietti |
| 2020 | CADE | Removing Algebraic Data Types from Constrained Horn Clauses Using Difference Predicates. | Emanuele De Angelis, Fabio Fioravanti, Alberto Pettorossi, Maurizio Proietti |
| 2019 | TAP | Property-Based Test Case Generators for Free. | Emanuele De Angelis, Fabio Fioravanti, Adrin Palacios, Alberto Pettorossi, Maurizio Proietti |
| 2017 | LOPSTR | Predicate Pairing with Abstraction for Relational Verification. | Emanuele De Angelis, Fabio Fioravanti, Alberto Pettorossi, Maurizio Proietti |
| 2016 | LOPSTR | Verification of Time-Aware Business Processes Using Constrained Horn Clauses. | Emanuele De Angelis, Fabio Fioravanti, Maria Chiara Meo, Alberto Pettorossi, Maurizio Proietti |
| 2016 | SAS | Relational Verification Through Horn Clause Transformation. | Emanuele De Angelis, Fabio Fioravanti, Alberto Pettorossi, Maurizio Proietti |
| 2015 | PPDP | Semantics-based generation of verification conditions by program specialization. | Emanuele De Angelis, Fabio Fioravanti, Alberto Pettorossi, Maurizio Proietti |
| 2014 | CAV | Program Verification using Constraint Handling Rules and Array Constraint Generalizations. | Emanuele De Angelis, Fabio Fioravanti, Alberto Pettorossi, Maurizio Proietti |
| 2014 | TACAS | VeriMAP: A Tool for Verifying Programs through Transformations. | Emanuele De Angelis, Fabio Fioravanti, Alberto Pettorossi, Maurizio Proietti |
| 2014 | VMCAI | Verifying Array Programs by Transforming Verification Conditions. | Emanuele De Angelis, Fabio Fioravanti, Alberto Pettorossi, Maurizio Proietti |
| 2013 | CAV | Verification of Imperative Programs through Transformation of Constraint Logic Programs. | Emanuele De Angelis, Fabio Fioravanti, Alberto Pettorossi, Maurizio Proietti |
| 2013 | CAV | Program Transformation for Program Verification. | Alberto Pettorossi, Maurizio Proietti |
| 2013 | PEPM | Verifying programs via iterated specialization. | Emanuele De Angelis, Fabio Fioravanti, Alberto Pettorossi, Maurizio Proietti |
| 2012 | LOPSTR | Specialization with Constrained Generalization for Software Model Checking. | Emanuele De Angelis, Fabio Fioravanti, Alberto Pettorossi, Maurizio Proietti |
| 2011 | LOPSTR | Using Real Relaxations during Program Specialization. | Fabio Fioravanti, Alberto Pettorossi, Maurizio Proietti, Valerio Senni |
| 2010 | LOPSTR | Program Specialization for Verifying Infinite State Systems: An Experimental Evaluation. | Fabio Fioravanti, Alberto Pettorossi, Maurizio Proietti, Valerio Senni |
| 2009 | LOPSTR | Deciding Full Branching Time Logic by Program Transformation. | Alberto Pettorossi, Maurizio Proietti, Valerio Senni |
| 2008 | ICLP | A Folding Algorithm for Eliminating Existential Variables from Constraint Logic Programs. | Valerio Senni, Alberto Pettorossi, Maurizio Proietti |
| 2007 | ICLP | Automatic Correctness Proofs for Logic Program Transformations. | Alberto Pettorossi, Maurizio Proietti, Valerio Senni |
| 2006 | ICLP | Proving Properties of Constraint Logic Programs by Eliminating Existential Variables. | Alberto Pettorossi, Maurizio Proietti, Valerio Senni |
| 2005 | LOPSTR | Transformational Verification of Parameterized Protocols Using Array Formulas. | Alberto Pettorossi, Maurizio Proietti, Valerio Senni |
| 2004 | PEPM | A theory of totally correct logic program transformations. | Alberto Pettorossi, Maurizio Proietti |
| 2002 | LOPSTR | Combining Logic Programs and Monadic Second Order Logics by Program Transformation. | Fabio Fioravanti, Alberto Pettorossi, Maurizio Proietti |
| 2001 | LOPSTR | Verification of Sets of Infinite State Processes Using Program Transformation. | Fabio Fioravanti, Alberto Pettorossi, Maurizio Proietti |
| 2000 | LOPSTR | Automated strategies for specializing constraint logic programs. | Fabio Fioravanti, Alberto Pettorossi, Maurizio Proietti |
| 2000 | LOPSTR | Automated Strategies for Specializing Constraint Logic Programs. | Fabio Fioravanti, Alberto Pettorossi, Maurizio Proietti |
| 1999 | ICLP | Transforming Inductive Definitions. | Maurizio Proietti, Alberto Pettorossi |
| 1999 | LOPSTR | Transformation Rules for Logic Programs with Goals as Arguments. | Alberto Pettorossi, Maurizio Proietti |
| 1997 | POPL | Reducing Nondeterminism while Specializing Logic Programs. | Alberto Pettorossi, Maurizio Proietti, Sophie Renault |
| 1996 | ICLP | How to Extend Partial Deduction to Derive the KMP String-Matching Algorithm from a Naive Specification (Poster Abstract). | Alberto Pettorossi, Maurizio Proietti, Sophie Renault |
| 1996 | LOPSTR | Enhancing Partial Deduction via Unfold/Fold Rules. | Alberto Pettorossi, Maurizio Proietti, Sophie Renault |
| 1994 | ICLP | Completeness of Some Transformation Strategies for Avoiding Unnecessary Logical Variables. | Maurizio Proietti, Alberto Pettorossi |
| 1993 | LOPSTR | Synthesis of Programs from Unfold/Fold Proofs. | Maurizio Proietti, Alberto Pettorossi |
| 1992 | LOPSTR | Best-first Strategies for Incremental Transformations of Logic Programs. | Maurizio Proietti, Alberto Pettorossi |
| 1991 | LOPSTR | An Automatic Transfomation Strategy for Avoiding Unnecessary Variables in Logic Programs (Extended Abstract). | Maurizio Proietti, Alberto Pettorossi |
| 1991 | PEPM | Semantics Preserving Transformation Rules for Prolog. | Maurizio Proietti, Alberto Pettorossi |
| 1990 | ESOP | Synthesis of Eureka Predicates for Developing Logic Programs. | Maurizio Proietti, Alberto Pettorossi |
| 1989 | ICLP | Decidability Results and Characterization of Strategies for the Development of Logic Programs. | Alberto Pettorossi, Maurizio Proietti |
| 1987 | ISMIS | On Learning with Imperfect Teachers. | Alberto Pettorossi, Zbigniew W. Ras, Maria Zemankova |
| 1986 | AAAI | Factual Knowledge For Developing Concurrent Programs. | Andrzej Skowron, Alberto Pettorossi |
| 1986 | ICPP | Using Facts for Improving the Parallel Execution of Functional Programs. | Alberto Pettorossi, Andrzej Skowron |
| 1981 | ICALP | Comparing and Putting Together Recursive Path Ordering, Simplification Orderings and Non-Ascending Property for Termination Proofs of Term Rewriting Systems. | Alberto Pettorossi |
| 1979 | FCT | On the definition of hierarchies of infinite sequential computations. | Alberto Pettorossi |
| 1978 | MFCS | Improving Memory Utilization in Transforming Recursive Programs (Extended Abstract). | Alberto Pettorossi |