Alberto Pettorossi

Springer, ISBN: 978-3-030-63188-8, 2021

2020

Preface.

[BibT_eX]

[DOI]

Manuel V. Hermenegildo

Pedro López-García

Fundam. Informaticae, 2020

A Historical Account of My Early Research Interests.

[BibT_eX]

[DOI]

Proceedings of the Proceedings 8th International Workshop on Verification and Program Transformation and 7th Workshop on Horn Clauses for Verification and Synthesis, 2020

Removing Algebraic Data Types from Constrained Horn Clauses Using Difference Predicates.

[BibT_eX]

[DOI]

Proceedings of the Automated Reasoning - 10th International Joint Conference, 2020

2019

Solving Horn Clauses on Inductive Data Types Without Induction - ERRATUM.

[BibT_eX]

[DOI]

Theory Pract. Log. Program., 2019

Semantics and Controllability of Time-Aware Business Processes.

[BibT_eX]

[DOI]

Fundam. Informaticae, 2019

Lemma Generation for Horn Clause Satisfiability: A Preliminary Study.

[BibT_eX]

[DOI]

Proceedings of the Proceedings Seventh International Workshop on Verification and Program Transformation, 2019

Proving Properties of Sorting Programs: A Case Study in Horn Clause Verification.

[BibT_eX]

[DOI]

Proceedings of the Sixth Workshop on Horn Clauses for Verification and Synthesis and Third Workshop on Program Equivalence and Relational Reasoning, 2019

Property-Based Test Case Generators for Free.

[BibT_eX]

[DOI]

Proceedings of the Tests and Proofs - 13th International Conference, 2019

2018

Solving Horn Clauses on Inductive Data Types Without Induction.

[BibT_eX]

[DOI]

Theory Pract. Log. Program., 2018

Predicate Pairing for program verification.

[BibT_eX]

[DOI]

Theory Pract. Log. Program., 2018

Preface.

[BibT_eX]

[DOI]

Fundam. Informaticae, 2018

Preface.

[BibT_eX]

[DOI]

Camillo Fiorentini

Alberto Momigliano

Fundam. Informaticae, 2018

Bounded Symbolic Execution for Runtime Error Detection of Erlang Programs.

[BibT_eX]

[DOI]

Proceedings of the Proceedings 5th Workshop on Horn Clauses for Verification and Synthesis, 2018

2017

Semantics-based generation of verification conditions via program specialization.

[BibT_eX]

[DOI]

Sci. Comput. Program., 2017

Preface.

[BibT_eX]

[DOI]

Fundam. Informaticae, 2017

Program Verification using Constraint Handling Rules and Array Constraint Generalizations.

[BibT_eX]

[DOI]

Fundam. Informaticae, 2017

Enhancing Predicate Pairing with Abstraction for Relational Verification.

[BibT_eX]

[DOI]

CoRR, 2017

Regularity of non context-free languages over a singleton terminal alphabet.

[BibT_eX]

[DOI]

CoRR, 2017

Verifying Controllability of Time-Aware Business Processes.

[BibT_eX]

[DOI]

Proceedings of the Rules and Reasoning - International Joint Conference, 2017

Predicate Pairing with Abstraction for Relational Verification.

[BibT_eX]

[DOI]

Proceedings of the Logic-Based Program Synthesis and Transformation, 2017

2016

Removing Unnecessary Variables from Horn Clause Verification Conditions.

[BibT_eX]

[DOI]

Proceedings of the Proceedings 3rd Workshop on Horn Clauses for Verification and Synthesis, 2016

Relational Verification Through Horn Clause Transformation.

[BibT_eX]

[DOI]

Proceedings of the Static Analysis - 23rd International Symposium, 2016

Verification of Time-Aware Business Processes Using Constrained Horn Clauses.

[BibT_eX]

[DOI]

Proceedings of the Logic-Based Program Synthesis and Transformation, 2016

Verifying Relational Program Properties by Transforming Constrained Horn clauses.

[BibT_eX]

[DOI]

Proceedings of the 31st Italian Conference on Computational Logic, 2016

2015

Proving correctness of imperative programs by linearizing constrained Horn clauses.

[BibT_eX]

[DOI]

Theory Pract. Log. Program., 2015

A Rule-based Verification Strategy for Array Manipulating Programs.

[BibT_eX]

[DOI]

Fundam. Informaticae, 2015

Semantics-based generation of verification conditions by program specialization.

[BibT_eX]

[DOI]

Proceedings of the 17th International Symposium on Principles and Practice of Declarative Programming, 2015

2014

Program verification via iterated specialization.

[BibT_eX]

[DOI]

Sci. Comput. Program., 2014

Verifying Array Programs by Transforming Verification Conditions.

[BibT_eX]

[DOI]

Proceedings of the Verification, Model Checking, and Abstract Interpretation, 2014

VeriMAP: A Tool for Verifying Programs through Transformations.

[BibT_eX]

[DOI]

Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2014

2013

Generalization strategies for the verification of infinite state systems.

[BibT_eX]

[DOI]

Theory Pract. Log. Program., 2013

Preface.

[BibT_eX]

[DOI]

Gianfranco Rossi

Fundam. Informaticae, 2013

Proving Theorems by Program Transformation.

[BibT_eX]

[DOI]

Fundam. Informaticae, 2013

Controlling Polyvariance for Specialization-based Verification.

[BibT_eX]

[DOI]

Fundam. Informaticae, 2013

Verification of Imperative Programs by Constraint Logic Program Transformation.

[BibT_eX]

[DOI]

Proceedings of the Semantics, 2013

Verifying programs via iterated specialization.

[BibT_eX]

[DOI]

Proceedings of the ACM SIGPLAN 2013 Workshop on Partial Evaluation and Program Manipulation, 2013

Verification of Imperative Programs by Transforming Constraint Logic Programs.

[BibT_eX]

[DOI]

Proceedings of the 28th Italian Conference on Computational Logic, 2013

Program Transformation for Program Verification.

[BibT_eX]

[DOI]

Proceedings of the First International Workshop on Verification and Program Transformation, 2013

Verification of Imperative Programs through Transformation of Constraint Logic Programs.

[BibT_eX]

[DOI]

Proceedings of the First International Workshop on Verification and Program Transformation, 2013

2012

Improving Reachability Analysis of Infinite State Systems by Specialization.

[BibT_eX]

[DOI]

Fundam. Informaticae, 2012

Synthesizing Concurrent Programs Using Answer Set Programming.

[BibT_eX]

[DOI]

Emanuele De Angelis

Fundam. Informaticae, 2012

Constraint-based correctness proofs for logic program transformations.

[BibT_eX]

[DOI]

Formal Aspects Comput., 2012

Specialization with Constrained Generalization for Software Model Checking.

[BibT_eX]

[DOI]

Proceedings of the Logic-Based Program Synthesis and Transformation, 2012

Software Model Checking by Program Specialization.

[BibT_eX]

[DOI]

Proceedings of the 9th Italian Convention on Computational Logic, 2012

2011

Program transformation for development, verification, and synthesis of programs.

[BibT_eX]

[DOI]

Intelligenza Artificiale, 2011

RCRA 2009 Experimental Evaluation of Algorithms for Solving Problems with Combinatorial Explosion.

[BibT_eX]

[DOI]

Marco Gavanelli

Toni Mancini

Fundam. Informaticae, 2011

Using Real Relaxations during Program Specialization.

[BibT_eX]

[DOI]

Proceedings of the Logic-Based Program Synthesis and Transformation, 2011

2010

Transformations of logic programs on infinite lists.

[BibT_eX]

[DOI]

Theory Pract. Log. Program., 2010

Preface.

[BibT_eX]

[DOI]

Marco Gavanelli

Fabrizio Riguzzi

Fundam. Informaticae, 2010

Program Specialization for Verifying Infinite State Systems: An Experimental Evaluation.

[BibT_eX]

[DOI]

Proceedings of the Logic-Based Program Synthesis and Transformation, 2010

A Transformation Strategy for Verifying Logic Programs on Infinite Lists.

[BibT_eX]

[DOI]

Proceedings of the 25th Italian Conference on Computational Logic, 2010

The Transformational Approach to Program Development.

[BibT_eX]

[DOI]

Proceedings of the A 25-Year Perspective on Logic Programming: Achievements of the Italian Association for Logic Programming, 2010

2009

A Folding Rule for Eliminating Existential Variables from Constraint Logic Programs.

[BibT_eX]

[DOI]

Fundam. Informaticae, 2009

Deciding Full Branching Time Logic by Program Transformation.

[BibT_eX]

[DOI]

Proceedings of the Logic-Based Program Synthesis and Transformation, 2009

2008

Totally correct logic program transformations via well-founded annotations.

[BibT_eX]

[DOI]

High. Order Symb. Comput., 2008

A Folding Algorithm for Eliminating Existential Variables from Constraint Logic Programs.

[BibT_eX]

[DOI]

Proceedings of the Logic Programming, 24th International Conference, 2008

Program Transformation for Development, Verification, and Synthesis of Software.

[BibT_eX]

[DOI]

Proceedings of the Il Milione (i.e. 2^6), 2008

2007

Automatic Correctness Proofs for Logic Program Transformations.

[BibT_eX]

[DOI]

Proceedings of the Logic Programming, 23rd International Conference, 2007

2006

Preface: Program Transformation: Theoretical Foundations and Basic Techniques. Part 2.

[BibT_eX]

[DOI]

Fundam. Informaticae, 2006

Proving Properties of Constraint Logic Programs by Eliminating Existential Variables.

[BibT_eX]

[DOI]

Proceedings of the Logic Programming, 22nd International Conference, 2006

2005

Derivation of Efficient Logic Programs by Specialization and Reduction of Nondeterminism.

[BibT_eX]

[DOI]

High. Order Symb. Comput., 2005

Editorial.

[BibT_eX]

[DOI]

High. Order Symb. Comput., 2005

Program Transformation: Theoretical Foundations and Basic Techniques. Part 1.

[BibT_eX]

[DOI]

Fundam. Informaticae, 2005

Transformational Verification of Parameterized Protocols Using Array Formulas.

[BibT_eX]

[DOI]

Proceedings of the Logic Based Program Synthesis and Transformation, 2005

Proofs of Program Properties via Unfold/Fold Transformations of Constraint Logic Programs.

[BibT_eX]

[DOI]

Proceedings of the Transformation Techniques in Software Engineering, 17.-22. April 2005, 2005

2004

Transformations of logic programs with goals as arguments.

[BibT_eX]

[DOI]

Theory Pract. Log. Program., 2004

Transformation Rules for Locally Stratified Constraint Logic Programs

[BibT_eX]

[DOI]

CoRR, 2004

A theory of totally correct logic program transformations.

[BibT_eX]

[DOI]

Proceedings of the 2004 ACM SIGPLAN Workshop on Partial Evaluation and Semantics-based Program Manipulation, 2004

Automatic Proofs of Protocols via Program Transformation.

[BibT_eX]

[DOI]

Proceedings of the Monitoring, Security, and Rescue Techniques in Multiagent Systems, 2004

Transformation Rules for Locally Stratified Constraint Logic Programs.

[BibT_eX]

[DOI]

Proceedings of the Program Development in Computational Logic: A Decade of Research Advances in Logic-Based Program Development, 2004

2003

Editorial: Special Issue Dedicated to Bob Paige.

[BibT_eX]

[DOI]

High. Order Symb. Comput., 2003

2002

The List Introduction Strategy for the Derivation of Logic Programs.

[BibT_eX]

[DOI]

Formal Aspects Comput., 2002

Combining Logic Programs and Monadic Second Order Logics by Program Transformation.

[BibT_eX]

[DOI]

Proceedings of the Logic Based Program Synthesis and Tranformation, 2002

Program Derivation = Rules + Strategies.

[BibT_eX]

[DOI]

Proceedings of the Computational Logic: Logic Programming and Beyond, 2002

Specialization with Clause Splitting for Deriving Deterministic Constraint Logic Programs.

[BibT_eX]

[DOI]

Proceedings of the AGP 2002: Proceedings of the Joint Conference on Declarative Programming, 2002

2001

Verification of Sets of Infinite State Processes Using Program Transformation.

[BibT_eX]

[DOI]

Proceedings of the Logic Based Program Synthesis and Transformation, 2001

2000

Automated strategies for specializing constraint logic programs.

[BibT_eX]

Proceedings of the Extended Abstracts of the 10th International Workshop on Logic-based Program Synthesis and Transformation, 2000

Perfect Model Checking via Unfold/Fold Transformations.

[BibT_eX]

[DOI]

Proceedings of the Computational Logic, 2000

1999

Rules and Strategies for Contextual Specialization of Constraint Logic Programs.

[BibT_eX]

[DOI]

Proceedings of the Workshop on Optimization and Implementation of Declarative Programs, 1999

Synthesis and Transformation of Logic Programs Using Unfold/Fold Proofs.

[BibT_eX]

[DOI]

J. Log. Program., 1999

Transformation Rules for Logic Programs with Goals as Arguments.

[BibT_eX]

[DOI]

Proceedings of the Logic Programming Synthesis and Transformation, 1999

Transforming Inductive Definitions.

[BibT_eX]

Proceedings of the Logic Programming: The 1999 International Conference, Las Cruces, New Mexico, USA, November 29, 1999

1998

Program Specialization via Algorithmic Unfold/Fold Transformations.

[BibT_eX]

[DOI]

ACM Comput. Surv., 1998

1997

Future Directions in Program Transformation.

[BibT_eX]

[DOI]

ACM SIGPLAN Notices, 1997

Reducing Nondeterminism while Specializing Logic Programs.

[BibT_eX]

[DOI]

Proceedings of the Conference Record of POPL'97: The 24th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 1997

Program derivation via list introduction.

[BibT_eX]

Proceedings of the Algorithmic Languages and Calculi, 1997

1996

Developing correct and efficient logic programs by transformation.

[BibT_eX]

[DOI]

Knowl. Eng. Rev., 1996

Rules and Strategies for Transforming Functional and Logic Programs.

[BibT_eX]

[DOI]

ACM Comput. Surv., 1996

Enhancing Partial Deduction via Unfold/Fold Rules.

[BibT_eX]

[DOI]

Proceedings of the Logic Programming Synthesis and Transformation, 1996

How to Extend Partial Deduction to Derive the KMP String-Matching Algorithm from a Naive Specification (Poster Abstract).

[BibT_eX]

[DOI]

Proceedings of the Logic Programming, 1996

A Theory of Logic Program Specialization and Generalization for Dealing with Input Data Properties.

[BibT_eX]

[DOI]

Proceedings of the Partial Evaluation, International Seminar, 1996

A Comparative Revisitation of Some Program Transformation Techniques.

[BibT_eX]

[DOI]

Proceedings of the Partial Evaluation, International Seminar, 1996

1995

Unfolding - Definition - Folding, in this Order, for Avaoiding Unnecessary Variables in Logic Programs.

[BibT_eX]

[DOI]

Theor. Comput. Sci., 1995

Correctness of Logic Program Transformations Based on Existential Termination.

[BibT_eX]

[DOI]

Proceedings of the Logic Programming, 1995

1994

Transformation of Logic Programs: Foundations and Techniques.

[BibT_eX]

[DOI]

J. Log. Program., 1994

Completeness of Some Transformation Strategies for Avoiding Unnecessary Logical Variables.

[BibT_eX]

Proceedings of the Logic Programming, 1994

Total correctness of a goal replacement rule based on the unfold/fold proof method.

[BibT_eX]

Proceedings of the 1994 Joint Conference on Declarative Programming, 1994

1993

The Loop Absorption and the Generalization Strategies for the Development of Logic Programs and Partial Deduction.

[BibT_eX]

[DOI]

J. Log. Program., 1993

An Abstract Strategy for Transforming Logic Programs.

[BibT_eX]

Fundam. Informaticae, 1993

Synthesis of Programs from Unfold/Fold Proofs.

[BibT_eX]

Proceedings of the Logic Program Synthesis and Transformation, 1993

Rules and Strategies for Program Transformation.

[BibT_eX]

[DOI]

Proceedings of the Formal Program Development - IFIP TC2/WG 2.1 State-of-the-Art Report, 1993

Completeness of some Transformation Strategies for Avoiding Unncecessary Logical Variables.

[BibT_eX]

Proceedings of the 8th Italian Conference on Logic Programming, 1993

1992

Best-first Strategies for Incremental Transformations of Logic Programs.

[BibT_eX]

[DOI]

Proceedings of the Logic Program Synthesis and Transformation, 1992

1991

Semantics Preserving Transformation Rules for Prolog.

[BibT_eX]

[DOI]

Proceedings of the Symposium on Partial Evaluation and Semantics-Based Program Manipulation, 1991

An Automatic Transfomation Strategy for Avoiding Unnecessary Variables in Logic Programs (Extended Abstract).

[BibT_eX]

[DOI]

Proceedings of the Logic Program Synthesis and Transformation, 1991

1990

Observers, Experiments and Agents: a Comprehensive Approach to Parallelism.

[BibT_eX]

[DOI]

Stefano Kasangian

Proceedings of the Semantics of Systems of Concurrent Processes, 1990

Synthesis of Eureka Predicates for Developing Logic Programs.

[BibT_eX]

[DOI]

Proceedings of the ESOP'90, 1990

1989

The Power of the Lambda Abstraction Strategy for Program Derivation.

[BibT_eX]

J. Inf. Process. Cybern., 1989

Decidability Results and Characterization of Strategies for the Development of Logic Programs.

[BibT_eX]

Proceedings of the Logic Programming, 1989

1987

Derivation of Efficient Programs for Computing Sequences of Actions.

[BibT_eX]

[DOI]

Theor. Comput. Sci., 1987

Higher Order Generalization in Program Derivation.

[BibT_eX]

[DOI]

Proceedings of the TAPSOFT'87: Proceedings of the International Joint Conference on Theory and Practice of Software Development, 1987

On Learning with Imperfect Teachers.

[BibT_eX]

Zbigniew W. Ras

Maria Zemankova

Proceedings of the Methodologies for Intelligent Systems, 1987

Program Development Using Lambda Abstraction.

[BibT_eX]

[DOI]

Proceedings of the Foundations of Software Technology and Theoretical Computer Science, 1987

Enriched Categories for Local and Interaction Calculi.

[BibT_eX]

[DOI]

Stefano Kasangian

Proceedings of the Category Theory and Computer Science, 1987

1986

Using Facts for Improving the Parallel Execution of Functional Programs.

[BibT_eX]

Proceedings of the International Conference on Parallel Processing, 1986

Transformation Strategies for Deriving On Line Programs.

[BibT_eX]

[DOI]

Proceedings of the CAAP '86, 1986

Universal Models in Categories for Process Synchronization.

[BibT_eX]

[DOI]

Proceedings of the Mathematical Models for the Semantics of Parallelism, Advanced School, Rome, Italy, September 24, 1986

Factual Knowledge For Developing Concurrent Programs.

[BibT_eX]

[DOI]

Proceedings of the 5th National Conference on Artificial Intelligence. Philadelphia, 1986

1985

A Note on Cohen's "Eliminating Redundant Recursive Calls".

[BibT_eX]

[DOI]

ACM Trans. Program. Lang. Syst., 1985

Towers of Hanoi Problems: Deriving Iterative Solutions by Program Transformations.

[BibT_eX]

[DOI]

BIT, 1985

Categorical Models of Process Cooperation.

[BibT_eX]

[DOI]

Proceedings of the Category Theory and Computer Programming, 1985

1984

Methodologies for transformations and memoing in applicative languages.

[BibT_eX]

[DOI]

PhD thesis, 1984

Higher-order communications for concurrent programming.

[BibT_eX]

[DOI]

Parallel Comput., 1984

A methodology for improving parallel programs by adding communications.

[BibT_eX]

[DOI]

Proceedings of the Computation Theory, 1984

A Powerful Strategy for Deriving Efficient Programs by Transformation.

[BibT_eX]

[DOI]

Proceedings of the 1984 ACM Conference on LISP and Functional Programming, 1984

1982

Deriving very Efficient Algorithms for Evaluating Linear Recurrence Relations Using the Program Transformation Technique.

[BibT_eX]

[DOI]

Rod M. Burstall

Acta Informatica, 1982

Communicating agents for applicative concurrent programming.

[BibT_eX]

[DOI]

Proceedings of the International Symposium on Programming, 1982

1981

A property which guarantees termination in weak combinatory logic and subtree replacement systems.

[BibT_eX]

[DOI]

Notre Dame J. Formal Log., 1981

An Approach to Communications and Parallelism in Applicative Languages.

[BibT_eX]

[DOI]

Proceedings of the Formalization of Programming Concepts, 1981

Comparing and Putting Together Recursive Path Ordering, Simplification Orderings and Non-Ascending Property for Termination Proofs of Term Rewriting Systems.

[BibT_eX]

[DOI]

Proceedings of the Automata, 1981

A transformational approach for developing parallel programs.

[BibT_eX]

[DOI]