Emanuele De Angelis
Emanuele De Angelis Emanuele De Angelis
Researcher

Istituto di Analisi dei Sistemi ed Informatica "Antonio Ruberti"
Via dei Taurini, 19
00185 Roma - Italy

Office n. .
email

Research groups

Selected publications
  • Emanuele De Angelis, Fioravanti F., Pettorossi A., Maurizio Proietti: Removing Algebraic Data Types from Constrained Horn Clauses Using Difference Predicates, in the Proceedings of International Joint Conference on Automated Reasoning IJCAR 2020, Lecture Notes in Computer Science, 12166, 2020
  • Emanuele De Angelis, Fioravanti F., Maurizio Proietti: Transformational verification of quicksort, in the Proceedings of 8th International Workshop on Verification and Program Transformation, Electronic Proceedings in Theoretical Computer Science, 320, 2020
  • Emanuele De Angelis, Fioravanti F., Meo M.C., Pettorossi A., Maurizio Proietti: Semantics and controllability of time-aware business processes, Fundamenta Informaticae 165, 2019
  • Emanuele De Angelis, Fioravanti F., Palacios A., Pettorossi A., Maurizio Proietti: Property-Based Test Case Generators for Free, Lecture Notes in Computer Science 11823, 186-206, 2019
  • Emanuele De Angelis, Fioravanti F., Pettorossi A., Maurizio Proietti: Lemma Generation for Horn Clause Satisfiability: A Preliminary Study, in the Proceedings of Seventh International Workshop on Verification and Program Transformation (VPT 2019), Lisitsa A., Nemytykh A. eds., Electronic Proceedings in Theoretical Computer Science, 299, 2019
  • Emanuele De Angelis, Fioravanti F., Pettorossi A., Maurizio Proietti: Proving Properties of Sorting Programs: A Case Study in Horn Clause Verification, in the Proceedings of Sixth Workshop on Horn Clauses for Verification and Synthesis and Third Workshop on Program Equivalence and Relational Reasoning (HCVS/PERR 2019), Electronic Proceedings in Theoretical Computer Science, 296, 2019
  • Emanuele De Angelis, Fioravanti F., Palacios A., Pettorossi A., Maurizio Proietti: Bounded Symbolic Execution for Runtime Error Detection of Erlang Programs, in the Proceedings of 5th Workshop on Horn Clauses for Verification and Synthesis (HCVS 2018), Electronic Proceedings in Theoretical Computer Science, 278, 2018
  • Emanuele De Angelis, Fioravanti F., Pettorossi A., Maurizio Proietti: Predicate Pairing for Program Verification, Theory and Practice of Logic Programming 18, 126-166, 2018
  • Emanuele De Angelis, Fioravanti F., Pettorossi A., Maurizio Proietti: Predicate pairing with abstraction for relational verification, Lecture Notes in Computer Science 10855, 289-305, 2018
  • Emanuele De Angelis, Fioravanti F., Pettorossi A., Maurizio Proietti: Solving Horn Clauses on Inductive Data Types Without Induction, Theory and Practice of Logic Programming 18, 452-469, 2018
  • Emanuele De Angelis, Fioravanti F., Meo M.C., Pettorossi A., Maurizio Proietti: Verifying Controllability of Time-Aware Business Processes, Lecture Notes in Computer Science 10364, 103-118, 2017
  • Emanuele De Angelis, Fioravanti F., Pettorossi A., Maurizio Proietti: Enhancing Predicate Pairing with Abstraction for Relational Verification, in the Proceedings of the 27th International Symposium on Logic-Based Program Synthesis and Transformation (LOPSTR 2017), Preliminary version, Fioravanti F, Gallagher J. eds., CoRR, arXiv, 1708-07854, 2017
  • Emanuele De Angelis, Fioravanti F., Pettorossi A., Maurizio Proietti: Predicate Pairing for Program Verification, CoRR arXiv.org 1708-01473, 17000, 2017
  • Emanuele De Angelis, Fioravanti F., Pettorossi A., Maurizio Proietti: Program Verification using Constraint Handling Rules and Array Constraint Generalizations, Fundamenta Informaticae 150 (1), 73-117, 2017
  • Emanuele De Angelis, Fioravanti F., Pettorossi A., Maurizio Proietti: Semantics-based generation of verification conditions via program specialization, Science of Computer Programming 147, 78-108, 2017
  • Emanuele De Angelis, Fioravanti F., Meo M.C., Pettorossi A., Maurizio Proietti: Verification of Time-Aware Business Processes using Constrained Horn Clauses, in the Proceedings of the International Symposium on Logic-based Program Transformation and Synthesis (LOPSTR 2016), 2016
  • Emanuele De Angelis, Fioravanti F., Meo M.C., Pettorossi A., Maurizio Proietti: Verifying Controllability of Time-Aware Business Processes, IASI-CNR, R. 16-08, 2016
  • Emanuele De Angelis, Fioravanti F., Pettorossi A., Maurizio Proietti: Horn Clause Transformation for Program Verification, Newsletter of the Association for Logic Programming, https://www.cs.nmsu.edu/ALP/2016/09, 2016
  • Emanuele De Angelis, Fioravanti F., Pettorossi A., Maurizio Proietti: Relational Verification Through Horn Clause Transformation, Lecture Notes in Computer Science 9837, 147-169, 2016
  • Emanuele De Angelis, Fioravanti F., Pettorossi A., Maurizio Proietti: Removing unnecessary variables from Horn clause verification conditions, in the Proceedings of 3rd International Workshop on Horn Clauses for Verification and Synthesis, Electronic Proceedings in Theoretical Computer Science, 219, 2016
  • Emanuele De Angelis, Fioravanti F., Pettorossi A., Maurizio Proietti: Semantics-based generation of verification conditions via program specialization, IASI-CNR, R. 16-09, 2016
  • Emanuele De Angelis, Fioravanti F., Pettorossi A., Maurizio Proietti: Verifying relational program properties by transforming constrained Horn clauses, in the Proceedings of Proceedings of the 31st Italian Conference on Computational Logic, CEUR-WS, 1645, 2016
  • Emanuele De Angelis, Fioravanti F., Pettorossi A., Maurizio Proietti: A Rule-based Verification Strategy for Array Manipulating Programs, Fundamenta Informaticae 140, 329-355, 2015
  • Emanuele De Angelis, Fioravanti F., Pettorossi A., Maurizio Proietti: Automated Verification of Relational Program Properties, IASI-CNR, R. 15-07, 2015
  • Emanuele De Angelis, Fioravanti F., Pettorossi A., Maurizio Proietti: Program Verification using Constraint Handling Rules and Array Constraint Generalizations, IASI-CNR, R. 15-08, 2015
  • Emanuele De Angelis, Fioravanti F., Pettorossi A., Maurizio Proietti: Proving Correctness of Imperative Programs by Linearizing Constrained Horn Clauses, Theory and Practice of Logic Programming 15, 635-650, 2015
  • Emanuele De Angelis, Fioravanti F., Pettorossi A., Maurizio Proietti: Proving Horn Clause Specifications of Imperative Programs, IASI-CNR, R. 15-09, 2015
  • Emanuele De Angelis, Fioravanti F., Pettorossi A., Maurizio Proietti: Semantics-based generation of verification conditions by program specialization, ACM Symposium on Principles and Practice of Declarative Programming, 2015
  • Emanuele De Angelis, Fioravanti F., Navas J, Maurizio Proietti: Verification of Programs by Combining Iterated Specialization with Interpolation, in the Proceedings of First Workshop on Horn Clauses for Verification and Synthesis, Electronic Proceedings in Theoretical Computer Science, 169, 2014
  • Emanuele De Angelis, Fioravanti F., Pettorossi A., Maurizio Proietti: A Rule-based Verification Strategy for Array Manipulating Programs, IASI-CNR, R. 14-07, 2014
  • Emanuele De Angelis, Fioravanti F., Pettorossi A., Maurizio Proietti: Program Verification using Constraint Handling Rules and Array Constraint Generalizations, in the Proceedings of Proceedings of VPT 2014, EasyChair Proceedings in Computing (EPiC) series, 28, 2014
  • Emanuele De Angelis, Fioravanti F., Pettorossi A., Maurizio Proietti: Program verification via iterated specialization, Science of Computer Programming 95, 149-175, 2014
  • Emanuele De Angelis, Fioravanti F., Pettorossi A., Maurizio Proietti: Verifying Array Programs by Transforming Verification Conditions, Lecture Notes in Computer Science 8318, 182-202, 2014
  • Emanuele De Angelis, Fioravanti F., Pettorossi A., Maurizio Proietti: VeriMAP: A tool for verifying programs through transformations, Lecture Notes in Computer Science 8413, 568-574, 2014
  • Emanuele De Angelis, Fioravanti F., Pettorossi A., Maurizio Proietti: Program Verification via Iterated Specialization, IASI-CNR, R. 13-11, 2013
  • Emanuele De Angelis, Fioravanti F., Pettorossi A., Maurizio Proietti: Specialization with Constrained Generalization for Software Model Checking, Lecture Notes in Computer Science Vol. 7844, pp. 51-70, 2013
  • Emanuele De Angelis, Fioravanti F., Pettorossi A., Maurizio Proietti: Verification of Imperative Programs by Constraint Logic Program Transformation, in the Proceedings of SAIRP 2013, Festschrift for Dave Schmidt, Electronic Proceedings in Theoretical Computer Science, Vol 129, pp. 186-210, 2013
  • Emanuele De Angelis, Fioravanti F., Pettorossi A., Maurizio Proietti: Verification of Imperative Programs by Transforming Constraint Logic Programs, in the Proceedings of the 28th Italian Conference on Computational Logic (CILC 2013), CEUR-WS, Vol. 1068, pp. 83-98, 2013
  • Emanuele De Angelis, Fioravanti F., Pettorossi A., Maurizio Proietti: Verification of Imperative Programs through Transformation of Constraint Logic Programs, in the Proceedings of First International Workshop on Verification and Program Transformation (VPT 2013), EasyChair Proceedings in Computing (EPiC) series, Vol. 16, pp. 30-41, 2013
  • Emanuele De Angelis, Fioravanti F., Pettorossi A., Maurizio Proietti: Verifying Array Programs by Transforming Verification Conditions, IASI-CNR, R. 13-12, 2013
  • Emanuele De Angelis, Fioravanti F., Pettorossi A., Maurizio Proietti: Verifying Programs via Iterated Specialization, in the Proceedings of Partial Evaluation and Program Manipulation (PEPM '13), ACM-SIGPLAN, 2013
  • Emanuele De Angelis, Fioravanti F., Pettorossi A., Maurizio Proietti: Branching Preserving Specialization for Software Model Checking, in the Proceedings of 22nd International Symposium on Logic-Based Program Synhesis and Transformation (LOPSTR 2012), Albert E. ed., 2012
  • Emanuele De Angelis, Fioravanti F., Pettorossi A., Maurizio Proietti: Software Model Checking by Program Specialization, in the Proceedings of 27th Italian Conference on Computational Logic (CILC-2012), CEUR-WS, 857, 2012
  • Emanuele De Angelis, Fioravanti F., Pettorossi A., Maurizio Proietti: Verifying Programs via Iterated Specialization, IASI-CNR, R. 12-22, 2012
  • Emanuele De Angelis, Pettorossi A., Maurizio Proietti: Synthesizing Concurrent Programs Using Answer Set Programming, Fundamenta Informaticae 120, 205-229, 2012
  • Emanuele De Angelis, Pettorossi A., Maurizio Proietti: Using Answer Set Programming Solvers to Synthesize Concurrent Programs, IASI-CNR, R. 12-19, 2012
  • Emanuele De Angelis, Pettorossi A., Maurizio Proietti: Synthesizing Concurrent Programs using Answer Set Programming, in the Proceedings of International Workshop on Concurrency, Specification and Programming (CS&P 2011), Pultusk, Poland, 28-30 Sept. 2011, 2011
- - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - -