On subrecursiveness in weak combinatory logic. - Carlo Batini; Alberto Pettorossi (Lambda-Calculus and Computer Science Theory, 1975)

Improving Memory Utilization in Transforming Recursive Programs (Extended Abstract). - Alberto Pettorossi (MFCS, 1978)

On the definition of hierarchies of infinite sequential computations. - Alberto Pettorossi (FCT, 1979)

Synthesis of subtree rewriting systems behaviour by solving equations. - Alberto Pettorossi (CLAAP, 1980)

Towards a theory of parallelism and communications for increasing efficiency in applicative languages. - Alberto Pettorossi (Logic of Programs, 1980)

Derivation of an O(k² log n) Algorithm for Computing Order-k Fibonacci Numbers From the O(k³ log n) Matrix Multiplication Method. - Alberto Pettorossi (Inf. Process. Lett., 1980)

A transformational approach for developing parallel programs. - Alberto Pettorossi (CONPAR, 1981)

Comparing and Putting Together Recursive Path Ordering, Simplification Orderings and Non-Ascending Property for Termination Proofs of Term Rewriting Systems. - Alberto Pettorossi (ICALP, 1981)

An Approach to Communications and Parallelism in Applicative Languages. - Alberto Pettorossi (ICFPC, 1981)

A property which guarantees termination in weak combinatory logic and subtree replacement systems. - Alberto Pettorossi (Notre Dame J. Formal Log., 1981)

Communicating agents for applicative concurrent programming. - Alberto Pettorossi; Andrzej Skowron (Symposium on Programming, 1982)

Deriving very Efficient Algorithms for Evaluating Linear Recurrence Relations Using the Program Transformation Technique. - Alberto Pettorossi; Rod M. Burstall (Acta Informatica, 1982)

A Powerful Strategy for Deriving Efficient Programs by Transformation. - Alberto Pettorossi (LISP and Functional Programming, 1984)

A methodology for improving parallel programs by adding communications. - Alberto Pettorossi; Andrzej Skowron (Symposium on Computation Theory, 1984)

Higher-order communications for concurrent programming. - Alberto Pettorossi; Andrzej Skowron (Parallel Comput., 1984)

Methodologies for transformations and memoing in applicative languages. - Alberto Pettorossi (1984)

Categorical Models of Process Cooperation. - Anna Labella; Alberto Pettorossi (CTCS, 1985)

Towers of Hanoi Problems: Deriving Iterative Solutions by Program Transformations. - Alberto Pettorossi (BIT, 1985)

A Note on Cohen's "Eliminating Redundant Recursive Calls". - Alberto Pettorossi (ACM Trans. Program. Lang. Syst., 1985)

Factual Knowledge For Developing Concurrent Programs. - Andrzej Skowron; Alberto Pettorossi (AAAI, 1986)

Universal Models in Categories for Process Synchronization. - Anna Labella; Alberto Pettorossi (Mathematical Models for the Semantics of Parallelism, 1986)

Transformation Strategies for Deriving On Line Programs. - Alberto Pettorossi (CAAP, 1986)

Using Facts for Improving the Parallel Execution of Functional Programs. - Alberto Pettorossi; Andrzej Skowron (ICPP, 1986)

Enriched Categories for Local and Interaction Calculi. - Stefano Kasangian; Anna Labella; Alberto Pettorossi (Category Theory and Computer Science, 1987)

Program Development Using Lambda Abstraction. - Alberto Pettorossi (FSTTCS, 1987)

On Learning with Imperfect Teachers. - Alberto Pettorossi; Zbigniew W. Ras; Maria Zemankova (ISMIS, 1987)

Higher Order Generalization in Program Derivation. - Alberto Pettorossi; Andrzej Skowron (TAPSOFT, Vol.2, 1987)

Derivation of Efficient Programs for Computing Sequences of Actions. - Alberto Pettorossi (Theor. Comput. Sci., 1987)

Decidability Results and Characterization of Strategies for the Development of Logic Programs. - Alberto Pettorossi; Maurizio Proietti (ICLP, 1989)

The Power of the Lambda Abstraction Strategy for Program Derivation. - Alberto Pettorossi; Andrzej Skowron (J. Inf. Process. Cybern., 1989)

Synthesis of Eureka Predicates for Developing Logic Programs. - Maurizio Proietti; Alberto Pettorossi (ESOP, 1990)

Observers, Experiments and Agents: a Comprehensive Approach to Parallelism. - Stefano Kasangian; Anna Labella; Alberto Pettorossi (Semantics of Systems of Concurrent Processes, 1990)

An Automatic Transfomation Strategy for Avoiding Unnecessary Variables in Logic Programs (Extended Abstract). - Maurizio Proietti; Alberto Pettorossi (LOPSTR, 1991)

Semantics Preserving Transformation Rules for Prolog. - Maurizio Proietti; Alberto Pettorossi (PEPM, 1991)

Best-first Strategies for Incremental Transformations of Logic Programs. - Maurizio Proietti; Alberto Pettorossi (LOPSTR, 1992)

Completeness of some Transformation Strategies for Avoiding Unncecessary Logical Variables. - Maurizio Proietti; Alberto Pettorossi (GULP, 1993)

Rules and Strategies for Program Transformation. - Alberto Pettorossi; Maurizio Proietti (Formal Program Development, 1993)

Synthesis of Programs from Unfold/Fold Proofs. - Maurizio Proietti; Alberto Pettorossi (LOPSTR, 1993)

An Abstract Strategy for Transforming Logic Programs. - Maurizio Proietti; Alberto Pettorossi (Fundam. Informaticae, 1993)

The Loop Absorption and the Generalization Strategies for the Development of Logic Programs and Partial Deduction. - Maurizio Proietti; Alberto Pettorossi (J. Log. Program., 1993)

Total correctness of a goal replacement rule based on the unfold/fold proof method. - Maurizio Proietti; Alberto Pettorossi (GULP-PRODE (1), 1994)

Completeness of Some Transformation Strategies for Avoiding Unnecessary Logical Variables. - Maurizio Proietti; Alberto Pettorossi (ICLP, 1994)

Transformation of Logic Programs: Foundations and Techniques. - Alberto Pettorossi; Maurizio Proietti (J. Log. Program., 1994)

Correctness of Logic Program Transformations Based on Existential Termination. - Kung-Kiu Lau; Mario Ornaghi; Alberto Pettorossi; Maurizio Proietti (ILPS, 1995)

Unfolding - Definition - Folding, in this Order, for Avaoiding Unnecessary Variables in Logic Programs. - Maurizio Proietti; Alberto Pettorossi (Theor. Comput. Sci., 1995)

A Comparative Revisitation of Some Program Transformation Techniques. - Alberto Pettorossi; Maurizio Proietti (Dagstuhl Seminar on Partial Evaluation, 1996)

A Theory of Logic Program Specialization and Generalization for Dealing with Input Data Properties. - Alberto Pettorossi; Maurizio Proietti (Dagstuhl Seminar on Partial Evaluation, 1996)

How to Extend Partial Deduction to Derive the KMP String-Matching Algorithm from a Naive Specification (Poster Abstract). - Alberto Pettorossi; Maurizio Proietti; Sophie Renault (JICSLP, 1996)

Enhancing Partial Deduction via Unfold/Fold Rules. - Alberto Pettorossi; Maurizio Proietti; Sophie Renault (LOPSTR, 1996)

Rules and Strategies for Transforming Functional and Logic Programs. - Alberto Pettorossi; Maurizio Proietti (ACM Comput. Surv., 1996)

Future Directions in Program Transformation. - Alberto Pettorossi; Maurizio Proietti (ACM Comput. Surv., 1996)

Developing correct and efficient logic programs by transformation. - Alberto Pettorossi; Maurizio Proietti (Knowl. Eng. Rev., 1996)

Program derivation via list introduction. - Alberto Pettorossi; Maurizio Proietti (Algorithmic Languages and Calculi, 1997)

Reducing Nondeterminism while Specializing Logic Programs. - Alberto Pettorossi; Maurizio Proietti; Sophie Renault (POPL, 1997)

Program Specialization via Algorithmic Unfold/Fold Transformations. - Alberto Pettorossi; Maurizio Proietti (ACM Comput. Surv., 1998)

Transforming Inductive Definitions. - Maurizio Proietti; Alberto Pettorossi (ICLP, 1999)

