Postdoc at University "G. D'Annunzio" of Chieti-Pescara and Research Associate at IASI - CNR of Rome.

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.

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 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.
De Angelis, E., Pettorossi, A., Proietti, M.
Fundamenta Informaticae, vol. 120, 2012.
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.
Branching Preserving Specialization for Software Model Checking. Download paper
E. De Angelis, F. Fioravanti, A. Pettorossi, M. Proietti.
Preliminary Proceedings of the 22nd International Symposium on Logic-Based Program Synthesis and Transformation (LOPSTR 2012).
Published by the KU of Leuven, 2012.
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

Verification of Programs by Combining Iterated Specialization with Interpolation. Download presentation
of the First International Workshop on Horn Clauses for Verification and Synthesis (HCVS 2014).
Vienna, Austria, 17 July, 2014.
Program Verification using Constraint Handling Rules and Array Constraint Generalizations. Download presentation
29th Italian Conference on Computational Logic (CILC 2014).
Turin, Italy, 16-18 June, 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, 5-13 April 2014.
Verifying Programs via Iterated Specialization. Download presentation
ACM SIGPLAN Workshop on Partial Evaluation and Program Manipulation. (PEPM 2013).
January 21-22 2013, Rome, Italy.
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.
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: