Alberto Pettorossi

ORCID

Publication Activity (10 Years)

Years Active: 1975-2024
Publications (10 Years): 44

Top Venues

CoRR

Fundam. Informaticae

Theory Pract. Log. Program.

LOPSTR

University of Edinburgh, UK (PHD)

Education History

University of Edinburgh, UK

PHD

Publications

Alberto Pettorossi, Maurizio Proietti, Fabio Fioravanti, Emanuele De Angelis
A Historical Perspective on Program Transformation and Recent Developments (Invited Contribution). PEPM (2024)
Emanuele De Angelis, Fabio Fioravanti, Alberto Pettorossi, Maurizio Proietti
Constrained Horn Clauses Satisfiability via Catamorphic Abstractions. LOPSTR (2023)
Emanuele De Angelis, Fabio Fioravanti, Alberto Pettorossi, Maurizio Proietti
Multiple Query Satisfiability of Constrained Horn Clauses. PADL (2023)
Emanuele De Angelis, Fabio Fioravanti, Alberto Pettorossi, Maurizio Proietti
Multiple Query Satisfiability of Constrained Horn Clauses. CoRR (2022)
Emanuele De Angelis, Fabio Fioravanti, Alberto Pettorossi, Maurizio Proietti
Contract Strengthening through Constrained Horn Clause Verification. HCVS/VPT@ETAPS (2022)
Emanuele De Angelis, Fabio Fioravanti, Alberto Pettorossi, Maurizio Proietti
Verifying Catamorphism-Based Contracts using Constrained Horn Clauses. CoRR (2022)
Emanuele De Angelis, Maurizio Proietti, Fabio Fioravanti, Alberto Pettorossi
Verifying Catamorphism-Based Contracts using Constrained Horn Clauses. Theory Pract. Log. Program. 22 (4) (2022)
Emanuele De Angelis, Fabio Fioravanti, John P. Gallagher, Manuel V. Hermenegildo, Alberto Pettorossi, Maurizio Proietti
Analysis and Transformation of Constrained Horn Clauses for Program Verification. Theory Pract. Log. Program. 22 (6) (2022)
Emanuele De Angelis, Fabio Fioravanti, Alberto Pettorossi, Maurizio Proietti
Satisfiability of constrained Horn clauses on algebraic data types: A transformation-based approach. J. Log. Comput. 32 (2) (2022)
Emanuele De Angelis, Fabio Fioravanti, John P. Gallagher, Manuel V. Hermenegildo, Alberto Pettorossi, Maurizio Proietti
Analysis and Transformation of Constrained Horn Clauses for Program Verification. CoRR (2021)
Emanuele De Angelis, Fabio Fioravanti, Alberto Pettorossi, Maurizio Proietti
Satisfiability of Constrained Horn Clauses on Algebraic Data Types: A Transformation-based Approach. CoRR (2021)
Emanuele De Angelis, Fabio Fioravanti, Alberto Pettorossi, Maurizio Proietti
Removing Algebraic Data Types from Constrained Horn Clauses Using Difference Predicates. IJCAR (1) (2020)
Alberto Pettorossi
A Historical Account of My Early Research Interests. VPT/HCVS@ETAPS (2020)
Manuel V. Hermenegildo, Pedro López-García, Alberto Pettorossi, Maurizio Proietti
Preface. Fundam. Informaticae 177 (3-4) (2020)
Emanuele De Angelis, Fabio Fioravanti, Alberto Pettorossi, Maurizio Proietti
Removing Algebraic Data Types from Constrained Horn Clauses Using Difference Predicates. CoRR (2020)
Emanuele De Angelis, Fabio Fioravanti, Adrián Palacios, Alberto Pettorossi, Maurizio Proietti
Property-Based Test Case Generators for Free. TAP@FM (2019)
Emanuele De Angelis, Fabio Fioravanti, Maria Chiara Meo, Alberto Pettorossi, Maurizio Proietti
Semantics and Controllability of Time-Aware Business Processes. Fundam. Informaticae 165 (3-4) (2019)
Emanuele De Angelis, Fabio Fioravanti, Alberto Pettorossi, Maurizio Proietti
Solving Horn Clauses on Inductive Data Types Without Induction - ERRATUM. Theory Pract. Log. Program. 19 (4) (2019)
Emanuele De Angelis, Fabio Fioravanti, Alberto Pettorossi, Maurizio Proietti
Lemma Generation for Horn Clause Satisfiability: A Preliminary Study. VPT@Programming (2019)
Emanuele De Angelis, Fabio Fioravanti, Alberto Pettorossi, Maurizio Proietti
Proving Properties of Sorting Programs: A Case Study in Horn Clause Verification. CILC (2019)
Emanuele De Angelis, Fabio Fioravanti, Alberto Pettorossi, Maurizio Proietti
Proving Properties of Sorting Programs: A Case Study in Horn Clause Verification. HCVS/PERR@ETAPS (2019)
Emanuele De Angelis, Fabio Fioravanti, Adrián Palacios, Alberto Pettorossi, Maurizio Proietti
Bounded Symbolic Execution for Runtime Error Detection of Erlang Programs. HCVS (2018)
Emanuele De Angelis, Fabio Fioravanti, Alberto Pettorossi, Maurizio Proietti
Predicate Pairing for program verification. Theory Pract. Log. Program. 18 (2) (2018)
Marco Maratea, Viviana Mascardi, Davide Ancona, Alberto Pettorossi
Preface. Fundam. Informaticae 159 (1-2) (2018)
Camillo Fiorentini, Alberto Momigliano, Alberto Pettorossi
Preface. Fundam. Informaticae 161 (1-2) (2018)
Emanuele De Angelis, Fabio Fioravanti, Alberto Pettorossi, Maurizio Proietti
Solving Horn Clauses on Inductive Data Types Without Induction. Theory Pract. Log. Program. 18 (3-4) (2018)
Emanuele De Angelis, Fabio Fioravanti, Alberto Pettorossi, Maurizio Proietti
Solving Horn Clauses on Inductive Data Types Without Induction. CoRR (2018)
Laura Giordano, Valentina Gliozzi, Alberto Pettorossi, Gian Luca Pozzato
Preface. Fundam. Informaticae 150 (1) (2017)
Emanuele De Angelis, Fabio Fioravanti, Maria Chiara Meo, Alberto Pettorossi, Maurizio Proietti
Verifying Controllability of Time-Aware Business Processes. RuleML+RR (2017)
Emanuele De Angelis, Fabio Fioravanti, Alberto Pettorossi, Maurizio Proietti
Enhancing Predicate Pairing with Abstraction for Relational Verification. CoRR (2017)
Emanuele De Angelis, Fabio Fioravanti, Alberto Pettorossi, Maurizio Proietti
Program Verification using Constraint Handling Rules and Array Constraint Generalizations. Fundam. Informaticae 150 (1) (2017)
Emanuele De Angelis, Fabio Fioravanti, Alberto Pettorossi, Maurizio Proietti
Predicate Pairing with Abstraction for Relational Verification. LOPSTR (2017)
Alberto Pettorossi, Maurizio Proietti
Regularity of non context-free languages over a singleton terminal alphabet. CoRR (2017)
Emanuele De Angelis, Fabio Fioravanti, Alberto Pettorossi, Maurizio Proietti
Predicate Pairing for Program Verification. CoRR (2017)
Emanuele De Angelis, Fabio Fioravanti, Alberto Pettorossi, Maurizio Proietti
Semantics-based generation of verification conditions via program specialization. Sci. Comput. Program. 147 (2017)
Emanuele De Angelis, Fabio Fioravanti, Alberto Pettorossi, Maurizio Proietti
Relational Verification Through Horn Clause Transformation. SAS (2016)
Emanuele De Angelis, Fabio Fioravanti, Alberto Pettorossi, Maurizio Proietti
Removing Unnecessary Variables from Horn Clause Verification Conditions. HCVS@ETAPS (2016)
Emanuele De Angelis, Fabio Fioravanti, Maria Chiara Meo, Alberto Pettorossi, Maurizio Proietti
Verification of Time-Aware Business Processes Using Constrained Horn Clauses. LOPSTR (2016)
Emanuele De Angelis, Fabio Fioravanti, Alberto Pettorossi, Maurizio Proietti
Verifying Relational Program Properties by Transforming Constrained Horn clauses. CILC (2016)
Emanuele De Angelis, Fabio Fioravanti, Maria Chiara Meo, Alberto Pettorossi, Maurizio Proietti
Verification of Time-Aware Business Processes using Constrained Horn Clauses. CoRR (2016)
Emanuele De Angelis, Fabio Fioravanti, Alberto Pettorossi, Maurizio Proietti
Proving correctness of imperative programs by linearizing constrained Horn clauses. Theory Pract. Log. Program. 15 (4-5) (2015)
Emanuele De Angelis, Fabio Fioravanti, Alberto Pettorossi, Maurizio Proietti
Semantics-based generation of verification conditions by program specialization. PPDP (2015)
Emanuele De Angelis, Fabio Fioravanti, Alberto Pettorossi, Maurizio Proietti
A Rule-based Verification Strategy for Array Manipulating Programs. Fundam. Informaticae 140 (3-4) (2015)
Emanuele De Angelis, Fabio Fioravanti, Alberto Pettorossi, Maurizio Proietti
Proving Correctness of Imperative Programs by Linearizing Constrained Horn Clauses. CoRR (2015)
Emanuele De Angelis, Fabio Fioravanti, Alberto Pettorossi, Maurizio Proietti
Program Verification using Constraint Handling Rules and Array Constraint Generalizations. CILC (2014)
Emanuele De Angelis, Fabio Fioravanti, Alberto Pettorossi, Maurizio Proietti
Program verification via iterated specialization. Sci. Comput. Program. 95 (2014)
Emanuele De Angelis, Fabio Fioravanti, Alberto Pettorossi, Maurizio Proietti
Verifying Array Programs by Transforming Verification Conditions. VMCAI (2014)
Emanuele De Angelis, Fabio Fioravanti, Alberto Pettorossi, Maurizio Proietti
VeriMAP: A Tool for Verifying Programs through Transformations. TACAS (2014)
Emanuele De Angelis, Fabio Fioravanti, Alberto Pettorossi, Maurizio Proietti
Program Verification using Constraint Handling Rules and Array Constraint Generalizations. VPT@CAV (2014)
Fabio Fioravanti, Alberto Pettorossi, Maurizio Proietti, Valerio Senni
Proving Theorems by Program Transformation. Fundam. Informaticae 127 (1-4) (2013)
Emanuele De Angelis, Fabio Fioravanti, Alberto Pettorossi, Maurizio Proietti
Verification of Imperative Programs by Constraint Logic Program Transformation. Festschrift for Dave Schmidt (2013)
Alberto Pettorossi, Maurizio Proietti
Program Transformation for Program Verification. VPT@CAV (2013)
Fabio Fioravanti, Alberto Pettorossi, Maurizio Proietti, Valerio Senni
Generalization strategies for the verification of infinite state systems. Theory Pract. Log. Program. 13 (2) (2013)
Emanuele De Angelis, Fabio Fioravanti, Alberto Pettorossi, Maurizio Proietti
Verification of Imperative Programs through Transformation of Constraint Logic Programs. VPT@CAV (2013)
Fabio Fioravanti, Alberto Pettorossi, Maurizio Proietti, Valerio Senni
Controlling Polyvariance for Specialization-based Verification. Fundam. Informaticae 124 (4) (2013)
Emanuele De Angelis, Fabio Fioravanti, Alberto Pettorossi, Maurizio Proietti
Verifying programs via iterated specialization. PEPM (2013)
Fabio Fioravanti, Alberto Pettorossi, Gianfranco Rossi
Preface. Fundam. Informaticae 124 (4) (2013)
Emanuele De Angelis, Fabio Fioravanti, Alberto Pettorossi, Maurizio Proietti
Verification of Imperative Programs by Transforming Constraint Logic Programs. CILC (2013)
Fabio Fioravanti, Alberto Pettorossi, Maurizio Proietti, Valerio Senni
Improving Reachability Analysis of Infinite State Systems by Specialization. Fundam. Informaticae 119 (3-4) (2012)
Emanuele De Angelis, Fabio Fioravanti, Maurizio Proietti, Alberto Pettorossi
Software Model Checking by Program Specialization. CILC (2012)
Emanuele De Angelis, Alberto Pettorossi, Maurizio Proietti
Synthesizing Concurrent Programs Using Answer Set Programming. Fundam. Informaticae 120 (3-4) (2012)
Emanuele De Angelis, Fabio Fioravanti, Alberto Pettorossi, Maurizio Proietti
Specialization with Constrained Generalization for Software Model Checking. LOPSTR (2012)
Alberto Pettorossi, Maurizio Proietti, Valerio Senni
Constraint-based correctness proofs for logic program transformations. Formal Aspects Comput. 24 (4-6) (2012)
Fabio Fioravanti, Alberto Pettorossi, Maurizio Proietti, Valerio Senni
Improving Reachability Analysis of Infinite State Systems by Specialization. RP (2011)
Fabio Fioravanti, Alberto Pettorossi, Maurizio Proietti, Valerio Senni
Program transformation for development, verification, and synthesis of programs. Intelligenza Artificiale 5 (1) (2011)
Fabio Fioravanti, Alberto Pettorossi, Maurizio Proietti, Valerio Senni
Generalization Strategies for the Verification of Infinite State Systems CoRR (2011)
Fabio Fioravanti, Alberto Pettorossi, Maurizio Proietti, Valerio Senni
Using Real Relaxations during Program Specialization. LOPSTR (2011)
Fabio Fioravanti, Alberto Pettorossi, Maurizio Proietti, Valerio Senni
Controlling Polyvariance for Specialization-based Verification. CILC (2011)
Marco Gavanelli, Toni Mancini, Alberto Pettorossi
RCRA 2009 Experimental Evaluation of Algorithms for Solving Problems with Combinatorial Explosion. Fundam. Informaticae 107 (2-3) (2011)
Emanuele De Angelis, Alberto Pettorossi, Maurizio Proietti
Synthesizing Concurrent Programs using Answer Set Programming. CILC (2011)
Alberto Pettorossi, Maurizio Proietti, Valerio Senni
Transformations of Logic Programs on Infinite Lists CoRR (2010)
Alberto Pettorossi, Valerio Senni, Maurizio Proietti
Transformations of logic programs on infinite lists. Theory Pract. Log. Program. 10 (4-6) (2010)
Fabio Fioravanti, Alberto Pettorossi, Maurizio Proietti, Valerio Senni
Program Specialization for Verifying Infinite State Systems: An Experimental Evaluation. LOPSTR (2010)
Marco Gavanelli, Fabrizio Riguzzi, Alberto Pettorossi
Preface. Fundam. Informaticae 105 (1-2) (2010)
Fabio Fioravanti, Alberto Pettorossi, Maurizio Proietti, Valerio Senni
Generalization Strategies for the Verification of Infinite State Systems. CILC (2010)
Alberto Pettorossi, Maurizio Proietti, Valerio Senni
A Transformation Strategy for Verifying Logic Programs on Infinite Lists. CILC (2010)
Valerio Senni, Alberto Pettorossi, Maurizio Proietti
A Folding Rule for Eliminating Existential Variables from Constraint Logic Programs. Fundam. Informaticae 96 (3) (2009)
Alberto Pettorossi, Maurizio Proietti, Valerio Senni
Deciding Full Branching Time Logic by Program Transformation. LOPSTR (2009)
Alberto Pettorossi, Maurizio Proietti
Totally correct logic program transformations via well-founded annotations. High. Order Symb. Comput. 21 (1-2) (2008)
Valerio Senni, Alberto Pettorossi, Maurizio Proietti
A Folding Algorithm for Eliminating Existential Variables from Constraint Logic Programs. ICLP (2008)
Alberto Pettorossi, Maurizio Proietti
Totally correct logic program transformations via well-founded annotations. High. Order Symb. Comput. 21 (1-2) (2008)
Alberto Pettorossi, Maurizio Proietti, Valerio Senni
Program Transformation for Development, Verification, and Synthesis of Software. Il Milione (2008)
Alberto Pettorossi, Maurizio Proietti, Valerio Senni
Automatic Correctness Proofs for Logic Program Transformations. ICLP (2007)
Alberto Pettorossi, Maurizio Proietti
Preface: Program Transformation: Theoretical Foundations and Basic Techniques. Part 2. Fundam. Informaticae 69 (1-2) (2006)
Alberto Pettorossi, Maurizio Proietti, Valerio Senni
Proving Properties of Constraint Logic Programs by Eliminating Existential Variables. ICLP (2006)
Alberto Pettorossi, Maurizio Proietti, Sophie Renault
Derivation of Efficient Logic Programs by Specialization and Reduction of Nondeterminism. High. Order Symb. Comput. 18 (1-2) (2005)
Alberto Pettorossi, Maurizio Proietti
Program Transformation: Theoretical Foundations and Basic Techniques. Part 1. Fundam. Informaticae 66 (4) (2005)
Olivier Danvy, Fritz Henglein, Harry G. Mairson, Alberto Pettorossi
Editorial. High. Order Symb. Comput. 18 (1-2) (2005)
Alberto Pettorossi, Maurizio Proietti, Valerio Senni
Transformational Verification of Parameterized Protocols Using Array Formulas. LOPSTR (2005)
Alberto Pettorossi, Maurizio Proietti, Valerio Senni
Proofs of Program Properties via Unfold/Fold Transformations of Constraint Logic Programs. Transformation Techniques in Software Engineering (2005)
Fabio Fioravanti, Alberto Pettorossi, Maurizio Proietti
Transformation Rules for Locally Stratified Constraint Logic Programs CoRR (2004)
Fabio Fioravanti, Alberto Pettorossi, Maurizio Proietti
Automatic Proofs of Protocols via Program Transformation. MSRAS (2004)
Alberto Pettorossi, Maurizio Proietti
A theory of totally correct logic program transformations. PEPM (2004)
Alberto Pettorossi, Maurizio Proietti
Transformations of logic programs with goals as arguments. Theory Pract. Log. Program. 4 (4) (2004)
Alberto Pettorossi, Maurizio Proietti
Transformations of Logic Programs with Goals as Arguments CoRR (2003)
Olivier Danvy, Fritz Henglein, Harry G. Mairson, Alberto Pettorossi
Editorial: Special Issue Dedicated to Bob Paige. High. Order Symb. Comput. 16 (1-2) (2003)
Alberto Pettorossi, Maurizio Proietti, Sophie Renault
Derivation of Efficient Logic Programs by Specialization and Reduction of Nondeterminism CoRR (2003)
Fabio Fioravanti, Alberto Pettorossi, Maurizio Proietti
Combining Logic Programs and Monadic Second Order Logics by Program Transformation CoRR (2003)
Fabio Fioravanti, Alberto Pettorossi, Maurizio Proietti
Combining Logic Programs and Monadic Second Order Logics by Program Transformation. LOPSTR (2002)
Alberto Pettorossi, Maurizio Proietti
Program Derivation = Rules + Strategies. Computational Logic: Logic Programming and Beyond (2002)

Alberto Pettorossi.css-eqlu8i{font-size:small;padding-left:4px;}

Publication Activity (10 Years)

Top Topics

Top Venues

Alberto Pettorossi