Transformation Rules for Logic Programs with Goals as Arguments. - Alberto Pettorossi; Maurizio Proietti (LOPSTR, 1999)

Synthesis and Transformation of Logic Programs Using Unfold/Fold Proofs. - Alberto Pettorossi; Maurizio Proietti (J. Log. Program., 1999)

Rules and Strategies for Contextual Specialization of Constraint Logic Programs. - Fabio Fioravanti; Alberto Pettorossi; Maurizio Proietti (WOID@ICLP, 1999)

Perfect Model Checking via Unfold/Fold Transformations. - Alberto Pettorossi; Maurizio Proietti (Computational Logic, 2000)

Automated strategies for specializing constraint logic programs. - Fabio Fioravanti; Alberto Pettorossi; Maurizio Proietti (LOPSTR, 2000)

Verification of Sets of Infinite State Processes Using Program Transformation. - Fabio Fioravanti; Alberto Pettorossi; Maurizio Proietti (LOPSTR, 2001)

Specialization with Clause Splitting for Deriving Deterministic Constraint Logic Programs. - Fabio Fioravanti; Alberto Pettorossi; Maurizio Proietti (APPIA-GULP-PRODE, 2002)

Program Derivation = Rules + Strategies. - Alberto Pettorossi; Maurizio Proietti (Computational Logic: Logic Programming and Beyond, 2002)

Combining Logic Programs and Monadic Second Order Logics by Program Transformation. - Fabio Fioravanti; Alberto Pettorossi; Maurizio Proietti (LOPSTR, 2002)

The List Introduction Strategy for the Derivation of Logic Programs. - Alberto Pettorossi; Maurizio Proietti (Formal Aspects Comput., 2002)

Editorial: Special Issue Dedicated to Bob Paige. - Olivier Danvy; Fritz Henglein; Harry G. Mairson; Alberto Pettorossi (High. Order Symb. Comput., 2003)

Transformation Rules for Locally Stratified Constraint Logic Programs. - Fabio Fioravanti; Alberto Pettorossi; Maurizio Proietti (Program Development in Computational Logic, 2004)

Automatic Proofs of Protocols via Program Transformation. - Fabio Fioravanti; Alberto Pettorossi; Maurizio Proietti (MSRAS, 2004)

A theory of totally correct logic program transformations. - Alberto Pettorossi; Maurizio Proietti (PEPM, 2004)

Transformation Rules for Locally Stratified Constraint Logic Programs - Fabio Fioravanti; Alberto Pettorossi; Maurizio Proietti (CoRR, 2004)

Transformations of logic programs with goals as arguments. - Alberto Pettorossi; Maurizio Proietti (Theory Pract. Log. Program., 2004)

Proofs of Program Properties via Unfold/Fold Transformations of Constraint Logic Programs. - Alberto Pettorossi; Maurizio Proietti; Valerio Senni (Transformation Techniques in Software Engineering, 2005)

Transformational Verification of Parameterized Protocols Using Array Formulas. - Alberto Pettorossi; Maurizio Proietti; Valerio Senni (LOPSTR, 2005)

Program Transformation: Theoretical Foundations and Basic Techniques. Part 1. - Alberto Pettorossi; Maurizio Proietti (Fundam. Informaticae, 2005)

Editorial. - Olivier Danvy; Fritz Henglein; Harry G. Mairson; Alberto Pettorossi (High. Order Symb. Comput., 2005)

Derivation of Efficient Logic Programs by Specialization and Reduction of Nondeterminism. - Alberto Pettorossi; Maurizio Proietti; Sophie Renault (High. Order Symb. Comput., 2005)

Proving Properties of Constraint Logic Programs by Eliminating Existential Variables. - Alberto Pettorossi; Maurizio Proietti; Valerio Senni (ICLP, 2006)

Preface: Program Transformation: Theoretical Foundations and Basic Techniques. Part 2. - Alberto Pettorossi; Maurizio Proietti (Fundam. Informaticae, 2006)

Automatic Correctness Proofs for Logic Program Transformations. - Alberto Pettorossi; Maurizio Proietti; Valerio Senni (ICLP, 2007)

