Maurizio Proietti
Maurizio Proietti Maurizio Proietti
Senior Researcher

Istituto di Analisi dei Sistemi ed Informatica "Antonio Ruberti"
Via dei Taurini, 19
00185 Roma - Italy

Office n. 508
Tel.: +39 06 4993 7114
Fax: +39 06 4993 7137
email

Research groups

Selected publications
  • Emanuele De Angelis, Fabio Fioravanti, Meo M.C., Alberto Pettorossi, Maurizio Proietti: Verifying Controllability of Time-Aware Business Processes, Lecture Notes in Computer Science 10364, 103-118, 2017
  • Emanuele De Angelis, Fabio Fioravanti, Alberto Pettorossi, Maurizio Proietti: Enhancing Predicate Pairing with Abstraction for Relational Verification, in the Proceedings of the 27th International Symposium on Logic-Based Program Synthesis and Transformation (LOPSTR 2017), Preliminary version, Fioravanti F, Gallagher J. eds., CoRR, arXiv, 1708-07854, 2017
  • Emanuele De Angelis, Fabio Fioravanti, Alberto Pettorossi, Maurizio Proietti: Predicate Pairing for Program Verification, CoRR arXiv.org 1708-01473, 17000, 2017
  • Emanuele De Angelis, Fabio Fioravanti, Alberto Pettorossi, Maurizio Proietti: Program Verification using Constraint Handling Rules and Array Constraint Generalizations, Fundamenta Informaticae 150 (1), 73-117, 2017
  • Emanuele De Angelis, Fabio Fioravanti, Alberto Pettorossi, Maurizio Proietti: Semantics-based generation of verification conditions via program specialization, Science of Computer Programming 147, 78-108, 2017
  • Lisitsa A., Nemytykh A.P., Maurizio Proietti eds.: Proceedings Fifth International Workshop on Verification and Program Transformation, VPT@ETAPS 2017, Uppsala, Sweden, 29th April 2017, Electronic Proceedings in Theoretical Computer Science, 253, Elsevier, 2017
  • Alberto Pettorossi, Maurizio Proietti: Regularity of non context-free languages over a singleton terminal alphabet, CoRR arXiv.org, 18705, 2017
  • Maurizio Proietti, Seki H., Woodcock J: Editorial of the Special Issue on LOPSTR'14, Formal Aspects of Computing 29, 1-2, 2017
  • Emanuele De Angelis, Fabio Fioravanti, Meo M.C., Alberto Pettorossi, Maurizio Proietti: Verification of Time-Aware Business Processes using Constrained Horn Clauses, in the Proceedings of the International Symposium on Logic-based Program Transformation and Synthesis (LOPSTR 2016), 2016
  • De Angelis E., Fioravanti F., Meo M.C., Pettorossi A., Maurizio Proietti: Verifying Controllability of Time-Aware Business Processes, IASI-CNR, R. 16-08, 2016
  • Emanuele De Angelis, Fabio Fioravanti, Alberto Pettorossi, Maurizio Proietti: Horn Clause Transformation for Program Verification, Newsletter of the Association for Logic Programming, https://www.cs.nmsu.edu/ALP/2016/09, 2016
  • Emanuele De Angelis, Fabio Fioravanti, Alberto Pettorossi, Maurizio Proietti: Relational Verification Through Horn Clause Transformation, Lecture Notes in Computer Science 9837, 147-169, 2016
  • Emanuele De Angelis, Fabio Fioravanti, Alberto Pettorossi, Maurizio Proietti: Removing unnecessary variables from Horn clause verification conditions, in the Proceedings of 3rd International Workshop on Horn Clauses for Verification and Synthesis, Electronic Proceedings in Theoretical Computer Science, 219, 2016
  • De Angelis E., Fioravanti F., Pettorossi A., Maurizio Proietti: Semantics-based generation of verification conditions via program specialization, IASI-CNR, R. 16-09, 2016
  • Emanuele De Angelis, Fabio Fioravanti, Alberto Pettorossi, Maurizio Proietti: Verifying relational program properties by transforming constrained Horn clauses, in the Proceedings of Proceedings of the 31st Italian Conference on Computational Logic, CEUR-WS, 1645, 2016
  • Alberto Pettorossi, Maurizio Proietti: First Order Predicate Calculus and Logic Programming. Fourth Edition., Aracne Editrice, 2016
  • Maurizio Proietti: Transforming Constrained Horn Clauses for Program Verification, Abstract of the Keynote Talk at the 3rd Workshop on Horn Clauses for Verification and Synthesis, 2016
  • Emanuele De Angelis, Fabio Fioravanti, Alberto Pettorossi, Maurizio Proietti: A Rule-based Verification Strategy for Array Manipulating Programs, Fundamenta Informaticae 140, 329-355, 2015
  • Emanuele De Angelis, Fabio Fioravanti, Alberto Pettorossi, Maurizio Proietti: Automated Verification of Relational Program Properties, IASI-CNR, R. 15-07, 2015
  • Emanuele De Angelis, Fabio Fioravanti, Alberto Pettorossi, Maurizio Proietti: Program Verification using Constraint Handling Rules and Array Constraint Generalizations, IASI-CNR, R. 15-08, 2015
  • Emanuele De Angelis, Fabio Fioravanti, Alberto Pettorossi, Maurizio Proietti: Proving Correctness of Imperative Programs by Linearizing Constrained Horn Clauses, Theory and Practice of Logic Programming 15, 635-650, 2015
  • Emanuele De Angelis, Fabio Fioravanti, Alberto Pettorossi, Maurizio Proietti: Proving Horn Clause Specifications of Imperative Programs, IASI-CNR, R. 15-09, 2015
  • Emanuele De Angelis, Fabio Fioravanti, Alberto Pettorossi, Maurizio Proietti: Semantics-based generation of verification conditions by program specialization, ACM Symposium on Principles and Practice of Declarative Programming, 2015
  • Fabio Fioravanti, Maurizio Proietti, Senni V.: Efficient generation of test data structures using constraint logic programming and program transformation, Journal of Logic and Computation 25, 1263-1283, 2015
  • Maurizio Proietti, Seki H. eds.: Logic-Based Program Synthesis and Transformation: 24th International Symposium, LOPSTR 2014 Canterbury, UK, September 9-11, 2014 Revised Selected Papers, Lecture Notes in Computer Science, 8981, 2015
  • Emanuele De Angelis, Fabio Fioravanti, Navas J, Maurizio Proietti: Verification of Programs by Combining Iterated Specialization with Interpolation, in the Proceedings of First Workshop on Horn Clauses for Verification and Synthesis, Electronic Proceedings in Theoretical Computer Science, 169, 2014
  • Emanuele De Angelis, Fabio Fioravanti, Alberto Pettorossi, Maurizio Proietti: A Rule-based Verification Strategy for Array Manipulating Programs, IASI-CNR, R. 14-07, 2014
  • Emanuele De Angelis, Fabio Fioravanti, Alberto Pettorossi, Maurizio Proietti: Program Verification using Constraint Handling Rules and Array Constraint Generalizations, in the Proceedings of Proceedings of VPT 2014, EasyChair Proceedings in Computing (EPiC) series, 28, 2014
  • Emanuele De Angelis, Fabio Fioravanti, Alberto Pettorossi, Maurizio Proietti: Program verification via iterated specialization, Science of Computer Programming 95, 149-175, 2014
  • Emanuele De Angelis, Fabio Fioravanti, Alberto Pettorossi, Maurizio Proietti: Verifying Array Programs by Transforming Verification Conditions, Lecture Notes in Computer Science 8318, 182-202, 2014
  • Emanuele De Angelis, Fabio Fioravanti, Alberto Pettorossi, Maurizio Proietti: VeriMAP: A tool for verifying programs through transformations, Lecture Notes in Computer Science 8413, 568-574, 2014
  • Maurizio Proietti, Seki H.: Logic-Based Program Synthesis and Transformation, Preliminary Proceedings, IASI-CNR, R. 14-03, 2014
  • Maurizio Proietti, Smith F.: Reasoning on Data-Aware Business Processes with Constraint Logic, in the Proceedings of Proceedings of the 4th International Symposium on Data-driven Process Discovery and Analysis (SIMPDA 2014), CEUR-WS, 1293, 2014
  • Smith F., Maurizio Proietti: Behavioral Reasoning on Semantic Business Processes in a Rule-Based Framework, in: Agents and Artificial Intelligence, Communications in Computer and Information Science, 449, Springer, 293-313, 2014
  • Smith F., Maurizio Proietti: Ontology-based Representation and Reasoning on Process Models: A Logic Programming Approach, Computing Research Repository (CoRR), arXiv:1410.1776, 14000, 2014
  • Emanuele De Angelis, Fabio Fioravanti, Alberto Pettorossi, Maurizio Proietti: Program Verification via Iterated Specialization, IASI-CNR, R. 13-11, 2013
  • Emanuele De Angelis, Fabio Fioravanti, Alberto Pettorossi, Maurizio Proietti: Specialization with Constrained Generalization for Software Model Checking, Lecture Notes in Computer Science Vol. 7844, pp. 51-70, 2013
  • Emanuele De Angelis, Fabio Fioravanti, Alberto Pettorossi, Maurizio Proietti: Verification of Imperative Programs by Constraint Logic Program Transformation, in the Proceedings of SAIRP 2013, Festschrift for Dave Schmidt, Electronic Proceedings in Theoretical Computer Science, Vol 129, pp. 186-210, 2013
  • Emanuele De Angelis, Fabio Fioravanti, Alberto Pettorossi, Maurizio Proietti: Verification of Imperative Programs by Transforming Constraint Logic Programs, in the Proceedings of the 28th Italian Conference on Computational Logic (CILC 2013), CEUR-WS, Vol. 1068, pp. 83-98, 2013
  • Emanuele De Angelis, Fabio Fioravanti, Alberto Pettorossi, Maurizio Proietti: Verification of Imperative Programs through Transformation of Constraint Logic Programs, in the Proceedings of First International Workshop on Verification and Program Transformation (VPT 2013), EasyChair Proceedings in Computing (EPiC) series, Vol. 16, pp. 30-41, 2013
  • Emanuele De Angelis, Fabio Fioravanti, Alberto Pettorossi, Maurizio Proietti: Verifying Array Programs by Transforming Verification Conditions, IASI-CNR, R. 13-12, 2013
  • Emanuele De Angelis, Fabio Fioravanti, Alberto Pettorossi, Maurizio Proietti: Verifying Programs via Iterated Specialization, in the Proceedings of Partial Evaluation and Program Manipulation (PEPM '13), ACM-SIGPLAN, 2013
  • Diamantini C., Potena D., Maurizio Proietti, Smith F., Storti E., Francesco Taglino: A Semantic Framework for Knowledge Management in Virtual Innovation Factories, International Journal of Information System Modeling and Design Vol 4(4), 70-92, 2013
  • Fabio Fioravanti, Alberto Pettorossi, Maurizio Proietti, Senni V.: Controlling Polyvariance for Specialization-based Verification, Fundamenta Informaticae 124, 483-502, 2013
  • Fabio Fioravanti, Alberto Pettorossi, Maurizio Proietti, Senni V.: Generalization Strategies for the Verification of Infinite State Systems, Theory and Practice of Logic Programming 13, 175-199, 2013
  • Fabio Fioravanti, Alberto Pettorossi, Maurizio Proietti, Senni V.: Proving Theorems by Program Transformation, Fundamenta Informaticae 127 (1-4), 115-134, 2013
  • Fabio Fioravanti, Maurizio Proietti, Senni V.: Efficient Generation of Test Data Structures Using Constraint Logic Programming and Program Transformation, IASI-CNR, R. 13-10, 2013
  • Alberto Pettorossi, Maurizio Proietti: First Order Predicate Calculus and Logic Programming, Third Edition, Aracne Editrice Roma, 2013
  • Alberto Pettorossi, Maurizio Proietti: Program Transformation for Program Verification, in the Proceedings of First International Workshop on Verification and Program Transformation (VPT 2013), EasyChair Proceedings in Computing (EPiC) series, Vol. 16, pp. 13-14, 2013
  • Smith F., De Sanctis D., Maurizio Proietti: A Platform for Managing Business Process Knowledge Bases via Logic Programming, in the Proceedings of the 28th Italian Conference on Computational Logic (CILC 2013), CEUR-WS, Vol. 1068, pp. 247-251, 2013
  • Smith F., Maurizio Proietti: Rule-Based Behavioural Reasoning on Semantic Business Processes, in the Proceedings of 5th International Conference on Agents and Artificial Intelligence, ICAART, pp. 130-143, 2013
  • Emanuele De Angelis, Fabio Fioravanti, Alberto Pettorossi, Maurizio Proietti: Branching Preserving Specialization for Software Model Checking, in the Proceedings of 22nd International Symposium on Logic-Based Program Synhesis and Transformation (LOPSTR 2012), Albert E. ed., 2012
  • Emanuele De Angelis, Fabio Fioravanti, Alberto Pettorossi, Maurizio Proietti: Software Model Checking by Program Specialization, in the Proceedings of 27th Italian Conference on Computational Logic (CILC-2012), CEUR-WS, 857, 2012
  • Emanuele De Angelis, Fabio Fioravanti, Alberto Pettorossi, Maurizio Proietti: Verifying Programs via Iterated Specialization, IASI-CNR, R. 12-22, 2012
  • Emanuele De Angelis, Alberto Pettorossi, Maurizio Proietti: Synthesizing Concurrent Programs Using Answer Set Programming, Fundamenta Informaticae 120, 205-229, 2012
  • Emanuele De Angelis, Alberto Pettorossi, Maurizio Proietti: Using Answer Set Programming Solvers to Synthesize Concurrent Programs, IASI-CNR, R. 12-19, 2012
  • Fabio Fioravanti, Alberto Pettorossi, Maurizio Proietti, Senni V.: Improving Reachability Analysis of Infinite State Systems by Specialization, Fundamenta Informaticae 119, 281-300, 2012
  • Fabio Fioravanti, Alberto Pettorossi, Maurizio Proietti, Senni V.: Using Real Relaxations During Program Specialization, in: Logic-based Program Synthesis and Transformation, Selected papers, Vidal G. ed., Lecture Notes in Computer Science, 7225, Springer Berlin, Heidelberg, 106-122, 2012
  • Alberto Pettorossi, Maurizio Proietti, Senni V.: Constraint-Based Correctness Proofs for Logic Program Transformations, Formal Aspects of Computing 24, 569-594, 2012
  • Smith F., Michele Missikoff, Maurizio Proietti: Ontology-Based Querying of Composite Services, in: Business System Management and Engineering, Lecture Notes in Computer Science, 7350, Springer Berlin, 159-180, 2012
  • Smith F., Maurizio Proietti: Rule-Based Behavioral Reasoning on Semantic Business Processes, IASI-CNR, R. 12-21, 2012
  • Francesco Taglino, Smith F., Maurizio Proietti: A Software Platform for Semantics-based Enterprise Knowledge Management, in: Proceedings of the Fifth Interop-Vlab.It Workshop on Complexity of Systems, Complexity of Interoperability, CEUR-WS, 915, 43-50, 2012
  • Francesco Taglino, Smith F., Maurizio Proietti: Knowledge-Based Support to Business Innovation, in: New Generation Enterprise and Business Innovation Systems 2012 (NGEBIS 2012), CEUR-WS, 864, 37-44, 2012
  • Emanuele De Angelis, Alberto Pettorossi, Maurizio Proietti: Synthesizing Concurrent Programs using Answer Set Programming, in the Proceedings of International Workshop on Concurrency, Specification and Programming (CS&P 2011), Pultusk, Poland, 28-30 Sept. 2011, 2011
  • Fabio Fioravanti, Alberto Pettorossi, Maurizio Proietti, Senni V.: Controlling Polyvariance for Specialization-Based Verification, in the Proceedings of 26th Italian Conference on Computational Logic (CILC'11), Fioravanti F ed., CEUR-WS, 2011
  • Fabio Fioravanti, Alberto Pettorossi, Maurizio Proietti, Senni V.: Improving Reachability Analysis of Infinite State Systems by Specialization, in: Reachability Problems (RP 2011), Delzanno G, Potapov I eds., Lecture Notes in Computer Science, 6945, Springer Berlin Heidelberg, 165-179, 2011
  • Fabio Fioravanti, Alberto Pettorossi, Maurizio Proietti, Senni V.: Program Specialization for Verifying Infinite State Systems: An Experimental Evaluation, in: Logic-Based Program Synthesis and Transformation, 20th International Symposium, LOPSTR '10, Revised Selected Papers, Alpuente M ed., Lecture Notes in Computer Science, 6564, Springer Berlin Heidelberg, 164-183, 2011
  • Fabio Fioravanti, Alberto Pettorossi, Maurizio Proietti, Senni V.: Program Transformation for Development, Verification, and Synthesis of Programs, Intelligenza Artificiale 5, 119-125, 2011
  • Fabio Fioravanti, Alberto Pettorossi, Maurizio Proietti, Senni V.: Using Real Relaxations During Program Specialization, in the Proceedings of 21st International Symposium on Logic-Based Synthesis and Transformation (LOPSTR 2011), Univ. of Southern Denmark, Odense, Denmark, pp. 96-111, 2011
  • Fabio Fioravanti, Maurizio Proietti, Alberto Pettorossi, Senni V.: A Constraint-Based Transformation for Verifying Infinite State Systems, IASI-CNR, R. 11-23, 2011
  • Michele Missikoff, Maurizio Proietti, Smith F.: Querying Business Processes and Ontologies in a Logic Programming Environment, in the Proceedings of 19th Italian Symposium on Advanced Database Systems, SEBD 2011, Maratea, Italy, 2011
  • Michele Missikoff, Maurizio Proietti, Smith F.: Querying Semantically Enriched Business Processes, in: 22nd International Conference on Database and Expert Systems Applications (DEXA 2011), Lecture Notes in Computer Science, 6861, Springer Berlin Heidelberg, 294-302, 2011
  • Alberto Pettorossi, Maurizio Proietti, Senni V.: Constraint-Based Correctness Proofs for Logic Program Transformations, IASI-CNR, R. 11-24, 2011
  • De Nicola A., Michele Missikoff, Maurizio Proietti, Smith F.: A Logic-Based Method for Business Process Knowledge Base Management, in the Proceedings of 18th Italian Symposium on Advanced Database Systems, SEBD 2010, Rimini, Italy, 2010
  • De Nicola A., Michele Missikoff, Maurizio Proietti, Smith F.: An Open Platform for Business Process Modeling and Verification, in the Proceedings of International Conference on Database and Expert Systems Applications, DEXA, September 2010, Lecture Notes in Computer Science, 6261, 2010
  • Fabio Fioravanti, Alberto Pettorossi, Maurizio Proietti, Senni V.: Generalization Strategies for the Verification of Infinite State Systems, in the Proceedings of 25th Italian Conference on Computational Logic (CILC'10), Leone N., Faber W. eds., CEUR-WS, 598, 2010
  • Fabio Fioravanti, Alberto Pettorossi, Maurizio Proietti, Senni V.: Program Specialization for Verifying Infinite State Systems: An Experimental Evaluation, in the Proceedings of 20th International Symposium on Logic-Based Synthesis and Transformation (LOPSTR 2010), July 23-25, 2010, Hagenberg, Austria, RISC-Linz Report Series No. 10-14., Alpuente M ed., 2010
  • Michele Missikoff, Maurizio Proietti, Smith F.: A Business Process Knowledge Base for Composite Services Development, in the Proceedings of International Workshop on Business System Management and Engineering, BSME, Malaga, 2010
  • Michele Missikoff, Maurizio Proietti, Smith F.: Linking Ontologies to Business Process Schemas, IASI-CNR, R. 10-20, 2010
  • Michele Missikoff, Maurizio Proietti, Smith F.: Querying semantically annotated business processes, IASI-CNR, R. 10-22, 2010
  • Michele Missikoff, Maurizio Proietti, Smith F.: Reasoning on Business Processes and Ontologies in a Logic Programming Environment, in the Proceedings of 3rd Interop-Vlab.It Workshop, CEUR-WS, 653, 2010
  • Alberto Pettorossi, Maurizio Proietti, Senni V.: A Transformation Strategy for Verifying Logic Programs on Infinite Lists, in the Proceedings of 25th Italian Conference on Computational Logic (CILC'10), Leone N., Faber W. eds., CEUR-WS, 598, 2010
  • Alberto Pettorossi, Maurizio Proietti, Senni V.: Deciding Full Branching Time Logic by Program Transformation, in: 19th International Symposium on Logic-Based Synthesis and Transformation (LOPSTR '09), Revised Selected Papers, De Schreye D. ed., Lecture Notes in Computer Science, 6037, Springer, 5-21, 2010
  • Alberto Pettorossi, Maurizio Proietti, Senni V.: The Transformational Approach to Program Development, in: A 25 Year Perspective on Logic Programming, Pontelli E., Dovier A. eds., Lecture Notes in Computer Science, 6125, Springer, 112-135, 2010
  • Alberto Pettorossi, Maurizio Proietti, Senni V.: Transformations of Logic Programs on Infinite Lists, Theory and Practice of Logic Programming 10, 383-399, 2010
  • De Nicola A., Michele Missikoff, Maurizio Proietti, Smith F.: A Logic-Based Method for BPMN Diagrams Verification, IASI-CNR, R. 09-07, 2009
  • De Nicola A., Michele Missikoff, Maurizio Proietti, Smith F.: A Logic-Based Method for BPMN Diagrams Verification, IASI-CNR, R. 09-09, 2009
  • Alberto Pettorossi, Maurizio Proietti, Senni V.: Deciding Full Branching Time Logic by Program Transformation, in the Proceedings of 19th International Symposium on Logic Program Synthesis and Transformation (LOPSTR 2009), De Schreye D., Quaresma P. eds., 2009
  • Alberto Pettorossi, Maurizio Proietti, Senni V.: The Transformational Approach to Program Development, IASI-CNR, R. 09-06, 2009
  • Alberto Pettorossi, Maurizio Proietti, Senni V.: Transformational Verification of Linear Temporal Logic, Electronic Proceedings of the 2009 Italian Conference on Computational Logic (CILC 2009), 24-26 June, 2009, Ferrara, Italy. http://www.ing.unife.it/eventi/cilc09/accepted.shtml, 2009
  • Senni V., Alberto Pettorossi, Maurizio Proietti: A Folding Rule for Eliminating Existential Variables from Constraint Logic Programs, Fundamenta Informaticae 96 (3), 373-393, 2009
  • Alberto Pettorossi, Maurizio Proietti: Totally Correct Logic Program Transformations Via Well-Founded Annotations, Higher-Order and Symbolic Computation 21, 193-235, 2008
  • Alberto Pettorossi, Maurizio Proietti, Renault S.: Derivation of Efficient Logic Programs by Specialization and Reduction of Nondeterminism, Henglein F., Danvy O., Pettorossi A., Mairson H. eds., Automatic Program Development, Springer Heidelberg, 130-177, 2008
  • Senni V., Alberto Pettorossi, Maurizio Proietti: Folding Transformation Rules for Constraint Logic Programs, Electronic Proceedings of the 2008 Italian Conference on Computational Logic (CILC 2008), 10-12 July, 2008, Perugia, Italy. http://www.dipmat.unipg.it/CILC08/, 2008
  • Senni V., Maurizio Proietti, Alberto Pettorossi: A Folding Algorithm for Eliminating Existential Variables from Constraint Logic Programs, in the Proceedings of 24th International Conference on Logic Programming, Garcia de la Banda M., Pontelli E. eds., Lecture Notes in Computer Science, 5366, pp. 284-300, 2008
  • Fabio Fioravanti, Alberto Pettorossi, Maurizio Proietti: Verifying Infinite State Systems by Specializing Constraint Logic Programs, IASI-CNR, R. 657, 2007
  • Alberto Pettorossi, Maurizio Proietti, Senni V.: Automatic Correctness Proofs for Logic Program Transformations, in the Proceedings of 23rd International Conference on Logic Programming (ICLP '07), Niemela I., Dahl V. eds., Lecture Notes in Computer Science, 4670, pp. 364-379, Springer, 2007
  • Alberto Pettorossi, Maurizio Proietti: Program Transformation: Theoretical Foundations and Basic Techniques. Part 2., Fundamenta Informaticae 69, i-iii, 2006
  • Alberto Pettorossi, Maurizio Proietti, Senni V.: Proofs of Program Properties via Unfold/Fold Transformations of Constraint Logic Programs, Electronic Proceedings of the Dagstuhl Seminar 05161, Transformation Techniques in Software Engineering, IBFI, Germany, 2006
  • Alberto Pettorossi, Maurizio Proietti, Senni V.: Proving Properties of Constraint Logic Programs by Eliminating Existential Variables, in: Proceedings of the 22nd International Conference on Logic Programming (ICLP '06), Etalle S., Truszczynski M. eds., Lecture Notes in Computer Science, 4079, Springer-Verlag, 179-195, 2006
  • Fabio Fioravanti, Alberto Pettorossi, Maurizio Proietti: Automatic Proofs of Protocols via Program Transformation., in: Monitoring, Security, and Rescue Techniques in Multiagent Systems, Advances in Soft Computing Series, Skowron A., Dunin-Keplicz B., Jankowski A., Szczuka M. eds., Advances in Soft Computing, 99-116, 2005
  • Alberto Pettorossi, Maurizio Proietti: Program Transformation: Theoretical Foundations and Basic Techniques. Part 1, Fundamenta Informaticae 66, i-iii, 2005
  • Alberto Pettorossi, Maurizio Proietti, Renault S.: Derivation of Efficient Logic Programs by Specialization and Reduction of Nondeterminism, Higher-Order and Symbolic Computation 18 (1-2), 121-210, 2005
  • Alberto Pettorossi, Maurizio Proietti, Senni V.: Transformational Verification of Parameterized Protocols Using Array Formulas., in the Proceedings of 15th International Symposium on Logic Based Program Synthesis and Transformation (LOPSTR 2005), Imperial College, London, UK, September 7-9, Hill P.M ed., Lecture Notes in Computer Science, 2005
  • Alberto Pettorossi, Maurizio Proietti, Senni V.: Verifying parameterized protocols by transforming stratified logic programs, Electronic Proceedings of the Italian Annual Meeting on Computational Logic (CILC'05), June 21-22, Roma, Italy, 2005
  • Alberto Pettorossi, Maurizio Proietti: A theory of totally correct logic program transformations, in the Proceedings of 2004 ACM-SIGPLAN Symposium on Partial Evaluation and Semantics-Based Program Manipulation, ACM-SIGPLAN, 2004
  • Alberto Pettorossi, Maurizio Proietti: Totally correct logic program transformations using well-founded annotations, in the Proceedings of Italian Conference on Computational Logic, Rossi G.F., Panegai E. eds., Quaderni del Dipartimento di Matematica - Università degli Studi di Parma, 2004
  • Alberto Pettorossi, Maurizio Proietti: Transformations of logic programs with goals as arguments, Theory and Practice of Logic Programming 4, 495-537, 2004
  • Alberto Pettorossi, Maurizio Proietti, Fabio Fioravanti: Transformation rules for locally stratified constraint logic programs, in: Program Development in Computational Logic, Bruynooghe M., Lau K.-K. eds., Lecture Notes in Computer Science, 3049, Springer Heidelberg, 291-339, 2004
  • Fabio Fioravanti, Alberto Pettorossi, Maurizio Proietti: Combining Logic Programs and Monadic Second Order Logics by Program Transformation, in: 12th International Symposium on Logic-based Program Develpment and Transformation, Leuschel M. ed., Lecture Notes in Computer Science, 2664, 160-181, 2003
  • Fabio Fioravanti, Alberto Pettorossi, Maurizio Proietti: A Specialization Technique For Deriving Deterministic Constraint Logic Programs and Its Application to Pattern Matching, in the Proceedings of AGP'02, 2002 Joint Conference on Declarative Programming, 16 - 18 September 2002, Madrid, Spain, Moreno-Navarro J.J., Marino-Carballo J. eds., 2002
  • Fabio Fioravanti, Alberto Pettorossi, Maurizio Proietti: Specialization with Clause Splitting for Deriving Deterministic Constraint Logic Programs, in the Proceedings of SMC'02, 6 - 9 October, 2002, Hammamet, Tunisia, IEEE International Conference on Systems, Man, and Cybernetics, 2002
  • Fabio Fioravanti, Alberto Pettorossi, Maurizio Proietti: Verification of Sets of Infinite State Systems Using Program Transformation, in: Logic Based Program Synthesis and Transformation, Pettorossi A. ed., Lecture Notes in Computer Science, 2372, 111-128, 2002
  • Alberto Pettorossi, Maurizio Proietti: First Order Predicate Calculus and Logic Programming, Aracne Roma, 2002
  • Alberto Pettorossi, Maurizio Proietti: Program Derivation = Rules + Strategies, Lecture Notes in Artificial Intelligence, 2407, 273-309, 2002
  • Alberto Pettorossi, Maurizio Proietti: The List Introduction Strategy for the Derivation of Logic Programs, Formal Aspects of Computing 13, 233-251, 2002
  • Fabio Fioravanti, Alberto Pettorossi, Maurizio Proietti: Automated Strategies for Specializing Constraint Logic Programs, Lecture Notes in Computer Science, 2042, Springer-Verlag, 124-146, 2001
  • Fabio Fioravanti, Alberto Pettorossi, Maurizio Proietti: Verifying CTL Properties of Infinite State Systems by Specializing Constraint Logic Programs, in the Proceedings of ACM-Sigplan International Workshop on Verification and Computational Logic, VCL'2001, Florence, Italy, September 4, 2001, pp. 85-96., 2001
  • Fabio Fioravanti, Alberto Pettorossi, Maurizio Proietti: Rules and Strategies for Contextual Specialization of Constraint Logic Programs, Theoretical Computer Science, Electronic Notes 30 (2), 2000
  • Alberto Pettorossi, Maurizio Proietti: Perfect Model Checking via Unfold/Fold Transformations, in the Proceedings of First International Conference on Computational Logic, CL'2000, London, 24-28 July, 2000, Lloyd J.W., others eds., Lecture Notes in Artificial Intelligence, 1861, Springer, 613-628, 2000
  • Alberto Pettorossi, Maurizio Proietti: Transformation Rules for Logic Programs with Goals as Arguments, in the Proceedings of Logic-based Program Synthesis and Transformation, LOPSTR '99, Venezia, Italy, Bossi A. ed., Lecture Notes in Computer Science, 1817, 2000
  • Fabio Fioravanti, Alberto Pettorossi, Maurizio Proietti: Rules and Strategies for Contextual Specialization of Constraint Logic Programs, in the Proceedings of ICLP'99 Workshop on Optimization and Implementation of Declarative Programming Languages, WOID '99, Las Cruces University, New Mexico, USA, December 2--3, Leuschel M. ed., 1999
  • Fabio Fioravanti, Maurizio Proietti: Contextual Specialization of Constraint Logic Programs, in the Proceedings of Joint Conference on Declarative Programming, L'Aquila, Italy, Vilares Ferro M., Meo M.C. eds., 1999
  • Alberto Pettorossi, Maurizio Proietti: Synthesis and Transformation of Logic Programs Using Unfold/Fold Proofs, Journal of Logic Programming 41, 197-230, 1999
  • Maurizio Proietti, Alberto Pettorossi: Transforming Inductive Definitions, in the Proceedings of 1999 International Conference on Logic Programming, De Schreye D. ed., Logic Programming Series, 1999
  • Alberto Pettorossi, Maurizio Proietti: Program Specialization via Algorithmic Unfold/Fold Transformations, ACM Computing Surveys 30, 6-es, 1998
  • Alberto Pettorossi, Maurizio Proietti: Transformation of Logic Programs, Hogger C.J., Gabbay D.M., Robinson J.A. eds., Handbook of Logic in Artificial Intelligence and Logic Programming, 5, 697-787, 1998
  • Alberto Pettorossi, Maurizio Proietti: Flexible Continuations in Logic Programs via Unfold/Fold Transformations and Goal Generalization, in the Proceedings of 2nd ACM SIGPLAN Workshop on Continuations, ENS, Paris, France, Danvy O. ed., BRICS Notes Series, N6-93-13, 1997
  • Alberto Pettorossi, Maurizio Proietti: Future Directions in Program Transformation, in the Proceedings of Workshop on Strategic Directions in Computing Research, MIT, Cambridge, USA, SIGPLAN Notices, 32/1, ACM Press, 99-102, 1997
  • Alberto Pettorossi, Maurizio Proietti: Program Derivation via List Introduction, in the Proceedings of IFIP TC2 Working Conference on Algorithmic Languages and Calculi, Le Bischenberg, France, Bird R., Meertens L.G.L.T. eds., Chapman \& Hall, 296-323, 1997
  • Alberto Pettorossi, Maurizio Proietti, Renault S.: Enhancing Partial Deduction via Unfold/Fold Rules, in the Proceedings of Logic Program Synthesis and Transformation, 6th International Workshop, Stockholm, Sweden, Gallagher J. ed., Lecture Notes in Computer Science, 1207, Springer-Verlag, 147-168, 1997
  • Alberto Pettorossi, Maurizio Proietti, Renault S.: Reducing Nondeterminism while Specializing Logic Programs, in the Proceedings of 24th ACM Symposium on Principles of Programming Languages, La Sorbonne, Paris, France, SIGPLAN Notices, 1997
  • Alberto Pettorossi, Maurizio Proietti: A Comparative Revisitation of Some Program Transformation Techniques, in the Proceedings of Dagstuhl Seminar on Partial Evaluation., Thiemann P., Danvy O., Glück R. eds., Lecture Notes in Computer Science, 1110, 1996
  • Alberto Pettorossi, Maurizio Proietti: A Theory of Logic Program Specialization and Generalization for Dealing with Input Data Properties, in the Proceedings of Dagstuhl Seminar on Partial Evaluation, Thiemann P., Danvy O., Glück R. eds., Lecture Notes in Computer Science, 1110, 1996
  • Alberto Pettorossi, Maurizio Proietti: Developing Correct and Efficient Logic Programs by Transformation, Knowledge Engineering Review 11 (4), 347-360, 1996
  • Alberto Pettorossi, Maurizio Proietti: Rules and Strategies for Transforming Functional and Logic Programs, ACM Computing Surveys 28 (2), 360-414, 1996
  • Alberto Pettorossi, Maurizio Proietti, Renault S.: How to Extend Partial Deduction to Derive the KMP String-Matching Algorithm from a Naive Specification, in the Proceedings of Joint International Conference and Symposium on Logic Programming, Bonn, Germany, Maher M. ed., Logic Programming Series, 1996
  • Maurizio Proietti ed.: Logic Program Synthesis and Transformation -- LOPSTR '95, Lecture Notes in Computer Science, 1048, Springer-Verlag, 1996
  • Lau K.-K., Ornaghi M., Alberto Pettorossi, Maurizio Proietti: Correctness of Logic Program Transformation Based on Existential Termination, in the Proceedings of 1995 International Logic Programming Symposium (ILPS '95), Lloyd J.W. ed., Logic Programming Series, 1995
  • Maurizio Proietti, Alberto Pettorossi: Unfolding-Definition-Folding, in this Order, for Avoiding Unnecessary Variables in Logic Programs, Theoretical Computer Science 142 (1), 89-124, 1995
  • Alberto Pettorossi, Maurizio Proietti: Transformation of Logic Programs: Foundations and Techniques, Journal of Logic Programming 19--20, 261-320, 1994
  • Maurizio Proietti, Alberto Pettorossi: Completeness of Some Transformation Strategies for Avoiding Unnecessary Logical Variables, in the Proceedings of Eleventh International Conference on Logic Programming (ICLP '94), S. Margherita Ligure, Italy, June 13--18, Van Hentenryck P. ed., Logic Programming Series, 1994
  • Maurizio Proietti, Alberto Pettorossi: Synthesis of Programs from Unfold/Fold Proofs, in the Proceedings of Logic Program Synthesis and Transformation, LOPSTR '93, Louvain-la-Neuve, Belgium, Deville Y. ed., Workshops in Computing, 1994
  • Alberto Pettorossi, Pietropoli E., Maurizio Proietti: The Use of the Tupling Strategy in the Development of Parallel Programs, in: Parallel Algorithm Derivation and Program Transformation, Paige R., Reif J., Wachter R. eds., Kluwer Academic Publishers, 111-151, 1993
  • Alberto Pettorossi, Maurizio Proietti: Rules and Strategies for Program Transformation, in: Formal Program Development, IFIP TC2/WG2.1 State-of-the-Art Report, Schuman S., Möller B., Partsch H. eds., Lecture Notes in Computer Science, 755, Springer-Verlag, 263-304, 1993
  • Maurizio Proietti, Alberto Pettorossi: An Abstract Strategy for Transforming Logic Programs, Fundamenta Informaticae 18 (2--4), 267-282, 1993
  • Maurizio Proietti, Alberto Pettorossi: Best-First Strategies for Incremental Transformation of Logic Programs, in the Proceedings of Logic Program Synthesis and Transformation, Manchester 1992, Clement T.P., Lau K.-K. eds., Workshops in Computing, 1993
  • Maurizio Proietti, Alberto Pettorossi: The Loop Absorption and the Generalization Strategies for the Development of Logic Programs and Partial Deduction, Journal of Logic Programming 16 (1--2), 123-161, 1993
  • Maurizio Proietti, Alberto Pettorossi: An Automatic Transformation Strategy for Avoiding Unnecessary Variables in Logic Programs, in the Proceedings of Logic Program Synthesis and Transformation, Manchester 1991, Lau K.-K., Clement T.P. eds., Workshops in Computing, 1992
  • Maurizio Proietti, Alberto Pettorossi: Semantics Preserving Transformation Rules for Prolog, in the Proceedings of ACM Symposium on Partial Evaluation and Semantics Based Program Manipulation, PEPM '91, SIGPLAN Notices, pp. 274-285, 1991
  • Maurizio Proietti, Alberto Pettorossi: Unfolding-Definition-Folding, in this Order, for Avoiding Unnecessary Variables in Logic Programs, in: Third International Symposium on Programming Language Implementation and Logic Programming, PLILP '91, Maluszynski J., Wirsing M. eds., Lecture Notes in Computer Science, 528, Springer-Verlag, 347-358, 1991
  • Maurizio Proietti, Alberto Pettorossi: Construction of Efficient Logic Programs by Loop Absorption and Generalization, in the Proceedings of Second International Workshop on Metaprogramming in Logic, Meta '90, Bruynooghe M. ed., 57-81, 1990
  • Maurizio Proietti, Alberto Pettorossi: Synthesis of Eureka Predicates for Developing Logic Programs, in the Proceedings of Third European Symposium on Programming, ESOP '90, Jones N. ed., Lecture Notes in Computer Science, 432, 1990
  • Alberto Pettorossi, Maurizio Proietti: Decidability Results and Characterization of Strategies for the Development of Logic Programs, in the Proceedings of Sixth International Conference on Logic Programming, Levi G., Martelli M. eds., Logic Programming Series, 1989
  • Alberto Pettorossi, Maurizio Proietti: Importing and Exporting Information in Program Development, in the Proceedings of IFIP TC2 Working Conference on Partial and Mixed Computation, Björner D., Ershov A.P. eds., North Holland, 405-426, 1988
  • Maurizio Proietti: Connections between Partial Maps Categories and Tripos Theory, in the Proceedings of Summer Conference on Category Theory and Computer Science, Pitt D.H., Poigné A., Rydeheard D.E. eds., Lecture Notes in Computer Science, 283, Springer-Verlag, 254-269, 1987
- - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - -