Alberto Pettorossi

According to our database1, Alberto Pettorossi
  • authored at least 139 papers between 1975 and 2017.
  • has a "Dijkstra number"2 of five.

Timeline

Legend:

Book 
In proceedings 
Article 
PhD thesis 
Other 

Links

On csauthors.net:

Bibliography

2017
Semantics-based generation of verification conditions via program specialization.
Sci. Comput. Program., 2017

Preface.
Fundam. Inform., 2017

Program Verification using Constraint Handling Rules and Array Constraint Generalizations.
Fundam. Inform., 2017

Enhancing Predicate Pairing with Abstraction for Relational Verification.
CoRR, 2017

Predicate Pairing for Program Verification.
CoRR, 2017

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

Verifying Controllability of Time-Aware Business Processes.
Proceedings of the Rules and Reasoning - International Joint Conference, 2017

2016
Removing Unnecessary Variables from Horn Clause Verification Conditions.
Proceedings of the Proceedings 3rd Workshop on Horn Clauses for Verification and Synthesis, 2016

Verification of Time-Aware Business Processes using Constrained Horn Clauses.
CoRR, 2016

Relational Verification Through Horn Clause Transformation.
Proceedings of the Static Analysis - 23rd International Symposium, 2016

Verification of Time-Aware Business Processes Using Constrained Horn Clauses.
Proceedings of the Logic-Based Program Synthesis and Transformation, 2016

Verifying Relational Program Properties by Transforming Constrained Horn clauses.
Proceedings of the 31st Italian Conference on Computational Logic, 2016

2015
Proving correctness of imperative programs by linearizing constrained Horn clauses.
TPLP, 2015

A Rule-based Verification Strategy for Array Manipulating Programs.
Fundam. Inform., 2015

Proving Correctness of Imperative Programs by Linearizing Constrained Horn Clauses.
CoRR, 2015

Semantics-based generation of verification conditions by program specialization.
Proceedings of the 17th International Symposium on Principles and Practice of Declarative Programming, 2015

2014
Program verification via iterated specialization.
Sci. Comput. Program., 2014

Verifying Array Programs by Transforming Verification Conditions.
Proceedings of the Verification, Model Checking, and Abstract Interpretation, 2014

VeriMAP: A Tool for Verifying Programs through Transformations.
Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2014

Program Verification using Constraint Handling Rules and Array Constraint Generalizations.
Proceedings of the 29th Italian Conference on Computational Logic, 2014

Program Verification using Constraint Handling Rules and Array Constraint Generalizations.
Proceedings of the VPT 2014. Second International Workshop on Verification and Program Transformation, 2014

2013
Generalization strategies for the verification of infinite state systems.
TPLP, 2013

Preface.
Fundam. Inform., 2013

Proving Theorems by Program Transformation.
Fundam. Inform., 2013

Controlling Polyvariance for Specialization-based Verification.
Fundam. Inform., 2013

Verification of Imperative Programs by Constraint Logic Program Transformation.
Proceedings of the Semantics, 2013

Verifying programs via iterated specialization.
Proceedings of the ACM SIGPLAN 2013 Workshop on Partial Evaluation and Program Manipulation, 2013

Verification of Imperative Programs by Transforming Constraint Logic Programs.
Proceedings of the 28th Italian Conference on Computational Logic, 2013

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

Verification of Imperative Programs through Transformation of Constraint Logic Programs.
Proceedings of the First International Workshop on Verification and Program Transformation, 2013

2012
Improving Reachability Analysis of Infinite State Systems by Specialization.
Fundam. Inform., 2012

Synthesizing Concurrent Programs Using Answer Set Programming.
Fundam. Inform., 2012

Constraint-based correctness proofs for logic program transformations.
Formal Asp. Comput., 2012

Specialization with Constrained Generalization for Software Model Checking.
Proceedings of the Logic-Based Program Synthesis and Transformation, 2012

Software Model Checking by Program Specialization.
Proceedings of the 9th Italian Convention on Computational Logic, 2012

2011
Program transformation for development, verification, and synthesis of programs.
Intelligenza Artificiale, 2011

RCRA 2009 Experimental Evaluation of Algorithms for Solving Problems with Combinatorial Explosion.
Fundam. Inform., 2011

Generalization Strategies for the Verification of Infinite State Systems
CoRR, 2011

Improving Reachability Analysis of Infinite State Systems by Specialization.
Proceedings of the Reachability Problems - 5th International Workshop, 2011

Using Real Relaxations during Program Specialization.
Proceedings of the Logic-Based Program Synthesis and Transformation, 2011

Controlling Polyvariance for Specialization-based Verification.
Proceedings of the 26th Italian Conference on Computational Logic, Pescara, Italy, August 31, 2011

Synthesizing Concurrent Programs using Answer Set Programming.
Proceedings of the 26th Italian Conference on Computational Logic, Pescara, Italy, August 31, 2011

2010
Transformations of logic programs on infinite lists.
TPLP, 2010

Preface.
Fundam. Inform., 2010

Transformations of Logic Programs on Infinite Lists
CoRR, 2010

Program Specialization for Verifying Infinite State Systems: An Experimental Evaluation.
Proceedings of the Logic-Based Program Synthesis and Transformation, 2010

A Transformation Strategy for Verifying Logic Programs on Infinite Lists.
Proceedings of the 25th Italian Conference on Computational Logic, 2010

Generalization Strategies for the Verification of Infinite State Systems.
Proceedings of the 25th Italian Conference on Computational Logic, 2010

The Transformational Approach to Program Development.
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.
Fundam. Inform., 2009

Deciding Full Branching Time Logic by Program Transformation.
Proceedings of the Logic-Based Program Synthesis and Transformation, 2009

2008
Totally correct logic program transformations via well-founded annotations.
Higher-Order and Symbolic Computation, 2008

Totally correct logic program transformations via well-founded annotations.
Higher-Order and Symbolic Computation, 2008

A Folding Algorithm for Eliminating Existential Variables from Constraint Logic Programs.
Proceedings of the Logic Programming, 24th International Conference, 2008

Program Transformation for Development, Verification, and Synthesis of Software.
Proceedings of the Il Milione (i.e. 2ˆ6), 2008

2007
Automatic Correctness Proofs for Logic Program Transformations.
Proceedings of the Logic Programming, 23rd International Conference, 2007

2006
Preface: Program Transformation: Theoretical Foundations and Basic Techniques. Part 2.
Fundam. Inform., 2006

Proving Properties of Constraint Logic Programs by Eliminating Existential Variables.
Proceedings of the Logic Programming, 22nd International Conference, 2006

2005
Derivation of Efficient Logic Programs by Specialization and Reduction of Nondeterminism.
Higher-Order and Symbolic Computation, 2005

Editorial.
Higher-Order and Symbolic Computation, 2005

Program Transformation: Theoretical Foundations and Basic Techniques. Part 1.
Fundam. Inform., 2005

Transformational Verification of Parameterized Protocols Using Array Formulas.
Proceedings of the Logic Based Program Synthesis and Transformation, 2005

Proofs of Program Properties via Unfold/Fold Transformations of Constraint Logic Programs.
Proceedings of the Transformation Techniques in Software Engineering, 17.-22. April 2005, 2005

2004
Transformations of logic programs with goals as arguments.
TPLP, 2004

Transformation Rules for Locally Stratified Constraint Logic Programs
CoRR, 2004

A theory of totally correct logic program transformations.
Proceedings of the 2004 ACM SIGPLAN Workshop on Partial Evaluation and Semantics-based Program Manipulation, 2004

Transformation Rules for Locally Stratified Constraint Logic Programs.
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.
Higher-Order and Symbolic Computation, 2003

Derivation of Efficient Logic Programs by Specialization and Reduction of Nondeterminism
CoRR, 2003

Combining Logic Programs and Monadic Second Order Logics by Program Transformation
CoRR, 2003

Transformations of Logic Programs with Goals as Arguments
CoRR, 2003

2002
The List Introduction Strategy for the Derivation of Logic Programs.
Formal Asp. Comput., 2002

Combining Logic Programs and Monadic Second Order Logics by Program Transformation.
Proceedings of the Logic Based Program Synthesis and Tranformation, 2002

Program Derivation = Rules + Strategies.
Proceedings of the Computational Logic: Logic Programming and Beyond, 2002

2001
Verification of Sets of Infinite State Processes Using Program Transformation.
Proceedings of the Logic Based Program Synthesis and Transformation, 2001

2000
Automated Strategies for Specializing Constraint Logic Programs.
Proceedings of the Logic Based Program Synthesis and Transformation, 2000

Automated strategies for specializing constraint logic programs.
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.
Proceedings of the Computational Logic, 2000

1999
Rules and Strategies for Contextual Specialization of Constraint Logic Programs.
Electr. Notes Theor. Comput. Sci., 1999

Synthesis and Transformation of Logic Programs Using Unfold/Fold Proofs.
J. Log. Program., 1999

Transformation Rules for Logic Programs with Goals as Arguments.
Proceedings of the Logic Programming Synthesis and Transformation, 1999

Transforming Inductive Definitions.
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.
ACM Comput. Surv., 1998

1997
Future Directions in Program Transformation.
SIGPLAN Notices, 1997

Reducing Nondeterminism while Specializing Logic Programs.
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.
Proceedings of the Algorithmic Languages and Calculi, 1997

1996
Developing correct and efficient logic programs by transformation.
Knowledge Eng. Review, 1996

Future Directions in Program Transformation.
ACM Comput. Surv., 1996

Rules and Strategies for Transforming Functional and Logic Programs.
ACM Comput. Surv., 1996

Enhancing Partial Deduction via Unfold/Fold Rules.
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).
Proceedings of the Logic Programming, 1996

A Theory of Logic Program Specialization and Generalization for Dealing with Input Data Properties.
Proceedings of the Partial Evaluation, International Seminar, 1996

A Comparative Revisitation of Some Program Transformation Techniques.
Proceedings of the Partial Evaluation, International Seminar, 1996

1995
Unfolding - Definition - Folding, in this Order, for Avaoiding Unnecessary Variables in Logic Programs.
Theor. Comput. Sci., 1995

Correctness of Logic Program Transformations Based on Existential Termination.
Proceedings of the Logic Programming, 1995

1994
Transformation of Logic Programs: Foundations and Techniques.
J. Log. Program., 1994

Completeness of Some Transformation Strategies for Avoiding Unnecessary Logical Variables.
Proceedings of the Logic Programming, 1994

Total correctness of a goal replacement rule based on the unfold/fold proof method.
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.
J. Log. Program., 1993

An Abstract Strategy for Transforming Logic Programs.
Fundam. Inform., 1993

Synthesis of Programs from Unfold/Fold Proofs.
Proceedings of the Logic Program Synthesis and Transformation, 1993

Rules and Strategies for Program Transformation.
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.
Proceedings of the 8th Italian Conference on Logic Programming, 1993

1992
Best-first Strategies for Incremental Transformations of Logic Programs.
Proceedings of the Logic Program Synthesis and Transformation, 1992

1991
Unfolding - Definition - Folding, in this Order, for Avaoiding Unnecessary Variables in Logic Programs.
Proceedings of the Programming Language Implementation and Logic Programming, 1991

Semantics Preserving Transformation Rules for Prolog.
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).
Proceedings of the Logic Program Synthesis and Transformation, 1991

1990
Observers, Experiments and Agents: a Comprehensive Approach to Parallelism.
Proceedings of the Semantics of Systems of Concurrent Processes, 1990

Synthesis of Eureka Predicates for Developing Logic Programs.
Proceedings of the ESOP'90, 1990

1989
The Power of the Lambda Abstraction Strategy for Program Derivation.
Elektronische Informationsverarbeitung und Kybernetik, 1989

Decidability Results and Characterization of Strategies for the Development of Logic Programs.
Proceedings of the Logic Programming, 1989

1987
Derivation of Efficient Programs for Computing Sequences of Actions.
Theor. Comput. Sci., 1987

Higher Order Generalization in Program Derivation.
Proceedings of the TAPSOFT'87: Proceedings of the International Joint Conference on Theory and Practice of Software Development, 1987

On Learning with Imperfect Teachers.
Proceedings of the Methodologies for Intelligent Systems, 1987

Program Development Using Lambda Abstraction.
Proceedings of the Foundations of Software Technology and Theoretical Computer Science, 1987

Enriched Categories for Local and Interaction Calculi.
Proceedings of the Category Theory and Computer Science, 1987

1986
Using Facts for Improving the Parallel Execution of Functional Programs.
Proceedings of the International Conference on Parallel Processing, 1986

Transformation Strategies for Deriving On Line Programs.
Proceedings of the CAAP '86, 1986

Universal Models in Categories for Process Synchronization.
Proceedings of the Mathematical Models for the Semantics of Parallelism, Advanced School, Rome, Italy, September 24, 1986

Factual Knowledge For Developing Concurrent Programs.
Proceedings of the 5th National Conference on Artificial Intelligence. Philadelphia, 1986

1985
A Note on Cohen's "Eliminating Redundant Recursive Calls".
ACM Trans. Program. Lang. Syst., 1985

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

Categorical Models of Process Cooperation.
Proceedings of the Category Theory and Computer Programming, 1985

1984
Methodologies for transformations and memoing in applicative languages.
PhD thesis, 1984

Higher-order communications for concurrent programming.
Parallel Computing, 1984

A methodology for improving parallel programs by adding communications.
Proceedings of the Computation Theory, 1984

A Powerful Strategy for Deriving Efficient Programs by Transformation.
LISP and Functional Programming, 1984

1982
Deriving very Efficient Algorithms for Evaluating Linear Recurrence Relations Using the Program Transformation Technique.
Acta Inf., 1982

Communicating agents for applicative concurrent programming.
Proceedings of the International Symposium on Programming, 1982

1981
A property which guarantees termination in weak combinatory logic and subtree replacement systems.
Notre Dame Journal of Formal Logic, 1981

An Approach to Communications and Parallelism in Applicative Languages.
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.
Proceedings of the Automata, 1981

A transformational approach for developing parallel programs.
Proceedings of the CONPAR 81: Conference on Analysing Problem Classes and Programming for Parallel Computing, 1981

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

Towards a theory of parallelism and communications for increasing efficiency in applicative languages.
Proceedings of the Logics of Programs and Their Applications, 1980

Synthesis of subtree rewriting systems behaviour by solving equations.
Proceedings of the Proc. 5eme Colleque de Lille sur les Arbres en Algebre et en Programmation, 1980

1979
On the definition of hierarchies of infinite sequential computations.
FCT, 1979

1978
Improving Memory Utilization in Transforming Recursive Programs (Extended Abstract).
Proceedings of the Mathematical Foundations of Computer Science 1978, 1978

1975
On subrecursiveness in weak combinatory logic.
Proceedings of the Lambda-Calculus and Computer Science Theory, 1975


  Loading...