Postdoc at University "G. D'Annunzio" of Chieti-Pescara

I received my Ph.D. degree in Computer Science from the University "G. D'Annunzio" of Chieti-Pescara in April 2014 defending a thesis entitled "Software Verification and Synthesis using Constraints and Program Transformation".
The thesis work has been done under the supervision of Prof. Fabio Fioravanti and Dr. Maurizio Proietti.

I received my master degree in Computer Science Engineering from the University of Rome "Tor Vergata" in May 2010 defending a thesis entitled "Synthesis of Reactive Systems using Answer Set Programming".
The thesis work has been done under the supervision of Prof. Alberto Pettorossi, and Dr. Maurizio Proietti.

Research Associate at IASI - CNR of Rome.

My research interests concern automatic synthesis and verification of reactive systems, static program analysis and software model checking by using techniques based on logic programming and program transformation.

Papers

Verification of Time-Aware Business Processes using Constrained Horn Clauses Download paper
E. De Angelis, F. Fioravanti, M.C. Meo, A. Pettorossi, M. Proietti.
Pre-proceedings of the 26th International Symposium on Logic-Based Program Synthesis and Transformation (LOPSTR 2016).
arXiv.org
Relational Verification through Horn Clause Transformation Download paper
E. De Angelis, F. Fioravanti, A. Pettorossi, M. Proietti.
Proceedings of the 23rd Static Analysis Symposium (SAS 2016).
Lecture Notes in Computer Science (LNCS), vol. 9837, Springer, 2016.
Verifying Relational Program Properties by Transforming Constrained Horn clauses Download paper
E. De Angelis, F. Fioravanti, A. Pettorossi, M. Proietti.
Proceedings of the 31st Italian Conference on Computational Logic (CILC 2016).
CEUR Workshop Proceedings (CEUR-WS.org), vol. 1645, CEUR-WS.org, 2016.
Removing Unnecessary Variables from Horn Clause Verification Conditions Download paper
E. De Angelis, F. Fioravanti, A. Pettorossi, M. Proietti.
Proceedings of the Third Workshop on Horn Clauses for Verification and Synthesis (HCVS 2016).
Electronic Proceedings in Theoretical Computer Science (EPTCS), volume 219, Open Publishing Association, 2016.
Proving Correctness of Imperative Programs by Linearizing Constrained Horn Clauses Download paper
E. De Angelis, F. Fioravanti, A. Pettorossi, M. Proietti.
Theory and Practice of Logic Programming, vol. 15 (issue 4-5), pp. 635-650, Cambridge University Press, 2015.
Special issue containing the regular papers of the 31st International Conference on Logic Programming (ICLP 2015).
A preliminary version has been presented at the 3rd International Workshop on Verification and Program Transformation (VPT 2015).
Semantics-based generation of verification conditions by program specialization Download paper
E. De Angelis, F. Fioravanti, A. Pettorossi, M. Proietti.
Proceedings of the 17th International Symposium on Principles and Practice of Declarative Programming (PPDP 2015).
ACM, 2015.
Also presented the 30th Italian Conference on Computational Logic (CILC 2015).
A Rule-based Verification Strategy for Array Manipulating Programs Download paper
E. De Angelis, F. Fioravanti, A. Pettorossi, M. Proietti.
Fundamenta Informaticae, vol. 140, 2015.
Verification of Programs by Combining Iterated Specialization with Interpolation Download paper
E. De Angelis, F. Fioravanti, J. A. Navas, M. Proietti.
Proceedings of the First Workshop on Horn Clauses for Verification and Synthesis (HCVS 2014).
Electronic Proceedings in Theoretical Computer Science (EPTCS), vol. 169, Open Publishing Association, 2014.
Program Verification using Constraint Handling Rules and Array Constraint Generalizations Download paper
E. De Angelis, F. Fioravanti, A. Pettorossi, M. Proietti.
Proceedings of the 29th Italian Conference on Computational Logic (CILC 2014).
CEUR Workshop Proceedings (CEUR-WS.org), vol. 1195, CEUR-WS.org, 2014.
Program Verification via Iterated Specialization Download paper
E. De Angelis, F. Fioravanti, A. Pettorossi, M. Proietti
Science of Computer Programming, 2014.
VeriMAP: A Tool for Verifying Programs through Transformations (Tool demonstration paper) Download paper
E. De Angelis, F. Fioravanti, A. Pettorossi, M. Proietti.
Proceedings of the 20th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2014).
Lecture Notes in Computer Science (LNCS), vol. 8413, Springer, 2014.
Verifying Array Programs by Transforming Verification Conditions Download paper
E. De Angelis, F. Fioravanti, A. Pettorossi, M. Proietti.
Proceedings of the 15th International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI 2014).
Lecture Notes in Computer Science (LNCS), vol. 8318, Springer, 2014.
Verification of Imperative Programs by Constraint Logic Program Transformation Download paper
E. De Angelis, F. Fioravanti, A. Pettorossi, M. Proietti.
Semantics, Abstract Interpretation, and Reasoning about Programs (SAIRP 2013).
Electronic Proceedings in Theoretical Computer Science (EPTCS), vol. 129, Open Publishing Association, 2013.
Verification of Imperative Programs through Transformation of Constraint Logic Programs Download paper
E. De Angelis, F. Fioravanti, A. Pettorossi, M. Proietti.
Proceedings of the First International Workshop on Verification and Program Transformation (VPT).
EasyChair Proceedings in Computing Series (EPiCS), vol. 16, 2013.
Also presented at the 28th Italian Conference on Computational Logic (CILC 2013).
CEUR Workshop Proceedings (CEUR-WS.org), vol. 1068, 2013.
Verifying Programs via Iterated Specialization Download paper
E. De Angelis, F. Fioravanti, A. Pettorossi, M. Proietti.
Proceedings of the ACM SIGPLAN Workshop on Partial Evaluation and Program Manipulation (PEPM 2013).
ACM, 2013.
Synthesizing Concurrent Programs using Answer Set Programming Download paper
E. De Angelis, A. Pettorossi, M. Proietti.
Fundamenta Informaticae, vol. 120, 2012.
The source code for synthesizing k-mutex-p programs can be found here.
More details on the experimental evaluation can be found in my Ph.D. thesis (Part II - Chapters 4 and 6).
Specialization with Constrained Generalization for Software Model Checking Download paper
E. De Angelis, F. Fioravanti, A. Pettorossi, M. Proietti.
Proceedings of the 22nd International Symposium on Logic-Based Program Synthesis and Transformation (LOPSTR 2012).
Lecture Notes in Computer Science (LNCS), vol. 7844, Springer, 2013.
Software Model Checking by Program Specialization (Research summary). Download paper
E. De Angelis.
Technical Communications of the 28th International Conference on Logic Programming (ICLP 2012).
Leibniz International Proceedings in Informatics (LIPIcs), vol. 17, 2012.
Software Model Checking by Program Specialization Download paper
E. De Angelis, F. Fioravanti, A. Pettorossi, M. Proietti.
Proceedings of the 27th Italian Conference on Computational Logic, (CILC 2012).
CEUR Workshop Proceedings (CEUR-WS.org), vol. 857, 2012.
Synthesizing Concurrent Programs using Answer Set Programming Download paper
E. De Angelis, A. Pettorossi, M. Proietti.
Proceedings of the International Workshop on on Concurrency, Specification, and Programming (CS&P2011).
Published by Białystok University of Technology, 2011.
Also presented at the 26th Italian Conference on Computational Logic (CILC 2011).
CEUR Workshop Proceedings (CEUR-WS.org), vol. 810, 2011.

Talks

Verifying Relational Program Properties by Transforming Constrained Horn clauses. Download presentation
31st Italian Conference on Computational Logic (CILC 2016).
June 20-22, 2016, University of Milano-Bicocca, Italy.
Software Verification and Synthesis using Constraints and Program Transformation. Download presentation
30th Italian Conference on Computational Logic (CILC 2015).
Genova, Italy, July 1-3, 2015.
Verification of Programs by Combining Iterated Specialization with Interpolation. Download presentation
First International Workshop on Horn Clauses for Verification and Synthesis (HCVS 2014).
Vienna, Austria, July 17, 2014.
Program Verification using Constraint Handling Rules and Array Constraint Generalizations. Download presentation
29th Italian Conference on Computational Logic (CILC 2014).
Turin, Italy, June 16-18, 2014.
VeriMAP: A Tool for Verifying Programs through Transformations. Download presentation
20th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2014).
Grenoble, France, April 5-13, 2014.
Verifying Programs via Iterated Specialization. Download presentation
ACM SIGPLAN Workshop on Partial Evaluation and Program Manipulation. (PEPM 2013).
Rome, Italy, January 21-22, 2013.
Branching Preserving Specialization for Software Model Checking. Download presentation
International Symposium on Logic-Based Program Synhesis and Transformation (LOPSTR 2012).
Leuven, Belgium, September 18-20, 2012.
Software Model Checking by Program Specialization. Download presentation
International Conference on Logic Programming (ICLP 2012).
Budapest, Hungary, September 3-8, 2012
Software Model Checking by Program Specialization. Download presentation
27th Italian Conference on Computational Logic (CILC 2012).
Rome, Italy, June 6-7, 2012.
Synthesizing Concurrent Programs using Answer Set Programming. Download presentation
International Workshop on on Concurrency, Specification, and Programming (CS& P2011).
Puł tusk, Poland, September 28-30, 2011.
Extended version of the presentation given in February 2012 at LIAFA, Paris, France. Download presentation
Synthesizing Concurrent Programs using Answer Set Programming. Download presentation
26th Italian Conference on Computational Logic (CILC 2011).
Pescara, Italy, August 31 - September 2, 2011.
CILC 2016: 31st Italian Conference on Computational Logic (PC Member)
June 20-22, 2016, University of Milano-Bicocca, Italy.
POPL 2016 Artifact Evaluation (PC Member)
CILC 2015: 30th Italian Conference on Computational Logic (PC Member)
July 1-3, 2015, University of Genova, Italy.
VPT 2015: 3rd International Workshop on Verification and Program Transformation (OC Member)
April 11, 2014, London, UK.
LOPSTR 2014: 24th International Symposium on Logic-based Program Transformation and Synthesis (OC Member)
September 9-11, 2014, University of Kent, Canterbury, UK.
CILC 2011: 26th Italian Conference on Computational Logic (OC Member)
August 31 - September 2, 2011, University of Chieti-Pescara, Italy.
IFIP WG2.1 2012: 68th meeting of the IFIP Working Group 2.1 on Algorithmic Languages and Calculi (OC Member)
February 6-10, 2012, Rome, Italy.
The VeriMAP software verifier based on transformation of contraint logic programs. (Please, take a look at the TACAS poster)
A prototype version of the CHC-CPA (Constrained Horn Clauses) for The Configurable Software-Verification Platform (preliminary results)

Emanuele DE ANGELIS
Dipartimento di Economia
Università G. D'Annunzio di Chieti-Pescara
Viale Pindaro, 42
I-65127 Pescara (ITALY)

Email: