Publications

Journals

Finite failure is and-compositional,  with Giorgio Levi. Journal  of  Logic and  Computation  6(7) , pp. 753-776, 1997.

Ragionando sul fallimento finito e le computazioni infinite usando l'interpretazione astratta, Bollettino U.M.I., 8, vol. III-A, pp. 351-354, 2000.

Enhancing the Expressive Power of the U-Datalog Language,  with Elisa Bertino and Barbara Catania. Theory and Practice of Logic Programming,  1(1), pp. 105-122, 2001.

Abstract Interpretation based Verification of Logic Programs,  with Marco Comini, Giorgio Levi and Paolo Volpe. Science  of  Computer Programming, 49 (1-3), pp. 89-123, 2003.

 An Abstract Interpretation Framework to reason on Finite Failure, Theoretical  Computer Science,  290(1), pp. 863-936, 2003.

 Finite-Tree Analysis for Constraint Logic-Based Languages, with Roberto Bagnara, Pat Hill and Enea Zaffanella, Information and  Computation, 2(193), pp. 84-116, 2004.
 
On the verification of finite failure, with Giorgio Levi. Journal of Computer and System Sciences, 71(4), pp. 535-575, 2005.


Conferences

 Finite Failure is AND-Compositional, with Giorgio Levi. In Proceding of the GULP-PRODE'94, M. Alpuente, R. Barbuti, I. Ramos editors, vol.1, pp 464-478, 1994.

 
A Hierarchy of Semantics for Normal Constraint Logic Programs, with Francois Fages. In Proceding of the Fifth International Conference on Algebraic and Logic Programming (ALP 96), vol. 1139 of  Lecture Notes in Computer Science, M. Hanus, M. Rodriguez-Artalejo, editors, pp. 77-91, 1996.


 Analysis of normal logic programs, with Francois Fages. In Proceding of the Static Analysis Symposium (SAS 98),  vol. 1503 of  Lecture Notes in Computer Science, G. Levi, editor, pp. 82-98, 1998.

 
Analysis of normal logic programs (extended abstract), with Francois Fages. In Proceding of the Sixth Italian Conference on Theoretical Computer Science, vol. 1,  P. Degano, U. Vaccaro, G. Pirillo editors, World Scientific, pp. 328-330, Prato 1998.


Aproximating the Well-Founded Semantics for Normal Logic Programs using Abstract Interpretation, with Ernesto Lastres, Rene' Moreno and Fausto Spoto.   In Proceding of the   APPIA-GULP-PRODE'98, J.L. Freire-Nistal, M. Falaschi, M. Vilares-Ferro editors, vol. 1, pp. 433-441, A Coruna 1998.


A fixpoint semantics for reasoning about finite failure. In Proceding of the International Conference on Logic for Programming and Automated Reasoning (LPAR 99), vol. 1705 of Lecture Notes in Artificial Intelligence,  Harald Ganzinger, David McAllester,  Andrei Voronkov, editors, pp. 238-257, Tbilisi 1999.
Also in Proceding of the  APPIA-GULP-PRODE'99, vol. 1, pp. 529-543, 1999.

On the verification of finite failure, with  Giorgio Levi. In Proceedings of the International Conference on Principles and Practice of Declarative Programming (PPDP 99), vol. 1702 of Lecture Notes in Computer Science, G.Nadathur, editor,  pp. 311-327,  1999.
Also in Proceedings of the APPIA-GULP-PRODE'99, vol. 1, pp. 197-211, L'Aquila, 1999.


Abstract interpretation based verification of logic programs, with Marco Comini, Giorgio Levi and Paolo Volpe.  In Proceedings of the Workshop on Verification of Logic Programs, vol. 30 of Electronic Notes of Theoretical Computer Science, pp. 22-38 , 1999.
Also in Proceedings of the 8th International Workshop on Functional and Logic Programming,  R. Echahed editor, pages 147--159, France, 1999.



An Abstract Interpretation approach to Termination of Logic Programs. In  Proceedings of the Conference on Logic for Programming and Automated Reasoning (LPAR '00), vol. 1955 of Lecture Notes  in Artificial Intelligence, Michel Parigot, Andrei Voronkov, editors, pp. 362-380, 2000.
Also in Proceedings of the APPIA-GULP-PRODE'00, vol. 1, M.C. Meo and M. Villares-Ferro editors, pp. 35-50, 2000.


Logic programs as specifications in the inductive verification of logic programs, with Marco Comini and Giorgio Levi. In Selected Papers from the Joint Conference APPIA-GULP-PRODE, n. 48 of  Electronic Notes of Theoretical Computer Science, A. Dovier, M. C. Meo, and A. Omicini, editors, pp 131-146, 2000.


Assertion based Inductive Verification Methods for Logic Programs, with Marco Comini and Giorgio Levi. In Selected Papers from the Proceedings of MFCSIT'2000,  n. 40 of Electronic Notes of Theoretical Computer Science, pp. 52-69 A. K. Seda editor.
Also in Proceedings of the MFCSIT'2000, vol. 40, pp. 1-18, 2001.


 Finite-Tree Analysis for Constraint Logic-Based Languages, with Roberto Bagnara, Pat Hill and Enea Zaffanella. In  Proceedings of the 8th International Symposium on Static Analysis (SAS '01), vol. 2126 of Lecture Notes in Computer Science, P. Cousot editor, pp. 165-184, 2001. 
Also in Proceedings of the Joint Conference APPIA-GULP-PRODE, vol. 1, pp. 63-79, Evora, 2001.


Boolean Functions for Finite-Tree Dependencies, with Roberto Bagnara, Pat Hill and Enea Zaffanella. In  Proceedings of the International Conference on Logic for Programming, Artificial Intelligence and Reasoning (LPAR '01), vol. 2250 of Lecture Notes in Artificial Intelligence,   R. Nieuwenhuis and A. Voronkov editors, pp. 579-594, 2001.
Also in Proceedings of the Joint Conference APPIA-GULP-PRODE, vol. 1, pp.  81-96,  Evora 2001.



How to transform an analyzer into a verifier, with Marco Comini and Giorgio Levi. In  Proceedings of the International Conference on Logic for Programming, Artificial Intelligence and Reasoning (LPAR '01), vol. 2250 of Lecture Notes in Artificial Intelligence, R. Nieuwenhuis and A. Voronkov editors, pp. 1-16,  2001. Also in Proceedings of the Joint Conference APPIA-GULP-PRODE, vol. 1, pp.131-148, Evora, 2001.


An experiment in type inference and verification by abstract interpretation, with Giorgio Levi. In  Proceedings of the International Workshop on Verification, Model Checking and Abstract Interpretation (VMCAI '02), vol. 2294 of Lecture Notes in Computer Science, A. Cortesi, editor, pp. 225-239, 2002.

Properties of a type abstract interpreter with Giorgio Levi. In  Proceedings of the International Workshop on Verification, Model Checking and Abstract Interpretation,  (VMCAI '03), vol. 2500 of Lecture Notes in Computer Science, Lenore D. Zuck, Paul C. Attie, Agostino Cortesi and Supratik Mukhopadhyay editors, pp. 103-118, 2003.

 A new Occurrence Counting analysis for BioAmbients with Francesca Levi.  In  Proceedings of the Third Asian Symposium (APLAS '05), vol. 3780  of Lecture Notes in Computer Science, Kwangkeun Yi editor, pp. 381-400, 2005.

An Analysis for Proving Temporal Properties of Biological Systems with Francesca Levi  In  Proceedings of the Fourth Asian Symposium (APLAS '06), vol. 4279  of Lecture Notes in Computer Science, Naoki Kobayashi editor, pp. 234-252, 2006.

 Approximating Probabilistic Behaviours of Biological Systems using Abstract Interpretation with Alessio Coletta and Francesca Levi.  In  Proceedings of the Workshop From Biology to Concurrency and back (FBTC'08),   Electronic Notes in Computer Science, Nicola Cannata Emanuela Merelli and Irek Uldowski Naoki Kobayashi editor, 2008.