Welcome to my webpage

Publications BibTeX

Click here to display ISI and Scopus codes


journals | book chapters | invited papers | electronic journals | conference and workshop proceedings | editorship | workshop notes | phd_thesis | master thesis
full text: download the full text in pdf       slides: download the slides in pdf       BibTeX: export the citation in BibTeX

    Journals [top]

  1. full text BibTeX Dylan Bellier, Massimo Benerecetti, Dario Della Monica, and Fabio Mogavero. Alternating (In)Dependence-Friendly Logic. Annals of Pure and Applied Logic (APAL), 2023 (DOI: 10.1016/j.apal.2023.103315).
  2. full text BibTeX Andrea Brunello, Dario Della Monica, Angelo Montanari, Nicola Saccomanno, and Andrea Urgolo. Monitors that Learn from Failures: Pairing STL and Genetic Programming. IEEE Access, 2023 (DOI: 10.1109/ACCESS.2023.3277620, online since May 2023).
  3. full text BibTeX D. Della Monica, A. Montanari, and P. Sala. An interval temporal logic characterization of extended omega-regular languages. Theoretical Computer Science (TCS), 2023 (DOI: 10.1016/j.tcs.2023.113929, online since 10 May 2023).
    *** Journal version of ICTCS 2021 and [Montanari, Sala; LATA 2013].
  4. full text BibTeX Willem Conradie, Dario Della Monica, Emilio Muñoz-Velasco, Guido Sciavicco, and Ionel Eduard Stan. Fuzzy Halpern and Shoham's Interval Temporal Logics. Fuzzy Sets and Systems (FSS), 2023 (DOI: 10.1016/j.fss.2022.05.014, online since 24 May 2022).
    *** Journal version of ECAI 2020 and ICTCS 2020.
  5. full text BibTeX D. Bellier, M. Benerecetti, D. Della Monica, F. Mogavero. Good-for-Game QPTL: An Alternating Hodges Semantics. ACM Transactions on Computational Logic (ACM ToCL), 2023 (DOI: 10.1145/3565365).
  6. full text BibTeX D. Barozzini, D. de Frutos-Escrig, D. Della Monica, A. Montanari, and P. Sala. Beyond omega-regular languages: omegaT-regular expressions and their automata and logic counterparts. Theoretical Computer Science (TCS), 2020 (DOI: 10.1016/j.tcs.2019.12.029, online since 3 January 2020).
    *** Journal version of ICTCS 2017 and GandALF 2017.
  7. full text BibTeX D. Bresolin, D. Della Monica, A. Montanari, P. Sala, and G. Sciavicco. Decidability and complexity of the fragments of the modal logic of Allen's relations over the rationals. Information and Computation (IC), 2019 (DOI: 10.1016/j.ic.2019.02.002, online since 4 March 2019).
    *** Journal version of LATA 2015.
  8. full text BibTeX L. Aceto, D. Della Monica, I. Fábregas, and A. Ingólfsdóttir. When are prime formulae characteristic?. Theoretical Computer Science (TCS), 2019 (DOI: 10.1016/j.tcs.2018.12.004, online since 6 December 2018).
    *** Journal version of MFCS 2015.
  9. full text BibTeX L. Aceto, D. Della Monica, V. Goranko, A. Ingólfsdóttir, A. Montanari, and G. Sciavicco. A complete classification of the expressiveness of interval logics of Allen's relations: The general and the dense cases. Acta Informatica, 53(3):207-246, 2016 (DOI: 10.1007/s00236-015-0231-4, online since May 2015).
    *** Journal version of IJCAI 2011 and TIME 2013.
  10. full text BibTeX D. Bresolin, D. Della Monica, A. Montanari, P. Sala, and G. Sciavicco. Interval temporal logics over strongly discrete linear orders: Expressiveness and complexity. Theoretical Computer Science (TCS), 560(Part 3):269-291, 2014 (DOI: 10.1016/j.tcs.2014.03.033, online since April 2014).
    *** Journal version of ECAI 2012 and GandALF 2012.
  11. full text BibTeX D. Bresolin, D. Della Monica, V. Goranko, A. Montanari, and G. Sciavicco. The dark side of Interval Temporal Logic: marking the undecidability border. Annals of Mathematics and Artificial Intelligence (AMAI), 71(1-3):41-83, 2014 (DOI: 10.1007/s10472-013-9376-4, online since September 2013).
    *** Journal version of TIME 2011 - The Dark Side.
  12. full text BibTeX D. Bresolin, D. Della Monica, A. Montanari, and G. Sciavicco. The Light Side of Interval Temporal Logic: the Bernays-Schönfinkel fragment of CDT. Annals of Mathematics and Artificial Intelligence (AMAI), 71(1-3):11-39, 2014 (DOI: 10.1007/s10472-013-9337-y, online since March 2013).
    *** Journal version of TIME 2011 - The Light Side.
  13. full text BibTeX D. Bresolin, D. Della Monica, V. Goranko, A. Montanari, and G. Sciavicco. Metric Propositional Neighborhood Logics on Natural Numbers. Software and Systems Modeling (SoSyM), 12(2):245-264, 2013.
    *** Journal version of ECAI 2010.
    *** Winner of the Young researcher award for 2011 - University of Udine (Italy).
  14. full text BibTeX D. Della Monica, V. Goranko, A. Montanari, and G. Sciavicco. Crossing the Undecidability Border with Extensions of Propositional Neighborhood Logic over Natural Numbers. Journal of Universal Computer Science (JUCS), 18(20):2798-2831, 2012.
    *** Journal version of HyLo 2010 and STeDY 2010.

  15. [download .bib file]

    Book Chapter [top]

  16. full text BibTeX D. Della Monica, A. Montanari, and P. Sala. The importance of the past in interval temporal logics: the case of Propositional Neighborhood Logic. In Alexander Artikis, Robert Craven, Nihan Kesim Cicekli, Babak Sadighi, and Kostas Stathis, editors, Logic Programs, Norms and Action - Essays in Honor of Marek J. Sergot on the Occasion of His 60th Birthday, volume 7360 of Lecture Notes in Computer Science, pages 79-102. Springer Berlin / Heidelberg, 2012.


  17. Invited papers [top]

  18. full text BibTeX D. Della Monica, V. Goranko, A. Montanari, and G. Sciavicco. Interval Temporal Logics: a Journey. Bulletin of the EATCS (BEATCS), Volume 105, October 2011.


  19. Electronic journals [top]

  20. full text slides BibTeX D. Della Monica, M. Napoli, and M. Parente. On a Logic for Coalitional Games with Priced-Resource Agents. Electronic Notes in Theoretical Computer Science (ENTCS), 278:215-228, 2011.
  21. full text slides BibTeX D. Della Monica, V. Goranko, and G. Sciavicco. Hybrid Metric Propositional Neighborhood Logics with Interval Length Binders. Electronic Notes in Theoretical Computer Science (ENTCS), 273:3-19, 2011.
  22. full text BibTeX D. Bresolin, D. Della Monica, V. Goranko, A. Montanari, and G. Sciavicco. Undecidability of the Logic of Overlap Relation over Discrete Linear Orderings. Electronic Notes in Theoretical Computer Science (ENTCS), 262:65-81, 2010.
    *** Proc. of the 6th Workshop on Methods for Modalities (M4M-6 2009).


  23. Conference and workshop proceedings Click here to display ISI and Scopus codes [top]


    2023 | 2020 | 2019 | 2018 | 2017 | 2016 | 2015 | 2014 | 2013 | 2012 | 2011 | 2010 | 2009 | 2008

    2023 [up to conference and workshop proceedings]

  24. full text BibTeX Dario Della Monica, Angelo Montanari, Gabriele Puppis, and Pietro Sala. The Logic of Prefixes and Suffixes is Elementary under Homogeneity. In Proc. of the 38th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), 2023.
  25. 2020 [up to conference and workshop proceedings]

  26. full text BibTeX Dario Della Monica, Nicola Gigante, Salvatore La Torre, and Angelo Montanari. Complexity of qualitative timeline-based planning. In Proc. of the 27th International Symposium on Temporal Representation and Reasoning (TIME), 2020.
  27. full text BibTeX Willem Conradie, Dario Della Monica, Emilio Muñoz-Velasco, and Guido Sciavicco. An Approach to Fuzzy Modal Logic of Time Intervals. In Proc. of the 24th European Conference on Artificial Intelligence (ECAI), 2020.
  28. 2019 [up to conference and workshop proceedings]

  29. full text BibTeX D. Della Monica, A. Montanari, A. Murano, and G. Sciavicco. Ultimately-periodic interval model checking for temporal dataset evaluation. In Proc. of the 5th Global Conference on Artificial Intelligence (GCAI), 2019.
  30. 2018 [up to conference and workshop proceedings]

  31. full text BibTeX D. Della Monica, N. Gigante, A. Montanari, and P. Sala. A novel automata-theoretic approach to timeline-based planning. In Proc. of the 16th International Conference on Principles of Knowledge Representation and Reasoning (KR), 2018.
  32. full text slides BibTeX D. Della Monica and A. Murano. Parity-energy ATL for qualitative and quantitative reasoning in MAS. In Proc. of the 17th International Conference on Autonomous Agents and Multiagent Systems (AAMAS), 2018.
    *** The published version of this paper (in the Proceedings of the 17th AAMAS, pages 1441--1449, 2018) contains an error in the statement of Theorem 5.1: in the officially published version, the complexity of the problem for mixed instances is mistakenly claimed to be in NPTIME; however, we are only able to show a higher upper bound, namely PNP. We thank Stéphane Demri and Francesco Belardinelli for spotting the mistake and kindly drawing our attention to it.
  33. 2017 [up to conference and workshop proceedings]

  34. full text BibTeX D. Della Monica, N. Gigante, A. Montanari, P. Sala, and G. Sciavicco. Bounded Timed Propositional Temporal Logic with Past Captures Timeline-based Planning with Bounded Constraints. In Proc. of the 26th International Joint Conference on Artificial Intelligence (IJCAI), 2017.
  35. full text BibTeX A. Francalanza, L. Aceto, A. Achilleos, D.P. Attard, I. Cassar, D. Della Monica, and A. Ingólfsdóttir. A Foundation for Runtime Monitoring. In Proc. of the 17th International Conference on Runtime Verification (RV), 2017.
  36. full text BibTeX D. Della Monica, D. de Frutos-Escrig, A. Montanari, A. Murano, and G. Sciavicco. Evaluation of Temporal Datasets via Interval Temporal Logic Model Checking. In Proc. of the 24th International Symposium on Temporal Representation and Reasoning (TIME), 2017.
  37. full text BibTeX D. Della Monica, A. Montanari, and P. Sala. Beyond omegaBS-regular Languages: omegaT-regular Expressions and Counter-Check Automata. In Proc. of the 8th International Symposium on Games, Automata, Logics and Formal Verification (GandALF), 2017.
  38. 2016 [up to conference and workshop proceedings]

  39. full text slides BibTeX D. Della Monica, A. Montanari, A. Murano, and P. Sala. Prompt Interval Temporal Logic. In Proc. of the 15th European Conference On Logics In Artificial Intelligence (JELIA), 2016.
  40. 2015 [up to conference and workshop proceedings]

  41. full text BibTeX D. Romero-Hérnandez, D. de Frutos-Escrig, and D. Della Monica. Proving Continuity of Coinductive Global Bisimulation Distances: A Never Ending Story. In Proc. of the 15th Jornadas sobre PROgramación y LEnguajes (PROLE), EPTCS, 2015.
  42. full text slides BibTeX L. Aceto, D. Della Monica, I. Fábregas, and A. Ingólfsdóttir. When are prime formulae characteristic?. In Proc. of the 40th International Symposium on Mathematical Foundations of Computer Science (MFCS), LNCS 9234, pages 76-88, 2015.
  43. full text BibTeX D. Bresolin, D. Della Monica, A. Montanari, P. Sala, and G. Sciavicco. On the Complexity of Fragments of the Modal Logic of Allen's Relations over Dense Structures. In Proc. of the 9th International Conference on Language and Automata Theory and Applications (LATA), 2015.
  44. 2014 [up to conference and workshop proceedings]

  45. full text slides BibTeX L. Aceto, D. Della Monica, A. Ingólfsdóttir, A. Montanari, and G. Sciavicco. On the expressiveness of the interval logic of Allen's relations over finite and discrete linear orders. In Proc. of the 14th European Conference on Logics in Artificial Intelligence (JELIA), LNAI 8761, pages 267-281, 2014.
  46. full text BibTeX D. Della Monica, A. Montanari, G. Sciavicco, and D. Tishkovsky. First steps towards automated synthesis of tableau systems for interval temporal logics. In Proc. of the 5th International Conference on Computational Logics, Algebras, Programming, Tools, and Benchmarking (COMPUTATION TOOLS), pages 32-37, 2014.
    *** Best paper award [html] [pdf].
  47. 2013 [up to conference and workshop proceedings]

  48. full text BibTeX L. Aceto, D. Della Monica, A. Ingólfsdóttir, A. Montanari, and G. Sciavicco. An Algorithm for Enumerating Maximal Models of Horn Theories with an Application to Modal Logics. In Proc. of the 19th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning (LPAR), LNCS 8312, pages 1-17, Stellenbosch, South Africa, December 15th-19th, Springer, 2013.
  49. full text slides BibTeX D. Della Monica, M. Napoli, and M. Parente. Model checking coalitional games in shortage resource scenarios. In Proc. of the 4th International International Symposium on Games, Automata, Logics and Formal Verification (GandALF), Borca di Cadore, Dolomites, Italy, August 29th-31st, 2013.
  50. full text BibTeX L. Aceto, D. Della Monica, A. Ingólfsdóttir, A. Montanari, and G. Sciavicco. A complete classification of the expressiveness of interval logics of Allen's relations over dense linear orders. In Proc. of the 20th International Symposium on Temporal Representation and Reasoning (TIME), Pensacola, FL (USA), September 26th-28th, pages 65-72, 2013.
  51. full text BibTeX D. Bresolin, D. Della Monica, A. Montanari, and G. Sciavicco. A Tableau System for Right Propositional Neighborhood Logic over Finite Linear Orders: an Implementation. In Proc. of the 22nd International Conference on Automated Reasoning with Analytic Tableaux and Related Methods (TABLEAUX), Nancy, France, September 16th-19th, LNCS 8123, pages 74-80, 2013.
  52. 2012 [up to conference and workshop proceedings]

  53. full text slides BibTeX D. Bresolin, D. Della Monica, A. Montanari, P. Sala, and G. Sciavicco. Interval Temporal Logics over Strongly Discrete Linear Orders: the Complete Picture. In Proc. of the 3rd International Symposium on Games, Automata, Logics and Formal Verification (GandALF), Naples, Italy, September 6th-8th, 2012.
  54. full text BibTeX D. Bresolin, D. Della Monica, A. Montanari, P. Sala, and G. Sciavicco. Interval Temporal Logics over Finite Linear Orders: the Complete Picture. In Proc. of the 20th European Conference on Artificial Intelligence (ECAI), Montpellier, France, August, 2012.
  55. full text BibTeX D. Della Monica and G. Lenzi. On a Priced Resource-Bounded Alternating μ-calculus. In Proc. of the 4th International Conference on Agents and Artificial Intelligence (ICAART), pages 222-227, Vilamoura, Algarve, Portugal, February 2012.
  56. 2011 [up to conference and workshop proceedings]

  57. full text BibTeX D. Bresolin, D. Della Monica, A. Montanari, and G. Sciavicco. The light side of Interval Temporal Logic: the Bernays-Schonfinkel's fragment of CDT. In Proc. of the 18th International Symposium on Temporal Representation and Reasoning (TIME), pages 123-130, Lübeck, Germany, September 2011.
  58. full text BibTeX D. Bresolin, D. Della Monica, V. Goranko, A. Montanari, and G. Sciavicco. The dark side of Interval Temporal Logic: sharpening the undecidability border. In Proc. of the 18th International Symposium on Temporal Representation and Reasoning (TIME), pages 131-138, Lübeck, Germany, September 2011.
  59. full text BibTeX D. Della Monica, V. Goranko, A. Montanari, and G. Sciavicco. Expressiveness of the Interval Logics of Allen's Relations on the Class of all Linear Orders: Complete Classification. In Proc. of the 22nd International Joint Conference on Artificial Intelligence (IJCAI), pages 845-850, Barcelona, Spain, July 2011.
  60. 2010 [up to conference and workshop proceedings]

  61. full text BibTeX D. Bresolin, D. Della Monica, A. Montanari, P. Sala, and G. Sciavicco. A decidable spatial generalization of Metric Interval Temporal Logic. In N. Markey and J. Wijsen, editors, Proc. of the 17th International Symposium on Temporal Representation and Reasoning (TIME), pages 95-102, Paris, France. IEEE Computer Society Press, September 2010.
  62. full text slides BibTeX D. Bresolin, D. Della Monica, V. Goranko, A. Montanari, and G. Sciavicco. Metric Propositional Neighborhood Logics: Expressiveness, Decidability, and Undecidability. In Proc. of the 19th European Conference on Artificial Intelligence (ECAI), pages 695-700, Lisbon, Portugal, August 2010.
  63. full text slides BibTeX D. Della Monica and G. Sciavicco. On First-Order Propositional Neighborhood Logics: a First Attempt. In Proc. of the ECAI 2010 Workshop on Spatio-Temporal Dynamics (STeDY), pages 43-48, Lisbon, Portugal, August 2010.
  64. 2009 [up to conference and workshop proceedings]

  65. full text slides BibTeX D. Bresolin, D. Della Monica, V. Goranko, A. Montanari, and G. Sciavicco. Undecidability of Interval Temporal Logics with the Overlap Modality. In C. Lutz and J.F. Raskin, editors, Proc. of the 16th International Symposium on Temporal Representation and Reasoning (TIME), pages 88-95. IEEE Computer Society Press, 2009.
  66. 2008 [up to conference and workshop proceedings]

  67. full text BibTeX D. Bresolin, D. Della Monica, V. Goranko, A. Montanari, and G. Sciavicco. Decidable and Undecidable Fragments of Halpern and Shoham's Interval Temporal Logic: Towards a Complete Classification. In I. Cervesato, H. Veith, and A. Voronkov, editors, Proc. of the 15th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning (LPAR), LNCS 5330, pages 590-604. Springer, 2008.


    Workshop notes (unofficial publications – without proceedings) BibTeX Click here to display ISI and Scopus codes [top]

  1. full text BibTeX Dario Della Monica, Giovanni Pagliarini, Guido Sciavicco, and Ionel Eduard Stan. Decision Trees with a Modal Flavor. 21st International Conference of the Italian Association for Artificial Intelligence (AIxIA), 2022.
  2. full text BibTeX Dario Della Monica, Angelo Montanari, and Pietro Sala. Extended omega-Regular Languages and Interval Temporal Logic. 22nd Italian Conference on Theoretical Computer Science (ICTCS), 2021.
  3. full text BibTeX Dylan Bellier, Massimo Benerecetti, Dario Della Monica, and Fabio Mogavero. Good-for-Game QPTL: An Alternating Hodges Semantics. arXiv , eprint: 2104.06085, primaryClass: cs.LO, 2021.
  4. full text BibTeX Dario Della Monica, Angelo Montanari, Guido Sciavicco, and Ionel Eduard Stan. A Note on Ultimately-Periodic Finite Interval Temporal Logic Model Checking. 2nd Workshop on Artificial Intelligence and fOrmal VERification, Logic, Automata, and sYnthesis (OVERLAY), 2020.
  5. full text BibTeX Andrea Brunello, Dario Della Monica, Angelo Montanari, and Andrea Urgolo. Learning How to Monitor: Pairing Monitoring and Learning for Online System Verification. 2nd Workshop on Artificial Intelligence and fOrmal VERification, Logic, Automata, and sYnthesis (OVERLAY), 2020.
  6. full text BibTeX Andrea Brunello, Dario Della Monica, Angelo Montanari, and Andrea Urgolo. Learning to Monitor: a Novel Framework for Online System Verification. Reasoning about ACtions and Events over Streams (RACES) within KR, 2020.
  7. full text BibTeX Willem Conradie, Dario Della Monica, Emilio Muñoz-Velasco, Guido Sciavicco, and Ionel Eduard Stan. Time Series Checking with Fuzzy Interval Temporal Logics. 21st Italian Conference on Theoretical Computer Science (ICTCS), 2020.
  8. full text slides BibTeX D. Della Monica and A. Francalanza. Pushing runtime verification to the limit: May process semantics be with us. 1st Workshop on Artificial Intelligence and fOrmal VERification, Logic, Automata, and sYnthesis (OVERLAY), 2019.
  9. full text BibTeX A. Brunello, D. Della Monica, and A. Montanari. Pairing monitoring with machine learning for smart system verification and predictive maintenance. 1st Workshop on Artificial Intelligence and fOrmal VERification, Logic, Automata, and sYnthesis (OVERLAY), 2019.
  10. full text slides BibTeX D. Della Monica and A. Murano. Parity-energy ATL for qualitative and quantitative reasoning in MAS. Workshop on Formal Methods & Logical Aspects of Multi-Agent Systems (FMLAMAS), 2018.
  11. full text BibTeX D. Barozzini, D. Della Monica, A. Montanari, and P. Sala. Counter-queue automata with an application to a meaningful extension of omega-regular languages. 18th Italian Conference on Theoretical Computer Science (ICTCS), 2017.
  12. full text BibTeX E. Cominato, D. Della Monica, A. Montanari, and G. Sciavicco. A model checker for interval temporal logic over finite structures. 18th Italian Conference on Theoretical Computer Science (ICTCS), 2017.
  13. full text slides BibTeX D. Della Monica and A. Francalanza. Towards A Hybrid Approach to Software Verification. 27th Nordic Workshop on Programming Theory (NWPT), October, 21st - 23rd 2015. (Extended Abstract)
  14. full text slides BibTeX D. Bresolin, D. Della Monica, A. Montanari, and G. Sciavicco. A Tableau System for Right Propositional Neighborhood Logic over Finite Linear Orders: an Implementation. 28th Italian Conference on Computational Logic (CILC), September, 25th - 27th 2013.
  15. full text BibTeX L. Aceto, D. Della Monica, A. Ingólfsdóttir, A. Montanari, and Guido Sciavicco. A complete classification of the expressiveness of interval logics of Allen's relations over dense linear order. 14th Italian Conference on Theoretical Computer Science (ICTCS), Palermo, Italy, September 9th - 11th, 2013. (extended abstract)
  16. full text slides BibTeX D. Della Monica, M. Napoli, and M. Parente. Model Checking Coalitional Games with Priced-Resource Agents. Annual Workshop of the ESF Networking Programme on Games for Design and Verification (GAMES), September, 7th - 12th 2012. (extended abstract)
  17. full text slides BibTeX D. Della Monica, M. Napoli, and M. Parente. On a Logic for Coalitional Games with Priced-Resource Agents. Annual Workshop of the ESF Networking Programme on Games for Design and Verification (GAMES), August, 31st - September, 3rd 2011. (extended abstract)
  18. full text slides BibTeX D. Della Monica, V. Goranko, A. Montanari, and G. Sciavicco. Expressiveness of the Interval Logics of Allen's Relations on the Class of all Linear Orders: Complete Classification. Annual Workshop of the ESF Networking Programme on Games for Design and Verification (GAMES), August, 31st - September, 3rd 2011. (extended abstract)
  19. full text slides BibTeX D. Della Monica, M. Napoli, and M. Parente. Coalitional Games with Priced-Resource Agents. 26th Italian Conference on Computational Logic (CILC), August, 31st - September, 2nd 2011. (short paper)
    *** Published online on CEUR-WS.org (ISSN 1613-0073, URN: nbn:de:0074-810-0), 810:341-347, 2011.
  20. full text slides BibTeX D. Bresolin, D. Della Monica, V. Goranko, A. Montanari, and G. Sciavicco. Metric Propositional Neighborhood Logics: Expressiveness, Decidability, and Undecidability. Annual Workshop of the ESF Networking Programme on Games for Design and Verification (GAMES), September 2010. (extended abstract)
  21. full text slides BibTeX D. Bresolin, D. Della Monica, V. Goranko, A. Montanari, and G. Sciavicco. Undecidability of the Logic of the Overlap Relation over Discrete Linear Orderings. Annual Workshop of the ESF Networking Programme on Games for Design and Verification (GAMES), September 2009. (extended abstract)

    PhD thesis [top]

  • full text slides BibTeX D. Della Monica. Expressiveness, decidability, and undecidability of Interval Temporal Logic. University of Udine, 2011.
    *** Winner of the GULP prize for the best PhD dissertation in the area of Computational Logic for the years 2010-2011.

    Master thesis (in Italian) [top]

  • full text BibTeX D. Della Monica. Una procedura di model checking in un dominio lineare astratto per la verifica di programmi C con array (A model checking procedure in abstract linear domain for the verification of C program with array). Universita' degli Studi di Napoli "Federico II", October 2007.