Research Papers (pdf files available)


G. Filé and F. Ranzato. Improving abstract interpretations by systematic lifting to the powerset. In M. Bruynooghe, editor, Proceedings of the 1994 International Logic Programming Symposium (ILPS'94), Ithaca, NY, pages 655-669. The MIT Press, 1994.

A. Cortesi, R. Giacobazzi, G. Filé, C. Palamidessi, and F. Ranzato. Complementation in abstract interpretation. In A. Mycroft, editor, Proceedings of the 2nd International Static Analysis Symposium (SAS'95), Glasgow, UK, LNCS vol. 983, pages 100-117. Springer-Verlag, 1995.

R. Giacobazzi and F. Ranzato. Functional dependencies and Moore-set completions of abstract interpretations and semantics. In J. Lloyd, editor, Proceedings of the 1995 International Logic Programming Symposium (ILPS'95), Portland, OR, pages 321-335. The MIT Press, 1995.

R. Giacobazzi and F. Ranzato. Compositional optimization of disjunctive abstract interpretations. In H.R. Nielson, editor, Proceedings of the 6th European Symposium on Programming (ESOP'96), Linkoping, SE. LNCS vol. 1058, pages 141-155. Springer-Verlag, 1996.

G. Filé, R. Giacobazzi, and F. Ranzato. A unifying view of abstract domain design. ACM Computing Surveys, 28(2):333-336, 1996.

G. Filé and F. Ranzato. Complementation of abstract domains made easy. In M. Maher, editor, Proceedings of the 1996 Joint International Conference and Symposium on Logic Programming (JICSLP'96), Bonn, DE, pages 348-362. The MIT Press, 1996.

R. Giacobazzi and F. Ranzato. Complementing logic program semantics. In M. Hanus and M. Rodríguez-Artalejo, editors, Proceedings of the 5th International Conference on Algebraic and Logic Programming (ALP'96), Aachen, DE. LNCS vol. 1139, pages 238-253. Springer-Verlag, 1996.

R. Giacobazzi, C. Palamidessi, and F. Ranzato. Weak relative pseudo-complements of closure operators. Algebra Universalis, 36(3):405-412, 1996.

A. Cortesi, G. Filé, R. Giacobazzi, C. Palamidessi, and F. Ranzato. Complementation in abstract interpretation. ACM Transactions on Programming Languages and Systems, 19(1):7-47, 1997.

R. Giacobazzi and F. Ranzato. Refining and compressing abstract domains. In P. Degano, R. Gorrieri, and A. Marchetti-Spaccamela, editors, Proceedings of the 24th International Colloquium on Automata, Languages, and Programming (ICALP '97), Bologna, IT. LNCS vol. 1256, pages 771-781. Springer-Verlag, 1997.

R. Giacobazzi and F. Ranzato. Completeness in abstract interpretation: a domain perspective. In M. Johnson, editor, Proceedings of the 6th International Conference on Algebraic Methodology and Software Technology (AMAST'97), Sydney, AU. LNCS vol. 1349, pages 231-245. Springer-Verlag, 1997.

R. Giacobazzi and F. Ranzato. On the least complete extension of complete subsemilattices. Algebra Universalis, 38(3):235-237, 1997.

R. Giacobazzi and F. Ranzato. Optimal domains for disjunctive abstract interpretation. Science of Computer Programming, 32(1-3):177-210, 1998.

R. Giacobazzi, F. Ranzato, and F. Scozzari. Complete abstract interpretations made constructive. In L. Brim, J. Gruska, and J. Zlatuska, editors, Proceedings of the 23rd International Symposium on Mathematical Foundations of Computer Science (MFCS'98), Brno, CZ. LNCS vol. 1450, pages 366-377. Springer-Verlag, 1998.

R. Giacobazzi and F. Ranzato. Some properties of complete congruence lattices. Algebra Universalis, 40(2)::189-200, 1998.

R. Giacobazzi, F. Ranzato, and F. Scozzari. Building complete abstract interpretations in a linear logic-based setting. In G. Levi, editor, Proceedings of the 5th International Static Analysis Symposium (SAS'98), Pisa, IT. LNCS vol. 1503, pages 215-229. Springer-Verlag, 1998.

R. Giacobazzi and F. Ranzato. Uniform closures: order-theoretically reconstructing logic program semantics and abstract domain refinements. Information and Computation, 145(2):153-190, 1998.

R. Giacobazzi and F. Ranzato. The reduced relative power operation on abstract domains. Theoretical Computer Science, 216(1-2):159-211, 1999.

G. Filé and F. Ranzato. The powerset operator on abstract interpretations. Theoretical Computer Science, 222(1-2):77-111, 1999.

F. Ranzato. Closures on CPOs form complete lattices. Information and Computation, 152(2):236-249, 1999.

R. Giacobazzi, F. Ranzato, and F. Scozzari. Making abstract interpretations complete. Journal of the ACM, 47(2):361-416, 2000.

F. Ranzato. A counterexample to a result concerning closure operators. Portugaliæ Mathematica, 58(1):121-125, 2001.

F. Ranzato. On the completeness of model checking. In D. Sands, editor, Proceedings of the 10th European Symposium on Programming (ESOP'01), Genova, IT. LNCS vol. 2028, pages 137-154. Springer-Verlag, 2001.

F. Ranzato and F. Tapparo. Making abstract model checking strongly preserving. In M. Hermenegildo and G. Puebla, editors, Proceedings of the 9th International Static Analysis Symposium (SAS'02) , Madrid, ES. LNCS vol. 2477, pages 411-427. Springer-Verlag, 2002.

R. Giacobazzi and F. Ranzato. States vs. traces in model checking by abstract interpretation. In M. Hermenegildo and G. Puebla, editors, Proceedings of the 9th International Static Analysis Symposium (SAS'02) , Madrid, ES. LNCS vol. 2477, pages 461-476. Springer-Verlag, 2002.

F. Ranzato. Pseudocomplements of closure operators on posets. Discrete Mathematics, 248(1-3):143-155, 2002.

F. Ranzato and F. Tapparo. Strong preservation as completeness in abstract interpretation. In D. Schmidt, editor, Proceedings of the 13th European Symposium on Programming (ESOP'04), Barcelona, ES. LNCS vol. 2986, pages 18-32. Springer-Verlag, 2004.

R. Giacobazzi, F. Ranzato, and F. Scozzari. Making abstract domains condensing. ACM Transactions on Computational Logic, 6(1):33-60, 2005.

F. Ranzato and F. Tapparo. An abstract interpretation-based refinement algorithm for strong preservation. In N. Halbwachs and L. Zuck, editors, Proceedings of the 11th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'05), Edinburgh, U.K. LNCS vol. 3440, pages 140-156, 2005.

F. Ranzato and F. Tapparo. An abstract interpretation perspective on linear vs. branching time. In K. Yi editor, Proceedings of the 3rd Asian Symposium on Programming Languages and Systems (APLAS'05), Tsukuba, Japan, LNCS vol. 3780, pages 69-85, 2005.

R. Giacobazzi and F. Ranzato. Incompleteness of states w.r.t. traces in model checking. Information and Computation, 204(3):376-407, 2006.

F. Ranzato and F. Tapparo. Strong preservation of temporal fixpoint-based operators by abstract interpretation. In E.A. Emerson and K.S. Namjoshi editors, Proceedings of the 7th International Conference on Verification, Model Checking and Abstract Interpretation (VMCAI'06), Charleston, SC, LNCS vol. 3855, pages 332-347, 2006.

F. Ranzato and F. Tapparo. A new efficient simulation equivalence algorithm. In L. Ong editor, Proceedings of the 22nd Annual IEEE Symposium on Logic in Computer Science (LICS'07), Wroclaw, Poland, IEEE Press, pages 171-180, 2007.

F. Ranzato and F. Tapparo. Generalized strong preservation by abstract interpretation. Journal of Logic and Computation, 17(1):157-197, 2007.

F. Ranzato, O. Rossi Doria and F. Tapparo. A forward-backward abstraction refinement algorithm. In Proceedings of the 9th International Conference on Verification, Model Checking and Abstract Interpretation (VMCAI'08), San Francisco, CA, LNCS vol. 4905, pages 248-262, 2008.

F. Ranzato and F. Tapparo. Generalizing the Paige-Tarjan algorithm by abstract interpretation. Information and Computation, 206(5):620-651, 2008.

L. De Nardo, F. Ranzato and F. Tapparo. The subgraph similarity problem. IEEE Transactions on Knowledge and Data Engineering, 21(5):748-749, 2009.

S. Crafa, F. Ranzato and F. Tapparo. Saving space in a time efficient simulation algorithm. In Proceedings of the 9th International Conference on Application of Concurrency to System Design (ACSD'09), Augsburg, Germany, IEEE Press, pages 60-69, 2009.

F. Ranzato and F. Tapparo. A time and space efficient simulation algorithm. Short Talk at the 24th Annual IEEE Symposium on Logic in Computer Science (LICS'09), Los Angeles, CA, 2009.

F. Ranzato and F. Tapparo. Computing stuttering simulations. In Proceedings of the 20th International Conference on Concurrency Theory (CONCUR'09), Bologna, Italy, LNCS vol. 5710, pages 542-556, Springer, 2009.

F. Ranzato and F. Tapparo. An efficient simulation algorithm based on abstract interpretation. Information and Computation, 208(1):1-22, 2010.

R. Giacobazzi and F. Ranzato. Example-guided abstraction simplification. In Proceedings of the 37th International Colloquium on Automata, Languages, and Programming (ICALP '10), Bordeaux, France. LNCS vol. 6199, pages 211-222, Springer, 2010.

G. Delzanno, R. Giacobazzi and F. Ranzato. Static analysis, abstract interpretation and verification in (constraint logic) programming. In A 25-Year Perspective onf Logic Programming, LNCS vol. 6125, pages 136-158, Springer, 2010.

S. Crafa, F. Ranzato and F. Tapparo. Saving space in a time efficient simulation algorithm. Fundamenta Informaticae, 108(1-2):23-42, 2011.

S. Crafa and F. Ranzato. Probabilistic bisimulation and simulation algorithms by abstract interpretation. In L. Aceto, M. Henzinger and J. Sgall editors, Proceedings of the 38th International Colloquium on Automata, Languages, and Programming (ICALP '11), Zurich, Switzerland. LNCS vol. 6756, pages 295-306, Springer, 2011.

S. Crafa and F. Ranzato. A spectrum of behavioral relations over LTSs on probability distributions. In J.-P. Katoen and B. Konig editors, Proceedings of the 22nd International Conference on Concurrency Theory (CONCUR'11), Aachen, Germany. LNCS vol. 6901, pages 124-139, Springer, 2011.

S. Crafa and F. Ranzato. Bisimulation and simulation algorithms on probabilistic transition systems by abstract interpretation. Formal Methods in System Design, 40(3):356-376, 2012.

F. Ranzato. Complete abstractions everywhere. Invited paper. In R. Giacobazzi, J. Berdine and I. Mastroeni editors, Proceedings of the 14th International Conference on Verification, Model Checking and Abstract Interpretation (VMCAI'13), Rome, IT, LNCS vol. 7737, pages 15-26, Springer, 2013. Slides.

F. Ranzato. A more efficient simulation algorithm on Kripke structures. In K. Chatterjee and J. Sgall editors, Proceedings of the 38th International Symposium on Mathematical Foundations of Computer Science (MFCS'13), IST Austria, Klosterneuburg, AT, LNCS vol. 8087, pages 753-764, Springer, 2013.

S. Dissegna, F. Logozzo and F. Ranzato. Tracing compilation by abstract interpretation. In S. Jagannathan and P. Sewell, editors, Proceedings of the 41st Annual ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages (POPL'14), San Diego, CA, pages 47-59, ACM Press, 2014. Video of the POPL talk in San Diego.

F. Ranzato. An efficient simulation algorithm on Kripke structures. Acta Informatica, 51(2):107-125, 2014.

R. Giacobazzi and F. Ranzato. Correctness kernels of abstract interpretations. Information and Computation, 237:187-203, 2014.

S. Crafa and F. Ranzato. Logical characterizations of behavioral relations on transition systems of probability distributions. ACM Transactions on Computational Logic, 16(1), Article No. 2, 2015.

R. Giacobazzi, F. Logozzo and F. Ranzato. Analyzing program analyses. In S. Rajamani and D. Walker, editors, Proceedings of the 42nd Annual ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages (POPL'15), Mumbai, India, pages 261-273, ACM Press, 2015. Video of the POPL talk in Mumbai.

S. Dissegna, F. Logozzo and F. Ranzato. An abstract interpretation-based model of tracing just-in-time compilation. ACM Transactions on Programming Languages and Systems, 38(2), Article No. 7, 50 pages, 2016.

F. Ranzato. Abstract interpretation of supermodular games. In X. Rival editor, Proceedings of the 23rd International Static Analysis Symposium (SAS'16), Edinburgh, UK, LNCS vol. 9837, pages 403-423, Springer, 2016.

F. Ranzato. A new characterization of complete Heyting and co-Heyting algebras. Logical Methods in Computer Science, to appear, 2017.

F. Ranzato. Abstracting Nash equilibria of supermodular games. Formal Methods in System Design, to appear, 2017.

F. Ranzato editor. Static Analysis, Proceedings of the 24th International Symposium, SAS 2017, New York, NY, USA, August 30 - September 1, 2017, Lecture Notes in Computer Science vol. 10422, to appear, 2017.



Copyright Notice

The documents distributed have been provided by the contributing authors as a means to ensure timely dissemination of technical work on a noncommercial basis. Copyright and all rights therein are maintained by the authors or by other copyright holders, notwithstanding that they have offered their works here electronically. It is understood that all persons copying this information will adhere to the terms and constraints invoked by each author's copyright. These works may not be reposted without the explicit permission of the copyright holder.