I'm associate professor in Computer Science (SSD 01/B1) at the University "G. d'Annunzio" of Chieti - Pescara (Italy).
- Habilitation as Full Professor (SSD 01/B1 - Computer Science)
- Habilitation as Full Professor (SSD 09/H1 - Information Processing Systems)
- Habilitation as Full Professor (SSD 01/A1 - Mathematical Logic)
- "G. d'Annunzio" University of Chieti - Pescara representative on the board of directors of CINI, the Italian National Interuniversity Consortium for Informatics
- Director of the "G. d'Annunzio" University of Chieti - Pescara unit of the CINI Cybersecurity National Laboratory
- Member of the scientific board of the Italian national PhD program in Blockchain and Distributed Ledger Technology
- Member of the scientific board of the PhD program in Computer Science and Mathematics of the University of Camerino
- Member of the steering committee of the
Logic-Based Program Synthesis and Transformation Symposium (LOPSTR)
- Co-founder and member of the steering committee of the
Horn Clauses for Verification and Synthesis Workshop (HCVS), since 2014
- A web interface for VeriMAP, a system for verifying programs using transformation of Constrained Horn Clauses and SMT solvers, is available
- Program committee member
ICLP 2023,
AAAI 2023,
AIxIA 2022,
LOPSTR 2022,
HCVS 2022,
CILC 2022,
ICLP Doctoral Consortium 2022,
- Chair of the
AIxIA (The Italian Association for Artificial Intelligence) committee
for conferring the
Doctoral Dissertation Award 2021
to the author of a PhD thesis in Artificial Intelligence.
- Secretary of the Italian Association for Logic Programming (GULP)
- Co-editor of the Association for Logic Programming newsletter for the area of Analysis and Verification
- I gave an invited tutorial at LOPSTR 2018 on Constrained Horn Clauses (CHCs). Topics: Constrained Horn Clauses (CHC) for verification;
Satisfiability-preserving CHC transformation rules and strategies;
Semantics-based translation to CHC;
CHC specialization as CHC solving;
Verification of relational properties
such as equivalence, functionality, non-interference (relational program verification);
Verification of programs with inductively-defined data structures (e.g., lists and trees);
Verification of time-aware business processes.
(Slides)
My research interests include
- Constrained Horn Clauses (CHCs), constraint logic programming (CLP)
and their use in analysis, verification and testing.
I'm one of the promoters and members of the steering committee
of HCVS (Workshop on Horn Clauses for Verification and Synthesis) ;
- program transformation methodologies for development, verification and synthesis of programs;
- artificial intelligence;
- cybersecurity;
- bioinformatics, and, in particular, systems biology;
- Program committee member
ICLP Doctoral Consortium 2021,
CILC 2021,
HCVS 2021
- Program committee member
IJCAI-PRICAI 2020,
ECAI 2020,
ICLP Doctoral Consortium 2020,
HCVS 2020,
CILC 2020
- Program committee member
IJCAI 2019,
ICLP 2019,
ICLP Doctoral Consortium 2019,
HCVS 2019,
CILC 2019
- Program committee member ICLP Doctoral Consortium 2018
- Guest editor for the Fundamenta Informaticae special issue on LOPSTR 2017
- Invited tutorialist at LOPSTR 2018 (slides)
- HCVS 2018. 5th Workshop on Horn Clauses for Verification and Synthesis.
Affiliated with CAV, ICLP and IJCAR at
FLoC 2018. 13 July 2018 · Oxford, UK.
- I'm one of the
LOPSTR 2017 Program Chairs
- HCVS 2017. 4th Workshop on Horn Clauses for Verification and Synthesis.
Affiliated with CADE 2017. August 7, 2017, Gothenburg, Sweden (PC)
- CP/ICLP-DC-2017. Joint CP/ICLP Doctoral Consortium. August 28, 2017, Melbourne, Australia. (PC)
- CILC 2017. 32nd Italian Conference on Computational Logic. 26-29 September 2017, Naples, Italy (PC)
- I'm on the editorial board of Intelligenza Artificiale,
the international journal of the Italian Association on Artificial Intelligence AIxIA.
- AIxIA Doctoral Dissertation Award 2016. (PC)
- LOPSTR 2016. 26th International Symposium on Logic-Based Program Synthesis and Transformation, September 6-8, 2016. Edinburgh, UK. (PC)
- ICLP-DC-2016. ICLP Doctoral Consortium. New York, 16 July 2016. (PC)
- CILC 2016. 31-esimo Convegno Italiano di Logica Computazionale. 20-22 giugno 2016. Milano. (PC)
- HCVS 2016. Third Workshop on Horn Clauses for Verification and Synthesis.
Affiliated with ETAPS 2016. 2-8 April 2016. Eindhoven, The Netherlands. (PC)
- VPT 2016. Fourth International Workshop on Verification and Program Transformation.
Affiliated with ETAPS 2016. 2-8 April 2016. Eindhoven, The Netherlands. (PC)
- ICLP-DC-2015. ICLP Doctoral Consortium. Cork, Ireland, 31 August 2015. (PC)
- HCVS 2015. Second Workshop on Horn Clauses for Verification and Synthesis.
Affiliated with CAV 2015. July 18, 2015. San Francisco, USA. (Program and Steering Committee).
- PPDP 2015.
17th International Symposium on Principles and Practice of Declarative Programming
July 14-16, 2015. Siena, Italy (PC)
- CILC 2015. 30-esimo Convegno Italiano di Logica Computazionale. 1-3 Luglio 2015, Genova (PC)
- VPT 2015.
Third International Workshop on Verification and Program Transformation.
April 11, 2015, London, UK @ETAPS2015 (PC)
- HCVS 2014. First Workshop on Horn Clauses for Verification and Synthesis.
Affiliated with ICLP and CAV
at FLoC / VSL. July 17, 2014. Vienna, Austria. (co-chair / organizer).
- LOPSTR 2014. 24th International Symposium on Logic-Based Program Synthesis and Transformation, September 10-11, 2014. Canterbury, UK (PC)
- CILC 2014. 29-esimo Convegno Italiano di Logica Computazionale. 16 - 18 Giugno 2014, Torino (PC)
- ICLP-DC-2014. ICLP Doctoral Consortium. Vienna, Austria, 20 July 2014. (PC)
- AIxIA Doctoral Dissertation Award 2013. (chair)
- CILC 2013. 28-esimo Convegno Italiano di Logica Computazionale. 25 - 27 Settembre 2013, Catania (PC)
- ICLP-DC-2013. ICLP Doctoral Consortium. Istanbul, Turkey, 24 August 2013. (PC)
- ICLP-DC-2012. ICLP Doctoral Consortium. Budapest, Hungary, 4 September 2012. (PC)
- CILC 2011. 26-esimo Convegno Italiano di Logica Computazionale. 31 Agosto - 2 Settembre 2011, Pescara. (chair)
- IJCAI 2011. The twentieth International Joint Conference on Artificial Intelligence. Barcelona July 2011. (PC)
- LOPSTR 2010. 20th International Symposium on Logic-Based Program Synthesis and Transformation, July 23-25, 2010. Hagenberg, Austria (PC)
- mLife 2010, Mobile Life Conferences, 27-29 October 2010, The Grand Hotel, Brighton, UK. And 2009, 2008, 2006 editions (PC)
I participated in the following research projects: - "Vincoli e preferenze come formalismo unificante per l'analisi di sistemi informatici e la soluzione di problemi reali" Progetto MIUR PRIN 2005 n.2005-015491
I was the local team coordinator of the research unit at the University of Chieti-Pescara, for the research project "Simulation and modeling of biological systems using StateCharts (SIMBIOSYS)", funded by the Italian Ministry for University and Scientific Research PRIN 2008, n.20083K772X_003.
I am a research associate at IASI-CNR and a member of the MAP group.
I am a member of the Italian Association for Logic Programming (GULP).
Below you can find some recent papers of mine.
Please cite the most recent papers that are indexed by Scopus, if possible.
Thank you!
If you are interested in my work, please feel free to contact me.
Some other papers of mine are listed
on DBLP,
on Google Scholar,
and on the reports page of the MAP Group
Note that the list of papers below has not been updated since 2017.
De Angelis, E., Fioravanti, F., Pettorossi, A., Proietti, M.: Predicate Pairing for Program Verification. Theory and Practice of Logic Programming (TPLP). Published online 4th December 2017. (to appear)
E. De Angelis, F. Fioravanti, M.C. Meo, A. Pettorossi, M. Proietti. 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. (Extended version)
E. De Angelis, F. Fioravanti, M.C. Meo, A. Pettorossi, M. Proietti. 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). LNCS, Vol 10184, Springer, 2017.
De Angelis, E., Fioravanti, F., Pettorossi, A., Proietti, M.: Semantics-based generation of verification conditions via program specialization. Science of Computer Programming, 2017 (To appear). Elsevier Copyright 2017. [Also available as Technical Report R. 9, 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, 2017, pp. 73-117. IOS Press Copyright 2017. [Also available as Technical Report R. 8, 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, A., 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. DOI: 10.1093/logcom/ext071
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. DOI 10.3233/FI-2015-1257. IOS Press. 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.
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).
Slides
Also presented at the 30th Italian Conference on Computational Logic (CILC 2015),
Genova, Italy, 1st - 3rd July, 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.
De Angelis, E., Fioravanti, F., Navas, J., Proietti, M.: Verification of Programs by Combining Iterated Specialization with Interpolation. Proceedings of the 1st CAV & ICLP Workshop on Horn Clauses for Verification and Synthesis, HCVS 2014, @FLoC 17 July, 2014, Vienna, Austria, EPTCS 169.
De Angelis, E., Fioravanti, F., Pettorossi, A., Proietti, M.: Program Verification using Constraint Handling Rules and Array Constraint Generalizations. Proceedings of the 29th Italian Conference on Computational Logic, CILC 2014, 16-18 June, 2014, Torino, Italy, CEUR-WS 1195.
De Angelis, E., Fioravanti, F., Pettorossi, A., Proietti, M.: Program Verification via Iterated Specialization. Science of Computer Programming 95: 149-175 (2014).
De Angelis, E., Fioravanti, F., Pettorossi, A., Proietti, M.: VeriMAP: A Tool for Verifying Programs through Transformations. 20th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS). @ETAPS 2014: 5-13 April 2014, Grenoble, France Lecture Notes in Computer Science, Vol. 8413.
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). January 19-21, 2014, San Diego, USA. Lecture Notes in Computer Science, Vol. 8318.
Fioravanti, F., Pettorossi, A., Proietti, M., Senni, V.: Proving Theorems by Program Transformation Fundamenta Informaticae, Vol. 127 (2013), Special issue on Andrzej Skowron's 70th Birthday, pp. 115-134, http://dx.doi.org/10.3233/FI-2013-899, IOS Press.
De Angelis, E., Fioravanti, F., Pettorossi, A., Proietti, M.: Verification of Imperative Programs by Constraint Logic Program Transformation. SAIRP 2013. Semantics, Abstract Interpretation, and Reasoning about Programs: Essays Dedicated to David A. Schmidt on the Occasion of his Sixtieth Birthday. Manhattan, Kansas, USA, 19-20th September 2013. Slides
De Angelis, E., Fioravanti, F., Pettorossi, A., Proietti, M.: Verification of Imperative Programs by Transforming Constraint Logic Programs. CILC 2013. Catania, Italy
Emanuele De Angelis, Fabio Fioravanti, Alberto Pettorossi and Maurizio Proietti. Verification of Imperative Programs through Transformation of Constraint Logic Programs. First International Workshop on Verification and Program Transformation (VPT13). @CAV2013. Slides
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.
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 Synhesis and Transformation (LOPSTR 2012), Leuven, Belgium, September 18-20, 2012. Lecture Notes in Computer Science 7844, pp. 51-70, Springer.
Fioravanti, F., Pettorossi, A., Proietti, M., Senni, V.: Generalization Strategies for the Verification of Infinite State Systems. Theory and Practice of Logic Programming, Volume 13-2, 2013. Wolfgang Faber and Nicola Leone (Eds.), Special Issue on the 25th GULP annual conference.
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.
Fioravanti, F., Pettorossi, A., Proietti, M., Senni, V.: Improving Reachability Analysis of Infinite State Systems by Specialization. Fundamenta Informaticae 119 (2012) pp. 1-20. DOI 10.3233/FI-2012-720, IOS Press.
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.
Senni, V., Fioravanti, F.: Generation of test data structures using Constraint Logic Programming. Proceedings of the 6th International Conference on Tests & Proofs TAP 2012, Lecture Notes in Computer Science 7305, pages 115-131, DOI: 10.1007/978-3-642-30473-6_10, Springer. [extended and revised version: IASI Report 12-04] [Experiments pack] Slides. Also presented at CILC12.
Fabio Fioravanti, Manuela Helmer-Citterich and Enrico Nardelli. Modeling gene regulatory network motifs using statecharts. BMC Bioinformatics 2012, 13(Suppl 4):S20.
Stefano Bistarelli, Fabio Fioravanti, Pamela Peretti, Francesco Santini. Evaluation of complex security scenarios using defense trees and economic indexes. Journal of Experimental & Theoretical Artificial Intelligence. pp 161-192 Volume 24, Issue 2, 2012. Journal website.
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 Synthesis and Transformation (LOPSTR 2011), July 18-20, 2011, Odense, Denmark, pp. 96-111, Univ. of Southern Denmark, 2011. Lecture Notes in Computer Science 7225, pp. 106-122, Springer, 2012
Fioravanti, F., Pettorossi, A., Proietti, M., Senni, V.: Reachability Analysis Via Specialization of Constraint Logic Programs. ALP Newsletter, September 2011.
Fioravanti, F.. Proceedings of the 26th Italian Conference on Computational Logic (CILC 2011), August 31 - September 2, 2011. Pescara, Italy. (Editor) [CEUR-WS, Vol-810, urn:nbn:de:0074-810-0, ISSN 1613-0073.]
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), August 31 - September 2, 2011. Pescara, Italy. [CEUR-WS, Vol-810, urn:nbn:de:0074-810-0, ISSN 1613-0073.]
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.
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.
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.
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.]
Fabio Fioravanti
Dipartimento di Economia
Università "G. D'Annunzio" di Chieti-Pescara
Viale Pindaro, 42
I-65127 Pescara (ITALY)
Email <mylastname> AT unich.it
Tel +39 (0)85 453 7697
Fax +39 (0)85 4508 3208