Alberto Pettorossi's publications from DBLP, CiteSeer, ACM, GoogleScholar.
Maurizio Proietti's publications from DBLP, CiteSeer, ACM, GoogleScholar.
For papers not available from this page, please email to maurizio proietti at iasi cnr it
1989 1990 1991 1992 1993 1994 1995 1996 1997 1998 1999 2000 2001 2002 2004 2005 2006 2007 2008 2009 2010 2011 2012 2013 2014 2015 2016 2017 2018
De Angelis, E., Fioravanti, F., Meo, M.C., Pettorossi, A., Proietti, M.: Semantics and Controllability of Time-Aware Business Processes. Fundamenta Informaticae 165(3-4): 205-244 IOS Press, 2019.
De Angelis, E., Fioravanti, F., Pettorossi, A., Proietti, M.: Predicate Pairing for Program Verification. Theory and Practice of Logic Programming, Vol. 18 (2), pp.126-166, Cambridge University Press, 2018.
Emanuele De Angelis, Fabio Fioravanti, Alberto Pettorossi, Maurizio Proietti: Solving Horn Clauses on Inductive Data Types Without Induction. Theory and Practice of Logic Programming 18(3-4): 452-469, Cambridge University Press, 2018.
Emanuele De Angelis, Fabio Fioravanti, Adrián Palacios, Alberto Pettorossi, Maurizio Proietti: Bounded Symbolic Execution for Runtime Error Detection of Erlang Programs. Proceedings 5th Workshop on Horn Clauses for Verification and Synthesis, HCVS 2018, EPTCS Vol. 278, 19-26, 2018.
Emanuele De Angelis, Fabio Fioravanti, Alberto Pettorossi, Maurizio Proietti: Predicate Pairing with Abstraction for Relational Verification. Proceedings of the 27th International Symposium on Logic-Based Program Synthesis and Transformation (LOPSTR 2017). Lecture Notes in Computer Science, vol. 10855, pp. 289–305, Springer, 2018.
De Angelis, E. , Fioravanti, F., Meo, M.C., Pettorossi, A., Proietti, M.: Verifying Controllability of Time-Aware Business Processes. Proceedings of the International Joint Conference on Rules and Reasoning (RuleML+RR 2017), 12-15 July 2017, London, UK. Lecture Notes in Computer Science, vol. 10364, pp. 103–118, Springer, 2017. (Extended version)
De Angelis, E. , Fioravanti, F., Meo, M.C., Pettorossi, A., Proietti, M.: Verification of Time-Aware Business Processes using Constrained Horn Clauses. Proceedings of the 26th International Symposium on Logic-Based Program Synthesis and Transformation (LOPSTR 2016). Lecture Notes in Computer Science, vol. 10184, pp. 38–55, Springer, 2017.
De Angelis, E., Fioravanti, F.,
Pettorossi, A., Proietti, M.: Semantics-based
generation of verification conditions via program specialization.
Science
of Computer Programming, Vol. 147, pp. 78-108. Elsevier,
2017.
[Also available as Technical
Report R. 9-2016, IASI-CNR, Rome, Italy, 2016.]
De Angelis, E., Fioravanti, F., Pettorossi, A., Proietti,
M.: Program Verification Using Constraint Handling Rules and Array
Constraint Generalizations. Fundamenta
Informaticae, Vol. 150, pp. 73-117. IOS Press, 2017.
[Also
available as Technical
Report R. 8-2015, IASI-CNR, Rome, Italy, 2015.]
E. De Angelis, F. Fioravanti, A. Pettorossi, M. Proietti. Horn Clause Transformation for Program Verification. Newsletter of the Association for Logic Programming (ALP), September/October 2016.
E. De Angelis, F. Fioravanti, A. Pettorossi, M. Proietti. Relational Verification through Horn Clause Transformation. Proceedings of the 23rd Static Analysis Symposium (SAS 2016). Lecture Notes in Computer Science (LNCS), vol. 9837, Springer, 2016, pp. 147-169.
E. De Angelis, F. Fioravanti, A. Pettorossi, M. Proietti. Verifying Relational Program Properties by Transforming Constrained Horn Clauses. Proceedings of the 31st Italian Conference on Computational Logic (CILC 2016). CEUR Workshop Proceedings vol. 1645, CEUR-WS.org, 2016, pp.69-85.
De Angelis, E., Fioravanti, F., Pettorossi, Proietti, M.: Removing Unnecessary Variables From Horn Clause Verification Conditions. Proceedings of the 3rd International Workshop on Horn Clauses for Verification and Synthesis, HCVS@ETAPS 2016, Eindhoven, NL, April 3, 2016, EPTCS, Vol. 219, 2016, pp. 49-55.
Fioravanti, F., Proietti, M., Senni, V.: Efficient generation of test data structures using constraint logic programming and program transformation. Journal of Logic and Computation, Vol. 25 (6), pp. 1263-1283, 2015. Oxford University Press.
De Angelis, E., Fioravanti, F., Pettorossi, A., Proietti, M.: A Rule-based Verification Strategy for Array Manipulating Programs. Fundamenta Informaticae 140 (3-4) pp. 329–355. IOS Press Copyright 2015.
De Angelis, E., Fioravanti, F., Pettorossi, A., Proietti, M.: Proving Correctness of Imperative Programs by Linearizing Constrained Horn Clauses. Theory and Practice of Logic Programming, Vol. 15 (4-5), pp. 635-650. Special Issue on the 31st International Conference on Logic Programming (ICLP 2015), Cork, Ireland, 31st August - 4th September, 2015. © Cambridge University Press 2015
De
Angelis, E., Fioravanti, F., Pettorossi, A.,
Proietti,
M.: Semantics-based
generation of verification conditions by program specialization.
17th
International Symposium on Principles and Practice of Declarative
Programming (PPDP 2015)
Siena, Italy, July 14-16, 2015. ACM press, pp. 91-102. Copyright
© 2015 ACM, Inc.
Also
presented at the
30th Italian Conference on Computational Logic (CILC
2015), Genova, Italy, 1st - 3rd July, 2015.
Proietti, M., 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, Volume 8981, Springer, 2015.
De
Angelis, E., Fioravanti, F., Pettorossi, A.,
Proietti,
M.: Proving
Horn Clause Specifications of Imperative Programs. Third
International Workshop on Verification and Program Transformation
(VPT-2015),
co-located with
ETAPS
2015,
April 11th, 2015, London, UK.
Also presented at the
30th Italian Conference on Computational Logic (CILC
2015), Genova, Italy, 1st - 3rd July, 2015.
Proietti, M., Smith, F.: Reasoning on Data-Aware Business Processes with Constraint Logic. In: Rafael Accorsi, Paolo Ceravolo, Barbara Russo (Eds.) Proceedings of the 4th International Symposium on Data-driven Process Discovery and Analysis (SIMPDA 2014), Milan, Italy, November 19-21, 2014. CEUR Workshop Proceedings 1293, pp. 60-75.
Smith, F. and Proietti, M.: BPAL: A Tool for Managing Semantically Enriched Conceptual Process Models. In Paul Cunningham and Miriam Cunningham (Eds) Proceedings of eChallenges (e-2014). IIMC International Information Management Corporation, 2014. ISBN: 978-1-905824-46-5
Smith, F., Proietti, M.: Ontology-based Representation and Reasoning on Process Models: A Logic Programming Approach. CoRR abs/1410.1776 (2014)
Smith, F., Proietti, M.: Behavioral Reasoning on Semantic Business Processes in a Rule-Based Framework. In: Agents and Artificial Intelligence, Communications, Computer and Information Science Series, Volume 449, 2014, Springer, pp. 293-313.
De Angelis, E., Fioravanti, F., Navas, J.A., Proietti, M.: Verification of Programs by Combining Iterated Specialization with Interpolation. In: Proceedings of the 1st International Workshop on Horn Clauses for Verification and Synthesis (HCVS 2014), Vienna, Austria, 17 July, 2014, Electronic Proceedings in Theoretical Computer Science, Vol 169, pp. 3-18.
De Angelis, E., Fioravanti, F., Pettorossi, A., Proietti, M.: Program Verification using Constraint Handling Rules and Array Constraint Generalization. In: A. Lisitsa, A. Nemytykh (Eds.), Proceedings of the 2nd International Workshop on Verification and Program Transformation (VPT), Vienna, Austria, 17-18 July, 2014. Also presented at the 29th Italian Conference on Computational Logic (CILC 2014), Torino, Italy, 16-18 June, 2014.
De Angelis, E., Fioravanti, F., Pettorossi, A., Proietti, M.: Program Verification Via Iterated Specialization. Science of Computer Programming, Volume 95, Part 2, 1 December 2014, Pages 149–175, Selected and extended papers from Partial Evaluation and Program Manipulation 2013.
De Angelis, E., Fioravanti, F., Pettorossi, A., Proietti, M.: VeriMAP: A tool for Verifying Programs through Transformation. (Tool demonstration paper). In: Proceedings of the 20th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2014), 5-13 April 2014, Grenoble, France, Lecture Notes in Computer Science 8413, Springer.
De Angelis, E., Fioravanti, F., Pettorossi, A., Proietti, M.: Verifying Array Programs by Transforming Verification Conditions. In: K.L. McMillan and X. Rival (Eds.), Proceedings of the 15th International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI 2014), San Diego, USA, January 19--21, 2014, Lecture Notes in Computer Science 8318, Springer, pp. 182-202.
Fioravanti, F., Pettorossi, A., Proietti, M., Senni, V.: Proving Theorems by Program Transformation. Fundamenta Informaticae, 127 (1-4) 2013, pp. 115-134.
De Angelis, E., Fioravanti,
F., Pettorossi, A., Proietti, M.: Verification
of Imperative Programs by Constraint Logic Program Transformation.
In: A. Banerjee, O. Danvy, K.-G. Doh, J. Hatcliff
(Eds.): Semantics, Abstract Interpretation, and Reasoning about
Programs: Essays Dedicated to David A. Schmidt on the Occasion of
his Sixtieth Birthday (SAIRP
2013), Manhattan, Kansas, USA, 19-20th September 2013,
Electronic Proceedings in Theoretical Computer Science, Vol 129, pp.
186-210.
Shorter versions appear as:
Verification
of Imperative Programs through Transformation of Constraint Logic
Programs In: A. Lisitsa, A. Nemytykh (eds.),
Proceedings of the First International Workshop on Verification and
Program Transformation (VPT),
Saint Petersburg, Russia, July 13-14, 2013, (EPiC Series, vol. 123),
pp. 30–41.
Verification
of Imperative Programs by Transforming Constraint Logic Programs.
In: Domenico
Cantone and Marianna
Nicolosi Asmundo (eds.), Proceedings
of the 28th Italian Conference on Computational Logic, Catania,
Italy, September 25-27, 2013 (CILC
2013), CEUR, Vol. 1068, pp. 83-98.
Fioravanti, F., Pettorossi, A., Proietti, M., Senni, V.: Controlling Polyvariance for Specialization-based Verification. Fundamenta Informaticae, Vol. 124 (2013), Special Issue on CILC-11, pp. 483–502, http://dx.doi.org/10.3233/FI-2013-845, IOS Press.
Fioravanti, F., Pettorossi, A., Proietti, M., Senni, V.: Generalization Strategies for the Verification of Infinite State Systems. Theory and Practice of Logic Programming. Wolfgang Faber and Nicola Leone (Eds.), Volume 13 / Special Issue 02 (25th GULP annual conference) / March 2013, pp. 175-199, http://dx.doi.org/10.1017/S1471068411000627. Copyright © Cambridge University Press.
De Angelis, E., Fioravanti, F., Pettorossi, A., Proietti, M.: Verifying Programs via Iterated Specialization. In: Proceedings of the ACM SIGPLAN Workshop on Partial Evaluation and Program Manipulation (PEPM'13), Rome, Italy, January 21-22, 2013, ACM Press, pp. 43-52. [An extended, revised version appears as: Technical Report R.11-2013, IASI-CNR, Rome, Italy, 2013.] [An older version appears as: Technical Report R.22-2012, IASI-CNR, Rome, Italy, 2012.]
Fabrizio Smith, Dario De Sanctis, Maurizio Proietti: BPAL: A Platform for Managing Business Process Knowledge Bases via Logic Programming. Proceedings of the 28th Italian Conference on Computational Logic, Catania, Italy, September 25-27, 2013 (CILC 2013), CEUR, Vol. 1068, pp. 247-251.
Diamantini, C., Potena D., Proietti, M., Smith, M., Storti, E., Taglino, F.: A Semantic Framework for Knowledge Management in Virtual Innovation Factories, International Journal of Information System Modeling and Design, 4 (4), 70-92, October-December 2013.
Smith, F., Proietti, M.: Rule-Based Behavioural Reasoning on Semantic Business Processes. In: J. Filipe, A. Fred (Eds.) Proceedings of the 5th International Conference on Agents and Artificial Intelligence (ICAART'13), Barcelona, Spain, February 15-18, 2013, SCITEPRESS, pp. 130-143. [Technical Report R.21, IASI-CNR, Rome, Italy, 2012.]
De Angelis, E., Pettorossi, A., Proietti, M.: Synthesizing Concurrent Programs using Answer Set Programming Fundamenta Informaticae, Special Issue on Concurrency, Specification, and Programming CS&P 2011, Vol. 120, 3-4 (2012), pp. 205-229. [Extended version: Technical Report R.19, IASI-CNR, Rome, Italy, 2012.]
De Angelis, E., Fioravanti, F., Pettorossi, A., Proietti, M.: Specialization with Constrained Generalization for Software Model Checking. In: E. Albert (Ed.), Proceedings of the 22nd International Symposium on Logic-Based Program Synthesis and Transformation (LOPSTR 2012), Leuven, Belgium, September 18-20, 2012, Lecture Notes in Computer Science 7844, pp. 51-70, Springer, 2013.
Smith, F., Missikoff, M., Proietti, M.: Ontology-Based Querying of Composite Services. In: C.A. Ardagna, E. Damiani, L.A. Maciaszek, M. Missikoff, and M. Parkin (Eds.) Business System Management and Engineering, From Open Issues to Applications, LNCS 7350, pp. 159–180, Springer, 2012.
Fioravanti, F., Pettorossi, A., Proietti, M., Senni, V.: Improving Reachability Analysis of Infinite State Systems by Specialization. Fundamenta Informaticae Vol. 119, N.3-4 (2012), pp. 281–300. DOI 10.3233/FI-2012-720, IOS Press.
Pettorossi, A., Proietti, M., Senni, V.: Constraint-Based Correctness Proofs for Logic Program Transformations. Formal Aspects of Computing (2012) 24: 569-594. [Technical Report R.24, IASI-CNR, Rome, Italy, 2011.]
De Angelis, E., Fioravanti, F., Pettorossi, A., Proietti, M.: Software Model Checking by Program Specialization. In: F. Lisi (Ed.), Proceedings of the 27th Italian Conference on Computational Logic, CILC-2012, 6-7 June, 2012, Rome, Italy, CEUR-WS, Vol-857, urn:nbn:de:0074-857-8, pp. 89-103.
Fioravanti, F., Pettorossi, A., Proietti, M., Senni, V.: A Constraint-Based Transformation for Verifying Infinite State Systems. Technical Report R.23, IASI-CNR, Rome, Italy, 2011.
De Angelis, E., Pettorossi, A., Proietti, M.: Synthesizing Concurrent Programs using Answer Set Programming In: M. Szczuka, L. Czaja , A. Skowron, and M. Kacprzak (Eds.), Proceedings of the International Workshop on Concurrency, Specification, and Programming (CS&P 2011), September 28-30, 2011, Pułtusk, Poland, pp. 85-98. (Also presented at th 26th Italian Conference on Computational Logic, CILC-2011, 31 August - 2 September 2011, Pescara, Italy.
Fioravanti, F., Pettorossi, A., Proietti, M., Senni, V.: Reachability Analysis Via Specialization of Constraint Logic Programs. ALP Newsletter, September 2011.
Fioravanti, F., Pettorossi, A., Proietti, M., Senni, V.: Improving Reachability Analysis of Infinite State Systems by Specialization In: G. Delzanno and I. Potapov (Eds.), Proceedings of the 5th International Workshop on Reachability Problems (RP 2011), September 28-30, 2011, Genova, Italy, LNCS 6945, Springer 2011, pp. 165-179. (Also presented at the International Workshop on on Concurrency, Specification, and Programming (CS&P 2011), September 28-30, 2011, Pułtusk, Poland, pp. 85-98.)
Fioravanti, F., Pettorossi, A., Proietti, M., Senni, V.: Controlling Polyvariance for Specialization-based Verification. In: F. Fioravanti (Ed.), Proceedings of the 26th Italian Conference on Computational Logic, CILC-2011, 31 August - 2 September 2011, Pescara, Italy, pp. 179-197. [CEUR-WS, Vol-810 urn:nbn:de:0074-810-0, ISSN 1613-0073.]
Missikoff, M., Proietti, M., Smith, F.: Querying Semantically Enriched Business Processes. In: Hameurlain et al. (Eds), Proceedings of the 22nd International Conference on Database and Expert Systems Applications (DEXA 2011), Toulouse, France, August 29 - September 2, 2011, LNCS 6861, pp. 294–302, Springer, 2011.
Fioravanti, F., Pettorossi, A., Proietti, M., Senni, V.: Using Real Relaxations During Program Specialization In: G. Vidal (Ed.), Proceedings of the 21st International Symposium on Logic-Based Program Synthesis and Transformation (LOPSTR 2011), July 18-20, 2011, Odense, Denmark, Lecture Notes in Computer Science 7225, pp. 106-122, Springer, 2012.
Missikoff, M., Proietti, M., Smith, F.: Querying Business Processes and Ontologies in a Logic Programming Environment. In: G. Mecca, S. Greco (Eds.) Proceedings of the 19th Italian Symposium on Advanced Database Systems (SEBD 2011), June 26th - 29th, 2011, Maratea, Italy, pp. 303-310.
Fioravanti, F., Pettorossi, A., Proietti, M., Senni, V.: Program Transformation for Development, Verification, and Synthesis of Programs In: M. Baldoni and C. Baroglio, editors. Special section: A Journey in Computational Logic in Italy – Dedicated to Prof. Alberto Martelli. Intelligenza Artificiale, Vol. 5, N.1, pp. 119-125, 2011.
Missikoff, M., Proietti, M., Smith, F.: Reasoning on Business Processes and Ontologies in a Logic Programming Environment. In: M. Missikoff and P. Velardi (Eds.), Proceedings of the Third Interop-Vlab.It Workshop on Enterprise Interoperability (INVIT 2010), Naples, Italy, October 9, 2010, pp. 17-21. [CEUR-WS, Vol-653, urn:nbn:de:0074-653-7, ISSN 1613-0073.]
De Nicola, A., Missikoff, M., Proietti, M., Smith, F.: An Open Platform for Business Process Modeling and Verification. In: P. G. Bringas, A. Hameurlain, and G. Quirchmayr (Eds.), 21st International Conference on Database and Expert Systems Applications (DEXA 2010), Bilbao, Spain, University of Deusto, 30 August - 3 September 2010, LNCS 6261, pp. 76--90, Springer, 2010.
Fioravanti, F., Pettorossi, A., Proietti, M., Senni, V.: Program Specialization for Verifying Infinite State Systems: An Experimental Evaluation. In: M. Alpuente (Ed.): Proceedings of the 20th International Symposium on Logic-Based Synthesis and Transformation (LOPSTR 2010), July 23-25, 2010, Hagenberg, Austria, Lecture Notes in Computer Science Vol. 6564, pp. 164-183, Springer, 2011.
Pettorossi, A., Proietti, M., Senni, V.: A Transformation Strategy for Verifying Logic Programs on Infinite Lists. In: Wolfgang Faber and Nicola Leone (Eds.), Proceedings of the 25th Italian Conference on Computational Logic (CILC'10), University of Calabria, Rende, Italy, July 7-9, 2010. [CEUR-WS, Vol-598, urn:nbn:de:0074-598-1, ISSN 1613-0073.
Fioravanti, F., Pettorossi, A., Proietti, M., Senni, V.: Generalization Strategies for the Verification of Infinite State Systems. In: Wolfgang Faber and Nicola Leone (Eds.), Proceedings of the 25th Italian Conference on Computational Logic (CILC'10), University of Calabria, Rende, Italy, July 7-9, 2010. [CEUR-WS, Vol-598, urn:nbn:de:0074-598-1, ISSN 1613-0073.]
Missikoff, M., Proietti, M., Smith, F.: A Business Process Knowledge Base for Composite Services Development. In: Proceedings of International Workshop on Business System Management and Engineering (BSME 2010), Malaga, 28 June 2010.
De Nicola, A., Missikoff, M., Proietti, M., Smith, F.: A Logic-Based Method for Business Process Knowledge Base Management. In: S. Bergamaschi, S. Lodi, R. Martoglia, C. Sartori (Eds.), Proceedings of the 18th Italian Symposium on Advanced Database Systems (SEBD 2010), June 20-23, 2010, Rimini, Italy, pp. 170-181.
Pettorossi, A., Proietti, M., Senni, V.: Transformations of Logic Programs on Infinite Lists. Theory and Practice of Logic Programming, Vol. 10 (4-6), Special Issue on the 26th International Conference on Logic Programming, Edinburgh, Scotland, UK, July 16-19, 2010, pp. 383-399. [Technical Report R. 10-04, IASI-CNR, Rome, Italy, 2010.]
Pettorossi, A., Proietti, M., Senni, V.: The Transformational Approach to Program Development. In: A. Dovier and E. Pontelli (Eds.) A 25 Year Perspective on Logic Programming (Achievements of the Italian Association for Logic Programming, GULP), Lecture Notes in Computer Science Vol. 6125, pp. 112-135, Springer, 2010. [Technical Report R. 09-06, IASI-CNR, Rome, Italy, 2009.]
Senni, V., Pettorossi, A., Proietti, M.: A Folding Rule for Eliminating Existential Variables from Constraint Logic Programs. Fundamenta Informaticae 96 (2009) 373-393. [Technical Report R. 08-03, IASI-CNR, Rome, Italy, 2008, revised January 2010.]
Pettorossi, A., Proietti, M., Senni, V.: Deciding Full Branching Time Logic by Program Transformation. In: Danny De Schreye (Ed.) 19th International Symposium on Logic-Based Synthesis and Transformation (LOPSTR '09), September 9-11, 2009, Coimbra, Portugal, LNCS 6037, pp. 5--21. Springer, Heidelberg (2010). [Technical Report R. 09-04, IASI-CNR, Rome, Italy, 2009.]
Pettorossi, A., Proietti, M., Senni, V.: Transformational Verification of Linear Temporal Logic. 24th Italian Conference on Computational Logic (CILC'09), June 24-26, 2009, Ferrara, Italy. [Technical Report R. 09-03, IASI-CNR, Rome, Italy, 2009.]
Senni, V., Pettorossi, A., Proietti, M.: A Folding Algorithm for Eliminating Existential Variables from Constraint Logic Programs. In: M. Garcia de la Banda and E. Pontelli (Eds.): Proceedings of the 24th International Conference on Logic Programming (ICLP'08), December 9-13, 2008, Udine, Italy. Lecture Notes in Computer Science 5366, Springer 2008, pp. 284-300. [Revised version]
Senni, V., Pettorossi, A., Proietti, M.: Folding Transformation Rules for Constraint Logic Programs. Presented at the 2008 Italian Conference on Computational Logic (CILC 2008), 10-12 July, 2008, Perugia, Italy. [Revised version]
Pettorossi, A., Proietti, M., Senni, V.: Program Transformation for Development, Verification, and Synthesis of Software. In: M. Baldoni and C. Baroglio, editors. Il Milione. Viaggio nella Logica Computazionale in Italia. Technical Report of Dipartimento di Informatica, Università degli Studi di Torino, RT 110/08, June 2008, pp. 7-14.
Pettorossi, A., Proietti, M.: Totally Correct Logic Program Transformations Via Well-Founded Annotations. Higher-Order and Symbolic Computation, Volume 21, Numbers 1-2 / June, 2008, pp. 193-235. Also available as: Technical Report R.639, IASI-CNR, Rome, Italy, February 2006. (Revised version of the PEPM'04 paper.) The original publication is available at www.springerlink.com.
Olivier Danvy, Fritz Henglein, Harry Mairson, and Alberto Pettorossi (Eds.): Automatic Program Development, A Tribute to Robert Paige, Springer, 2008.
Fioravanti, F., Pettorossi, A., Proietti, M.: Verifying Infinite State Systems by Specializing Constraint Logic Programs. Technical Report R.657, IASI - CNR, Roma, Italy, 2007.
Pettorossi, A., Proietti, M., Senni, V.: Automatic Correctness Proofs for Logic Program TransformationsIn: V. Dahl and I. Niemelä (Eds.): Proceedings of the 23rd International Conference on Logic Programming (ICLP '07), September 8-13, 2007, Porto, Portugal. Lecture Notes in Computer Science 4670, Springer, 2007, pp. 364-379. [Also presented at the 2007 Italian Conference on Computational Logic (CILC 2007), 21-22 June, 2007, Messina, Italy.]
Pettorossi, A., Proietti, M., Senni, V.: Proving Properties of Constraint Logic Programs by Eliminating Existential Variables. In: S. Etalle and M. Truszczyński (Eds.): Proceedings of the Twenty Second International Conference on Logic Programming (ICLP '06), August 17-20, 2006, Seattle, Washington, USA. Lecture Notes in Computer Science 4079, Springer, 2006, pp. 179-195. An extended version of this paper appears as: Research Report 07.62, Dipartimento di Informatica, Sistemi e Produzione, University of Rome Tor Vergata, Rome, Italy, February 2007.
Also presented at the 2006 Italian Conference on Computational Logic (CILC 2006), 26-27 June, 2006, Bari, Italy.
Pettorossi, A., Proietti, M., Senni, V.: Proofs of Program Properties via Unfold/Fold Transformations of Constraint Logic Programs (Abstract) In J. R. Cordy, R. Lämmel, A. Winter (Eds.) Proceedings of the Dagstuhl Seminar 05161, Transformation Techniques in Software Engineering, 17.04. - 22.04.2005.
Pettorossi, A., Proietti, M., Senni, V.: Transformational Verification of Parameterized Protocols Using Array Formulas, In Patricia M. Hill (Ed.): Logic Based Program Synthesis and Transformation, 15th International Symposium, LOPSTR 2005, Imperial College, London, UK, September 7-9, 2005, Revised Selected Papers. Lecture Notes in Computer Science 3901, Springer 2006, pp. 23-43.
Pettorossi, A., Proietti, M., Senni, V.: Verifying parameterized protocols by transforming stratified logic programs. Online Proceedings of the Italian Annual Meeting on Computational Logic (CILC'05), June 21-22, 2005, Roma, Italy.
Pettorossi, A., Proietti, M., Renault, S.: Derivation of Efficient Logic Programs by Specialization and Reduction of Nondeterminism (revised May 2005). Higher-Order and Symbolic Computation, 18 (1-2), Special Issue in memory of Bob Paige, 2005, pp. 121-210. Also published as a chapter of: Olivier Danvy, Harry Mairson, Fritz Henglein and Alberto Pettorossi (Eds.): Automatic Program Development, A Tribute to Robert Paige, Springer, 2008, pp. 130-177.
Fioravanti, F., Pettorossi, A., Proietti, M.: Automatic Proofs of Protocols via Program Transformation. In: Dunin-Keplicz, B.; Jankowski, A.; Skowron, A.; Szczuka, M. (Eds.): Monitoring, Security, and Rescue Techniques in Multiagent Systems, Advances in Soft Computing Series, Springer, 2005, pp. 99-116. (Extended and revised version of a paper presented at the International Workshop MSRAS '04, June 7-9, 2004, Płock, Poland)
Pettorossi, A., Proietti, M.: A Theory of Totally Correct Logic Program Transformations. Proceedings of the ACM Symposium on Partial Evaluation and Semantics-Based Program Manipulation (PEPM '04), August 24-26, 2004, Verona, Italy, pp. 159-168.
Pettorossi, A., Proietti, M.: Totally Correct Logic Program Transformations Using Well-Founded Annotations. In: Elio Panegai and Gianfranco Rossi (Eds.) Proceedings of the Italian Conference on Computational Logic (CILC '04), June16-17, 2004, Parma, Italy, pp. 325-329.
Fioravanti, F., Pettorossi, A., Proietti, M.: Transformation Rules for Locally Stratified Constraint Logic Programs. Chapter of: Maurice Bruynooghe and Kung-Kiu Lau (Eds.) Program Development in Computational Logic, Lecture Notes in Computer Science 3049, Springer, 2004, pp. 291-339.
Pettorossi, A., Proietti, M.: Transformations of Logic Programs with Goals as Arguments. Full version of a paper that appears in Theory and Practice of Logic Programming, 4 (4) July 2004, pp. 495-537.
Fioravanti, F., Pettorossi, A., Proietti, M.: Specialization with Clause Splitting For Deriving Deterministic Constraint Logic Programs. Proceedings of the IEEE International Conference on Systems, Man, and Cybernetics (SMC'02), 6 - 9 October, 2002, Hammamet, Tunisia, IEEE Computer Society Press, 2002, Volume 1, pp. 188-193 (Invited paper).
Fioravanti, F., Pettorossi, A., Proietti, M.: A Specialization Technique For Deriving Deterministic Constraint Logic Programs and Its Application to Pattern Matching. In: J.J. Moreno-Navarro and J. Mariño-Carballo (eds.) Proceedings of AGP'02, 2002 JOINT CONFERENCE ON DECLARATIVE PROGRAMMING, Madrid, Spain,16 - 18 September 2002, pp. 241-257.
Fioravanti, F., Pettorossi, A., Proietti, M.: Combining Logic Programs and Monadic Second Order Logics by Program Transformation. Long version of a paper that appears in: M. Leuschel (ed.) Proceedings of LOPSTR'02, Twelfth International Workshop on Logic-based Program Development and Transformation, Madrid, Spain, 17-20 Sept. 2002. Lecture Notes in Computer Science 2664. Springer-Verlag Berlin Heidelberg, 2003, pp. 160-181.
Pettorossi, A., Proietti, M.: The List Introduction Strategy for the Derivation of Logic Programs. Formal Aspects of Computing (2002) 13: 233-251, (Special Issue in Honour of Rod Burstall).
Pettorossi, A., Proietti, M.: Program Derivation = Rules + Strategies. In: A. Kakas and F. Sadri (eds.) Computational Logic: Logic Programming and Beyond (Essays in Honour of Robert A. Kowalski - Part I), Lecture Notes in Artificial Intelligence 2407, Springer, 2002, pp. 273-309.
Pettorossi, A. (ed.): Proceedings of the Eleventh International Workshop on Logic-based Program Synthesis and Transformation. (LOPSTR '01) Paphos, Cyprus, November 28-30, 2001, Lecture Notes in Computer Science 2372, Springer, 2002. A few free copies of this book are available from the editor
Fioravanti, F., Pettorossi, A., Proietti, M.: Verification of Sets of Infinite State Systems Using Program Transformation. In: A. Pettorossi (ed.) Proceedings of LOPSTR '01, Eleventh International Workshop on Logic-based Program Synthesis and Transformation, Paphos, Cyprus, November 28-30, 2001, Lecture Notes in Computer Science 2372, Springer, 2002, pp. 111-128. Also available as: Technical Report R.557, IASI - CNR, Roma, Italy.
Fioravanti, F., Pettorossi, A., Proietti, M.: Verifying CTL Properties of Infinite State Systems by Specializing Constraint Logic Programs. M. Leuschel, A. Podelski, C.R. Ramakrishnan, U. Ultes-Nitsche (editors) Proceedings of the Second ACM-Sigplan International Workshop on Verification and Computational Logic, VCL'2001, Florence, Italy, September 4, 2001, pp. 85-96. Revised Version: Technical Report R.544, IASI - CNR, Roma, Italy.
Pettorossi, A., Proietti, M.: Transformation Rules for a Higher Order Logic Programming Language. Technical Report R.525, IASI - CNR, Roma, Italy May 2000. Revised version (published on TPLP): Transformations of Logic Programs with Goals as Arguments.
Pettorossi, A., Proietti, M.: Automatic Derivaton of Logic Programs by Transformation. Lecture Notes for the 2000 European Summer School on Logic, Language, and Information (ESSLLI'2000), Birmingham, U.K. 6-18 August 2000.
Fioravanti, F., Pettorossi, A., Proietti, M.: Automated Strategies for Specializing Constraint Logic Programs. In: Kung-Kiu Lau (ed.) Proceedings of LOPSTR 2000, Tenth International Workshop on Logic-based Program Synthesis and Transformation, London, UK, 24-28 July, 2000, Lecture Notes in Computer Science 2042, Springer, 2001, pp. 125-146.
Pettorossi, A., Proietti, M.: Perfect Model Checking via Unfold/Fold Tansformations. Technical Report R.513, IASI - CNR, Roma, Italy November 1999 (revised September 2000). Shorter version in: J.W. Lloyd et al. (eds.) Proceedings of the First International Conference on Computational Logic ( CL 2000 ), London, UK, July 24-28, 2000, Lecture Notes in Artificial Intelligence 1861, Springer, 2000, pp. 613-628.
Fioravanti, F., Pettorossi, A., Proietti, M.: Rules and Strategies for Contextual Specialization of Constraint Logic Programs. In: M. Leuschel (ed.) Proceedings of the ICLP'99 Workshop on Optimization and Implementation of Declarative Programming Languages (WOID'99), Las Cruces, New Mexico, USA, Dec.2-3, 1999, Electronic Notes in Theoretical Computer Science 30 No. 2 (2000).
Proietti, M. and Pettorossi, A.: Transforming Inductive Definitions. In: D. De Schreye (ed.) Proceedings of the 16th International Conference on Logic Programming (ICLP'99), Las Cruces, New Mexico, USA, Nov. 29 - Dec. 4, 1999, MIT Press, pp. 486-499.
Pettorossi, A., Proietti, M.: Transformation Rules for Logic Programs with Goals as Arguments. In: A. Bossi (ed.) Proceedings of the Nineth International Workshop on Logic-based Program Synthesis and Transformation (LOPSTR`99), Venezia, Italy, September 22-24, 1999, Lecture Notes in Computer Science 1817, Springer, 2000, pp. 177-196.
Fioravanti, F., Proietti, M.: Contextual Specialization of Constraint Logic Programs. In: M.C. Meo, M. Vilares Ferro (eds.) Proceedings of the Joint Conference on Declarative Programming (Appia-Gulp-Prode'99), L'Aquila, Italy, September, 6-9, 1999, pp. 455-469.
Pettorossi, A., Proietti, M.: Synthesis and Transformation of Logic Programs Using Unfold/Fold Proofs. Journal of Logic Programming, Vol. 41, N. 2&3, November 1999, pp. 197-230.
Renault, S., Pettorossi, A., Proietti, M.: Design, Implementation, and Use of the MAP Transformation System. R. 491, IASI-CNR, Roma, Italy, December 1998.
Pettorossi, A., Proietti, M.: The List Introduction Strategy for the Automatic Derivation of Programs. R. 472, IASI-CNR, Roma, Italy, October 1998.
Pettorossi, A., Proietti, M.: Program Specialization via Algorithmic Unfold/Fold Transformations. 1998 Symposium on Partial Evaluation, ACM Computing Surveys, Vol. 30, No. 3es (Sept 1998), Pages 6-es.
Pettorossi, A. and Proietti, M.: Transformation of Logic Programs. Chapter of: D. M. Gabbay, C. J. Hogger, and J. A. Robinson (eds.), Handbook of Logic in Artificial Intelligence and Logic Programming, Vol. 5, Oxford University Press, 1998, pp. 697-787.
Pettorossi, A., Proietti, M.: Program Derivation via List Introduction. In: R. Bird and L.G.L.T. Meertens (Eds.) Proceedings of the IFIP TC2 Working Conference on Algorithmic Languages and Calculi, Le Bischenberg, France, February 17-21, 1997, Chapman & Hall, 1997, pp. 296-323.
Pettorossi, A., Proietti, M.: Flexible Continuations in Logic Programs via Unfold/Fold Transformations and Goal Generalization. In: O. Danvy (Ed.) Proceedings of the Second ACM Sigplan Workshop on Continuations (CW'97) La Sorbonne, Paris, France, January 14, 1997, BRICS Notes Series, N6-93-13 Aahrus, Denmark (December 1996) pp. 9.1-9.22.
· Pettorossi, A., Proietti, M., Renault, S.: Reducing Nondeterminism while Specializing Logic Programs 24th ACM Symposium on Principles of Programming Languages (POPL'97) La Sorbonne, Paris, France, January 15-17, 1997, ACM Press, 1997, pp. 414-427.
Pettorossi, A. and Proietti, M.: Developing Correct and Efficient Logic Programs by Transformation Knowledge Engineering Review, Vol. 11, No. 4. (December 1996), pp. 347-360.
Pettorossi, A. and Proietti, M.: Future Directions in Program Transformation. Position Statement at the Workshop on Strategic Directions in Computing Research, MIT, Cambridge, MA, USA, June 14-15, 1996, ACM Sigplan Notices 32/1 (Jan 1997) pp. 99-102. Also published in: ACM Computing Surveys, 28 (4es) (December 1996), pp. 171-es
Pettorossi, A., Proietti, M., and Renault, S.: Enhancing Partial Deduction via Unfold/Fold Rules. In: J. Gallagher (Ed.) Logic Program Synthesis and Transformation. Proceedings of the 6th International Workshop, LOPSTR'96, Stockholm, Sweden, August 1996, Lecture Notes in Computer Science 1207, Springer, 1997.
Pettorossi, A. and Proietti, M.: A Comparative Revisitation of Some Program Transformation Strategies. In: O. Danvy, R. Glueck, and T. Thiemann (eds.), Partial Evaluation, International Seminar, Dagstuhl Castle, Germany, February 1996, Lecture Notes in Computer Science 1110, Springer, 1996, pp. 355-385.
Pettorossi, A. and Proietti, M.: A Theory of Logic Program Specialization and Generalization for Dealing with Input Data Properties. In: O. Danvy, R. Glueck, and T. Thiemann (eds.), Partial Evaluation, International Seminar, Dagstuhl Castle, Germany, February 1996, Lecture Notes in Computer Science 1110, Springer, 1996 pp. 386-408.
Pettorossi, A. and Proietti, M.: Rules and Strategies for Transforming Functional and Logic Programs. ACM Computing Surveys, Vol. 28, No. 2, June 1996, pp. 360-414. Also available as: Technical Report, R. 423, IASI-CNR, December 1995.
Proietti, M. (ed.): Logic Program Synthesis and Transformation. Proceedings of the Fifth International Workshop, LOPSTR'95, Utrecht, The Netherlands, September 20-22, 1995, Lecture Notes in Computer Science Vol. 1048, Springer, 1996. A few free copies of this book are available from the editor
Lau, K.-K., Ornaghi, M., Pettorossi, A., and Proietti, M.: Correctness of Logic Program Transformation Based on Existential Termination. In: J. W. Lloyd (ed.) Proceedings of the 1995 International Logic Programming Symposium (ILPS'95) Portland, Oregon (U.S.A.) December 4-7, MIT Press, 1995, pp. 480-494.
Proietti, M. and Pettorossi, A.: Unfolding-Definition-Folding, in this order, for Avoiding Unnecessary Variables in Logic Programs. Theoretical Computer Science 142 (1) 1995, 89-124.
Proietti, M. and Pettorossi, A.: Total Correctness of a Goal Replacement Rule based on the Unfold/Fold Proof Method. In: M. Alpuente, R. Barbuti, and I. Ramos (eds.), Proceedings of the 1994 Joint Conference on Declarative Programming (Gulp - Prode '94) Peniscola, Spain, September 19-22, 1994, Vol. 1, pp. 203-217.
Proietti, M. and Pettorossi, A.: Completeness of Some Transformation Strategies for Avoiding Unnecessary Logical Variables. In: P. Van Hentenryck (ed.) Proceedings of the Eleventh International Conference on Logic Programming (ICLP '94), S.Margherita Ligure, Italy, June 13-18, The MIT Press, 1994, pp. 714-729.
Pettorossi, A. and Proietti, M.: Transformation of Logic Programs: Foundations and Techniques. Journal of Logic Programming 1994: 19, 20: 261-320. Errata Corrige.
Proietti, M. and Pettorossi, A.: Synthesis of Programs from Unfold/Fold Proofs. In: Y. Deville (ed.) Logic Program Synthesis and Transformation, LOPSTR '93, Louvain-la-Neuve, Belgium, 1993, Springer-Verlag, Workshops in Computing Series, 1994, pp. 141-158.
Pettorossi, A., Pietropoli, E., and Proietti, M.: The Use of the Tupling Strategy in the Development of Parallel Programs. In: Paige, R., Reif, J., and Wachter, R. (Eds.) Parallel Algorithm Derivation and Program Transformation, Kluwer Academic Publishers, 1993, pp. 111-151.
Proietti, M. and Pettorossi, A.: An Abstract Strategy for Transforming Logic Programs. Fundamenta Informaticae, Vol. 18, Numbers 2, 3, 4, February-April 1993, pp. 267-286.
Proietti, M. and Pettorossi, A.: The Loop Absorption and the Generalization Strategies for the Development of Logic Programs and Partial Deduction. Journal of Logic Programming, 1993:16:123-161.
Pettorossi, A. (Ed.): Meta-Programming in Logic. Proceedings of the Third International Workshop, Meta-92, Uppsala, Sweden, June 1992, Lecture Notes in Computer Science 649, Springer-Verlag, 1992.
Proietti, M. and Pettorossi, A.: Best-First Strategies for Incremental Transformation of Logic Programs. Proceedings Logic Program Synthesis and Transformation, LOPSTR'92. K.-K. Lau and T.P. Clement (eds.), Workshops in Computing Series, Springer Verlag (1993), pp. 82-98.
Proietti, M. and Pettorossi, A.: Semantics Preserving Transformation Rules for Prolog. Proceedings ACM Symposium on Partial Evaluation and Semantics Based Program Manipulation, (PEPM '91) Yale University, New Haven, U.S.A. (1991), pp. 274-284.
Proietti, M. and Pettorossi, A.: Construction of Efficient Logic Programs by Loop Absorption and Generalization. Proceedings Meta'90 (M. Bruynooghe, ed.), Leuven, Belgium (1990), 57-81.
Proietti, M. and Pettorossi, A.: Synthesis of Eureka Predicates for Developing Logic Programs. Proceedings ESOP '90 (N. Jones, ed.), Copenhagen, Lecture Notes in Computer Science 432, (1990), 306-325.
Pettorossi, A. and Proietti, M.: Decidability Results and Characterization of Strategies for the Development of Logic Programs. Proceedings 6th International Conference on Logic Programming, (G.Levi and M. Martelli, eds.), Lisbon, Portugal, 19-23 June, 1989, MIT Press, pp. 539-553.