Program Transformation for Development, Verification, and Synthesis of Software. - Alberto Pettorossi; Maurizio Proietti; Valerio Senni (Il Milione, 2008)

A Folding Algorithm for Eliminating Existential Variables from Constraint Logic Programs. - Valerio Senni; Alberto Pettorossi; Maurizio Proietti (ICLP, 2008)

Totally correct logic program transformations via well-founded annotations. - Alberto Pettorossi; Maurizio Proietti (High. Order Symb. Comput., 2008)

Deciding Full Branching Time Logic by Program Transformation. - Alberto Pettorossi; Maurizio Proietti; Valerio Senni (LOPSTR, 2009)

A Folding Rule for Eliminating Existential Variables from Constraint Logic Programs. - Valerio Senni; Alberto Pettorossi; Maurizio Proietti (Fundam. Informaticae, 2009)

The Transformational Approach to Program Development. - Alberto Pettorossi; Maurizio Proietti; Valerio Senni (25 Years GULP, 2010)

A Transformation Strategy for Verifying Logic Programs on Infinite Lists. - Alberto Pettorossi; Maurizio Proietti; Valerio Senni (CILC, 2010)

Program Specialization for Verifying Infinite State Systems: An Experimental Evaluation. - Fabio Fioravanti; Alberto Pettorossi; Maurizio Proietti; Valerio Senni (LOPSTR, 2010)

Preface. - Marco Gavanelli; Fabrizio Riguzzi; Alberto Pettorossi (Fundam. Informaticae, 2010)

Transformations of logic programs on infinite lists. - Alberto Pettorossi; Valerio Senni; Maurizio Proietti (Theory Pract. Log. Program., 2010)

Using Real Relaxations during Program Specialization. - Fabio Fioravanti; Alberto Pettorossi; Maurizio Proietti; Valerio Senni (LOPSTR, 2011)

RCRA 2009 Experimental Evaluation of Algorithms for Solving Problems with Combinatorial Explosion. - Marco Gavanelli; Toni Mancini; Alberto Pettorossi (Fundam. Informaticae, 2011)

Program transformation for development, verification, and synthesis of programs. - Fabio Fioravanti; Alberto Pettorossi; Maurizio Proietti; Valerio Senni (Intelligenza Artificiale, 2011)

Software Model Checking by Program Specialization. - Emanuele De Angelis; Fabio Fioravanti; Maurizio Proietti; Alberto Pettorossi (CILC, 2012)

Specialization with Constrained Generalization for Software Model Checking. - Emanuele De Angelis; Fabio Fioravanti; Alberto Pettorossi; Maurizio Proietti (LOPSTR, 2012)

Constraint-based correctness proofs for logic program transformations. - Alberto Pettorossi; Maurizio Proietti; Valerio Senni (Formal Aspects Comput., 2012)

Synthesizing Concurrent Programs Using Answer Set Programming. - Emanuele De Angelis; Alberto Pettorossi; Maurizio Proietti (Fundam. Informaticae, 2012)

Improving Reachability Analysis of Infinite State Systems by Specialization. - Fabio Fioravanti; Alberto Pettorossi; Maurizio Proietti; Valerio Senni (Fundam. Informaticae, 2012)

Verification of Imperative Programs through Transformation of Constraint Logic Programs. - Emanuele De Angelis; Fabio Fioravanti; Alberto Pettorossi; Maurizio Proietti (VPT@CAV, 2013)

Program Transformation for Program Verification. - Alberto Pettorossi; Maurizio Proietti (VPT@CAV, 2013)

Verification of Imperative Programs by Transforming Constraint Logic Programs. - Emanuele De Angelis; Fabio Fioravanti; Alberto Pettorossi; Maurizio Proietti (CILC, 2013)

Verifying programs via iterated specialization. - Emanuele De Angelis; Fabio Fioravanti; Alberto Pettorossi; Maurizio Proietti (PEPM, 2013)

Verification of Imperative Programs by Constraint Logic Program Transformation. - Emanuele De Angelis; Fabio Fioravanti; Alberto Pettorossi; Maurizio Proietti (Festschrift for Dave Schmidt, 2013)

Controlling Polyvariance for Specialization-based Verification. - Fabio Fioravanti; Alberto Pettorossi; Maurizio Proietti; Valerio Senni (Fundam. Informaticae, 2013)

Proving Theorems by Program Transformation. - Fabio Fioravanti; Alberto Pettorossi; Maurizio Proietti; Valerio Senni (Fundam. Informaticae, 2013)

Preface. - Fabio Fioravanti; Alberto Pettorossi; Gianfranco Rossi (Fundam. Informaticae, 2013)

Generalization strategies for the verification of infinite state systems. - Fabio Fioravanti; Alberto Pettorossi; Maurizio Proietti; Valerio Senni (Theory Pract. Log. Program., 2013)

VeriMAP: A Tool for Verifying Programs through Transformations. - Emanuele De Angelis; Fabio Fioravanti; Alberto Pettorossi; Maurizio Proietti (TACAS, 2014)

Verifying Array Programs by Transforming Verification Conditions. - Emanuele De Angelis; Fabio Fioravanti; Alberto Pettorossi; Maurizio Proietti (VMCAI, 2014)

Program verification via iterated specialization. - Emanuele De Angelis; Fabio Fioravanti; Alberto Pettorossi; Maurizio Proietti (Sci. Comput. Program., 2014)

Semantics-based generation of verification conditions by program specialization. - Emanuele De Angelis; Fabio Fioravanti; Alberto Pettorossi; Maurizio Proietti (PPDP, 2015)

A Rule-based Verification Strategy for Array Manipulating Programs. - Emanuele De Angelis; Fabio Fioravanti; Alberto Pettorossi; Maurizio Proietti (Fundam. Informaticae, 2015)

Proving correctness of imperative programs by linearizing constrained Horn clauses. - Emanuele De Angelis; Fabio Fioravanti; Alberto Pettorossi; Maurizio Proietti (Theory Pract. Log. Program., 2015)

Verifying Relational Program Properties by Transforming Constrained Horn clauses. - Emanuele De Angelis; Fabio Fioravanti; Alberto Pettorossi; Maurizio Proietti (CILC, 2016)

Verification of Time-Aware Business Processes Using Constrained Horn Clauses. - Emanuele De Angelis; Fabio Fioravanti; Maria Chiara Meo; Alberto Pettorossi; Maurizio Proietti (LOPSTR, 2016)

Relational Verification Through Horn Clause Transformation. - Emanuele De Angelis; Fabio Fioravanti; Alberto Pettorossi; Maurizio Proietti (SAS, 2016)

Removing Unnecessary Variables from Horn Clause Verification Conditions. - Emanuele De Angelis; Fabio Fioravanti; Alberto Pettorossi; Maurizio Proietti (HCVS@ETAPS, 2016)

Predicate Pairing with Abstraction for Relational Verification. - Emanuele De Angelis; Fabio Fioravanti; Alberto Pettorossi; Maurizio Proietti (LOPSTR, 2017)

Verifying Controllability of Time-Aware Business Processes. - Emanuele De Angelis; Fabio Fioravanti; Maria Chiara Meo; Alberto Pettorossi; Maurizio Proietti (RuleML+RR, 2017)

Regularity of non context-free languages over a singleton terminal alphabet. - Alberto Pettorossi; Maurizio Proietti (CoRR, 2017)

Enhancing Predicate Pairing with Abstraction for Relational Verification. - Emanuele De Angelis; Fabio Fioravanti; Alberto Pettorossi; Maurizio Proietti (CoRR, 2017)

Program Verification using Constraint Handling Rules and Array Constraint Generalizations. - Emanuele De Angelis; Fabio Fioravanti; Alberto Pettorossi; Maurizio Proietti (Fundam. Informaticae, 2017)

Preface. - Laura Giordano 001; Valentina Gliozzi; Alberto Pettorossi; Gian Luca Pozzato (Fundam. Informaticae, 2017)

Semantics-based generation of verification conditions via program specialization. - Emanuele De Angelis; Fabio Fioravanti; Alberto Pettorossi; Maurizio Proietti (Sci. Comput. Program., 2017)

Bounded Symbolic Execution for Runtime Error Detection of Erlang Programs. - Emanuele De Angelis; Fabio Fioravanti; Adrián Palacios; Alberto Pettorossi; Maurizio Proietti (HCVS, 2018)

Preface. - Camillo Fiorentini; Alberto Momigliano; Alberto Pettorossi (Fundam. Informaticae, 2018)

Preface. - Marco Maratea; Viviana Mascardi; Davide Ancona; Alberto Pettorossi (Fundam. Informaticae, 2018)

Predicate Pairing for program verification. - Emanuele De Angelis; Fabio Fioravanti; Alberto Pettorossi; Maurizio Proietti (Theory Pract. Log. Program., 2018)

Solving Horn Clauses on Inductive Data Types Without Induction. - Emanuele De Angelis; Fabio Fioravanti; Alberto Pettorossi; Maurizio Proietti (Theory Pract. Log. Program., 2018)

Property-Based Test Case Generators for Free. - Emanuele De Angelis; Fabio Fioravanti; Adrián Palacios; Alberto Pettorossi; Maurizio Proietti (TAP@FM, 2019)

Proving Properties of Sorting Programs: A Case Study in Horn Clause Verification. - Emanuele De Angelis; Fabio Fioravanti; Alberto Pettorossi; Maurizio Proietti (HCVS/PERR@ETAPS, 2019)

Lemma Generation for Horn Clause Satisfiability: A Preliminary Study. - Emanuele De Angelis; Fabio Fioravanti; Alberto Pettorossi; Maurizio Proietti (VPT@Programming, 2019)

Semantics and Controllability of Time-Aware Business Processes. - Emanuele De Angelis; Fabio Fioravanti; Maria Chiara Meo; Alberto Pettorossi; Maurizio Proietti (Fundam. Informaticae, 2019)

Solving Horn Clauses on Inductive Data Types Without Induction - ERRATUM. - Emanuele De Angelis; Fabio Fioravanti; Alberto Pettorossi; Maurizio Proietti (Theory Pract. Log. Program., 2019)

Removing Algebraic Data Types from Constrained Horn Clauses Using Difference Predicates. - Emanuele De Angelis; Fabio Fioravanti; Alberto Pettorossi; Maurizio Proietti (IJCAR (1), 2020)

A Historical Account of My Early Research Interests. - Alberto Pettorossi (VPT/HCVS@ETAPS, 2020)

Preface. - Manuel V. Hermenegildo; Pedro López-García 001; Alberto Pettorossi; Maurizio Proietti (Fundam. Informaticae, 2020)

Techniques for Searching, Parsing, and Matching - Alberto Pettorossi (Springer, 2021)

Contract Strengthening through Constrained Horn Clause Verification. - Emanuele De Angelis; Fabio Fioravanti; Alberto Pettorossi; Maurizio Proietti (HCVS/VPT@ETAPS, 2022)

Satisfiability of constrained Horn clauses on algebraic data types: A transformation-based approach. - Emanuele De Angelis; Fabio Fioravanti; Alberto Pettorossi; Maurizio Proietti (J. Log. Comput., 2022)

Analysis and Transformation of Constrained Horn Clauses for Program Verification. - Emanuele De Angelis; Fabio Fioravanti; John P. Gallagher; Manuel V. Hermenegildo; Alberto Pettorossi; Maurizio Proietti (Theory Pract. Log. Program., 2022)

Verifying Catamorphism-Based Contracts using Constrained Horn Clauses. - Emanuele De Angelis; Maurizio Proietti; Fabio Fioravanti; Alberto Pettorossi (Theory Pract. Log. Program., 2022)

Constrained Horn Clauses Satisfiability via Catamorphic Abstractions. - Emanuele De Angelis; Fabio Fioravanti; Alberto Pettorossi; Maurizio Proietti (LOPSTR, 2023)

Multiple Query Satisfiability of Constrained Horn Clauses. - Emanuele De Angelis; Fabio Fioravanti; Alberto Pettorossi; Maurizio Proietti (PADL, 2023)

A Historical Perspective on Program Transformation and Recent Developments (Invited Contribution). - Alberto Pettorossi; Maurizio Proietti; Fabio Fioravanti; Emanuele De Angelis (PEPM, 2024)

Catamorphic Abstractions for Constrained Horn Clause Satisfiability. - Emanuele De Angelis; Fabio Fioravanti; Alberto Pettorossi; Maurizio Proietti (Theory Pract. Log. Program., 2025)