2019
E. De Angelis, F. Fioravanti, A. Pettorossi, M. Proietti. Proving Properties of Sorting Algorithms: A Case Study in Horn Clause Verification. 6th Workshop on Horn Clauses for Verification and Synthesis (HCVS 2019), Prague, Czech Republic, 7 April, 2019.
2017
E. De Angelis, F. Fioravanti, M.C. Meo, A. Pettorossi, M. Proietti. Semantics and Controllability of Time-Aware Business Processes. Invited talk at Concurrency Specification and Programming (CS&P 2017), Special session in memoriam of Helena Rasiowa, Warsaw, Poland, 25 Sept. 2017 (paper)
E.
De Angelis, F. Fioravanti, M.C. Meo, A. Pettorossi, M.
Proietti. Verifying
Controllability of Time-Aware Business Processes using Constrained
Horn Clauses.
International
Joint Conference on Rules and Reasoning (RuleML+RR
2017), 12-15 July 2017, London, UK. (paper)
Short
version presented at the 32nd
Italian
Conference on Computational Logic (CILC
2017), 26-28 September 2017, Naples, Italy.
2016
E. De Angelis, F. Fioravanti, M.C. Meo, A. Pettorossi, M. Proietti. Verification of Time-Aware Business Processes using Constrained Horn Clauses. 26th International Symposium on Logic-Based Program Synthesis and Transformation (LOPSTR 2016), Edinburgh, UK, 6-8 September, 2016.
E. De Angelis, F. Fioravanti, A. Pettorossi, M. Proietti. Relational Verification through Horn Clause Transformation. 23rd Static Analysis Symposium (SAS 2016), Edinburgh, UK, 6-8 September, 2016.
E. De Angelis, F. Fioravanti, A. Pettorossi, M. Proietti. Verifying Relational Program Properties by Transforming Constrained Horn Clauses. 31st Italian Conference on Computational Logic (CILC 2016), Milan, Italy, 20-22 June, 2016.
E. De Angelis, F. Fioravanti, A. Pettorossi, M. Proietti: Removing Unnecessary Variables From Horn Clause Verification Conditions. 3rd International Workshop on Horn Clauses for Verification and Synthesis, HCVS@ETAPS 2016, Eindhoven, NL, April 3, 2016.
M. Proietti: Transforming Constrained Horn Clauses for Program Verification. 3rd International Workshop on Horn Clauses for Verification and Synthesis, HCVS@ETAPS 2016, Eindhoven, NL, April 3, 2016 (Invited Talk).
2015
De Angelis, E., Fioravanti, F., Pettorossi, A., Proietti, M.: Proving Correctness of Imperative Programs by Linearization of Constrained Horn Clauses. 31st International Conference on Logic Programming (ICLP 2015), Cork, Ireland, 31 Aug. - 4 Sept. 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.
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.
2014
De Angelis, E., Fioravanti, F., Pettorossi, A., Proietti, M.: Program Verification using Constraint Handling Rules and Array Constraint Generalization. Workshop su "Metodi Dichiarativi nella Verifica di Sistemi Parametrici", Dipartimento di Matematica, Università di Milano, 25-26 Settembre 2014.
De Angelis, E., Fioravanti, F., Pettorossi, A., Proietti, M.: Verification of Imperative Programs Through Transformation of Constraint Logic Programs. Workshop su "Metodi Dichiarativi nella Verifica di Sistemi Parametrici", Dipartimento di Matematica, Università di Milano, 25-26 Settembre 2014.
De Angelis, E., Fioravanti, F., Pettorossi, A., Proietti, M.: Verification of Array Manipulating Programs: A Transformational Approach. First International Workshop on Parameterized Verification (PV@CONCUR), Rome, Itay, September 6, 2014.
De Angelis, E., Fioravanti, F., Pettorossi, A., Proietti, M.: Program Verification using Constraint Handling Rules and Array Constraint Generalization. 2nd International Workshop on Verification and Program Transformation (VPT), Vienna, Austria, 17-18 July, 2014.
De Angelis, E., Fioravanti, F., Pettorossi, A., Proietti, M.: Verification of Imperative Programs Through Transformation of Constraint Logic Programs. LSV-ENS, Cachan, France, Feb 12, 2014.
De Angelis, E., Fioravanti, F., Pettorossi, A., Proietti, M.: Verifying Array Programs by Transforming Verification Conditions, 15th International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI 2014), San Diego, USA, January 19--21, 2014.
Fioravanti, F., Pettorossi, A., Proietti, M., Senni, V.: Improving Reachability Analysis of Infinite State Systems by Specialization. International Workshop on Reachability Problems, (RP 2011), 28-30 September 2011, Genoa, Italy.
Fioravanti, F., Pettorossi, A., Proietti, M., Senni, V.: Improving Reachability Analysis of Infinite State Systems by Specialization. International Workshop on Concurrency, Specification and Programming, (CS&P 2011), 28-30 September 2011, Pułtusk, Poland.
Fioravanti, F., Pettorossi, A., Proietti, M., Senni, V.: Controlling Polyvariance for Specialization-Based Verification. 26th Italian Conference on Computational Logic (CILC'11), Pescara, August 31 - September 2, 2011.
Fioravanti, F., Pettorossi, A., Proietti, M., Senni, V.: Program Transformation and Its Applications to Software Synthesis and Verification. IASI-CNR, October 1, 2010.
Pettorossi, A., Proietti, M., Senni, V.: Proving Properties of Infinite Behaviours by Transformation of omega-Programs. IFIP Working Group 2.1, Meeting #66, Atlantic City, NJ, USA 19-24 September 2010.
Pettorossi, A., Proietti, M., Senni, V.: Transformations of Logic Programs on Infinite Lists. 26th International Conference on Logic Programming (ICLP 2010), Edinburgh, Scotland, UK, July 16-19, 2010.
Pettorossi, A., Proietti, M., Senni, V.: A Transformation Strategy for Verifying Logic Programs on Infinite Lists. 25th Italian Conference on Computational Logic (CILC'10), University of Calabria, Rende, Italy, July 7-9, 2010.
Fioravanti, F., Pettorossi, A., Proietti, M., Senni, V.: Generalization Strategies for the Verification of Infinite State Systems. 25th Italian Conference on Computational Logic (CILC'10), University of Calabria, Rende, Italy, July 7-9, 2010.
Pettorossi, A., Proietti, M., Senni, V.: Deciding Full Branching Time Logic by Program Transformation. April 16, 2010, Pescara, Italy.
Pettorossi, A., Proietti, M., Senni, V.: Proving Theorems by Program Transformation. April 16, 2010, Pescara, Italy.
Pettorossi, A., Proietti, M., Senni, V.: Deciding Full Branching Time Logic by Program Transformation. 19th International Symposium on Logic-Based Synthesis and Transformation (LOPSTR '09), September 9-11, 2009, Coimbra, Portugal.
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.
Pettorossi, A.: Algorithms, Nondeterminism, Complexity, and Randomicity, Department of Informatics, Systems, and Production, University of Roma Tor Vergata, March 4, 2009.
Senni, V., Pettorossi, A., Proietti, M.: A Folding Algorithm for Eliminating Existential Variables from Constraint Logic Programs. 24th International Conference on Logic Programming (ICLP'08), December 9-13, 2008, Udine, Italy.
Pettorossi, A.: Just a few sentences... Banquet Speech at the 24rd International Conference on Logic Programming (ICLP 2008), December 9-13, 2008, Udine, Italy.
Pettorossi, A., Proietti, M., Senni, V.: Automatic Correctness Proofs for Logic Program Transformations. 23rd International Conference on Logic Programming (ICLP 2007), September 8-13, 2007, Porto, Portugal.
Pettorossi, A., Proietti, M: Synthesis of Strategies for Impartial Two-Person Games. IFIP WG 2.1, Namur, Belgium, December 11-15, 2006.
Pettorossi, A., Proietti, M., Senni, V.: Proving Properties of Constraint Logic Programs by Eliminating Existential Variables. Twenty Second International Conference on Logic Programming, Seattle (Wa), USA, August 17 - 20, 2006.
Proietti, M.: An Overview of Program Transformation. Workshop on Model Morphisms. IASI-CNR, Rome, Italy, October 17, 2005.
Pettorossi, A., Proietti, M.: Formal Aspects of Program Transformation: Rules and Strategies. Seminar on "Transformation Techniques in Software Engineering" Schloss Dagstuhl, Germany, April 18 - 22, 2005.
Pettorossi, A., Proietti, M.: A Theory of Totally Correct Logic Program Transformations. ACM Symposium on Partial Evaluation and Semantics-Based Program Manipulation (PEPM '04), Verona, Italy, August 24-26, 2004.
Pettorossi, A., Proietti, M.: Automatic Proofs of Protocols by Program Transformation MSRAS-04, International Workshop on Monitoring, Security, and Rescue Techniques in Multiagent Systems, Plock (Poland), June 5-7, 2004. (Invited Talk)
Pettorossi, A.: Derivation of Efficient Logic Programs by Specialization and Reduction of Nondeterminism WRSC'03, Workshop on Robust Software Construction, Hayama, Kanagawa, Japan, February 28 - March 2, 2003. (Invited Talk)
Pettorossi, A.: Specialization of Constraint Logic Programs Waseda University, Tokyo, Japan, March 3, 2003.
Proietti, M.: Software Verification and Synthesis via Program Transformation WRSC'03, Workshop on Robust Software Construction, Hayama, Kanagawa, Japan, February 28 - March 2, 2003. (Invited Talk)
Proietti, M.: Software Verification and Synthesis via Program Transformation. A Case Study: Monadic Second Order Logic Waseda University, Tokyo, Japan, March 4, 2003.
Fioravanti, F., Pettorossi, A., Proietti, M.: Program Specialization, Synthesis, and Verification via Unfold/Fold Transformations Giornata GULP, Bologna 25 October, 2002.
Fioravanti, F., Pettorossi, A., Proietti, M.: Specialization with Clause Splitting For Deriving Deterministic Constraint Logic Programs. IEEE International Conference on Systems, Man, and Cybernetics (SMC'02), 6 - 9 October, 2002, Hammamet, Tunisia.
Fioravanti, F., Pettorossi, A., Proietti, M.: Combining Logic Programs and Monadic Second Order Logics by Program Transformation. LOPSTR'02 Twelfth International Workshop on Logic-based Program Synthesis and Transformation, Madrid, Spain, 17-20 Sept. 2002.
Fioravanti, F., Pettorossi, A., Proietti, M.: A Specialization Technique For Deriving Deterministic Constraint Logic Programs and Its Application to Pattern Matching. AGP'02, 2002 JOINT CONFERENCE ON DECLARATIVE PROGRAMMING, Madrid, Spain,16 - 18 September 2002.
Pettorossi, A., Proietti, M.: Techniques for Program Transformation and Program Synthesis. Workshop of Progetto Cofinanziato, Roma (Italy), December 21-23, 1998.
Pettorossi, A., Proietti, M.: Goal Generalization for Logic Program Transformation. Workshop of Progetto Cofinanziato, Roma (Italy), December 21-23, 1998.