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 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, 2017.

F. Ranzato. A new characterization of complete Heyting and co-Heyting algebras. Logical Methods in Computer Science, 13(3:25), 2017.

F. Ranzato. On constructivity of Galois connections. In I. Dillig and J. Palsberg editors, Proceedings of the 19th International Conference on Verification, Model Checking and Abstract Interpretation (VMCAI'18), Los Angeles, CA, LNCS vol. 10747, pages 452-473, Springer, 2018.

F. Ranzato. Abstracting Nash equilibria of supermodular games. Formal Methods in System Design, 53(2):259-285, 2018.

P. Cousot, R. Giacobazzi and F. Ranzato. Program analysis is harder than verification: A computability perspective. In H. Chockler and G. Weissenbacher editors, Proceedings of the 30th International Conference on Computer Aided Verification (CAV'18), Oxford, UK, LNCS vol. 10981, pages 75-95, Springer, 2018.

F. Ranzato and M. Zanella. Invertible linear transforms of numerical abstract domains.. In A. Podelski editor, Proceedings of the 25th International Static Analysis Symposium (SAS'18), Freiburg im Breisgau, Germany, LNCS vol. 11002, pages 344-363, Springer, 2018.

P. Cousot, R. Giacobazzi and F. Ranzato. A2I: Abstract2 interpretation. In Proceedings of the 46th Annual ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages (POPL'19), Cascais, Portugal, Proc. ACM Program. Lang., Vol. 3, No. POPL, Article 42, 2019. Distinguished POPL paper award.

R. Giacobazzi and F. Ranzato. History of Abstract Interpretation. In Workshop on History of Formal Methods (HFM'19), LNCS vol. 12233. Affiliated with the 3rd World Congress on Formal Methods, Porto, Portugal, October 2019. Slides.

F. Ranzato and M. Zanella. Robustness verification of support vector machines. In Bor-Yuh Evan Chang editor, Proceedings of the 26th International Static Analysis Symposium (SAS'19), Porto, Portugal, LNCS vol. 11822, pages 271-295, Springer, 2019. Link to the open source software artifact SAVer on GitHub.

P. Ganty, F. Ranzato and P. Valero. Language inclusion algorithms as complete abstract interpretations. In Bor-Yuh Evan Chang editor, Proceedings of the 26th International Static Analysis Symposium (SAS'19), Porto, Portugal, LNCS vol. 11822, pages 240-261, Springer, 2019.

F. Ranzato and M. Zanella. Abstract interpretation of decision tree ensemble classifiers. In V. Conitzer and F. Sha editors, Proceedings of the Thirty-Fourth AAAI Conference on Artificial Intelligence (AAAI'20), New York, NY, Vol. 34, No. 04, AAAI-20 Technical Track: Machine Learning, pages 5478-5486, AAAI Press, 2020. Link to the open source software artifact Silva on GitHub.

F. Ranzato. Decidability and synthesis of abstract inductive invariants. In Igor Konnov and Laura Kovacs editors, Proceedings of the 31st International Conference on Concurrency Theory (CONCUR'20), Online Conference (originally planned in Vienna, Austria), Leibniz International Proceedings in Informatics (LIPIcs) volume 171, article No. 30, pp. 30:1-30:21, 2020. Video of the talk.

F. Ranzato and M. Zanella. Genetic Adversarial Training of Decision Trees. In K. Krawiec editor, Proceedings of the 2021 Genetic and Evolutionary Computation Conference (GECCO'21), Online Conference (originally planned in Lille, France). ACM Press, pages 358-367, 2021. Link to the open source software artifact Meta Silvae on GitHub. Video of the talk.

R. Bruni, R. Giacobazzi, R. Gori and F. Ranzato. A Logic for Locally Complete Abstract Interpretations. In L. Libkin editor, Proceedings of the 36th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS'21), Online Conference (originally planned in Rome, Italy), ACM, 2021. Distinguished LICS paper award. Video of the talk.

P. Baldan, F. Ranzato and L. Zhang. A Rice's Theorem for Abstract Semantics. In N. Bansal, E. Merelli, and J. Worrell editors, Proceedings of the 48th International Colloquium on Automata, Languages, and Programming (ICALP'21), Online Conference (originally planned in Glasgow, Scotland), Leibniz International Proceedings in Informatics (LIPIcs) volume 198, Article No. 117, pp. 117:1-117:19, 2021. Video of the talk.

K. Doveri, P. Ganty, F. Parolini and F. Ranzato. Inclusion Testing of Büchi Automata based on Well-quasiorders. In S. Haddad and D. Varacca editors, Proceedings of the 32nd International Conference on Concurrency Theory (CONCUR'21), Online Conference (originally planned in Paris, France), Leibniz International Proceedings in Informatics (LIPIcs) vol. 203, Article No. 3, 2021. Link to the open source software artifact BAIT on GitHub. Video of the talk.

F. Ranzato, C. Urban and M. Zanella. Fairness-Aware Training of Decision Trees by Abstract Interpretation. In Proceedings of the 30th ACM International Conference on Information and Knowledge Management (CIKM'21), Online Conference (originally planned in Gold Coast, Queensland, Australia). Pages 1508-1517, ACM Press, 2021. Link to the open source software artifact FATT on GitHub.

P. Ganty, F. Ranzato and P. Valero. Complete abstractions for checking language inclusion. ACM Transactions on Computational Logic, vol. 22(4), Article No.22, 2021.

R. Giacobazzi and F. Ranzato. History of abstract interpretation. IEEE Annals of the History of Computing, 44(2):33-43, 2022.

R. Bruni, R. Giacobazzi, R. Gori and F. Ranzato. Abstract interpretation repair. In I. Dillig and R. Jhala editors, Proceedings of the 43rd ACM SIGPLAN International Conference on Programming Language Design and Implementation (PLDI'22), San Diego, CA, USA, pp. 426-441, ACM, 2022. Video of the talk.

P. Baldan, F. Ranzato and L. Zhang. Intensional Kleene and Rice Theorems for Abstract Program Semantics. Information and Computation, Vol.289, Part A, Article 104953, 2022.

M. Milanese and F. Ranzato. Local Completeness Logic on Kleene Algebra with Tests. In G. Singh and C. Urban editors, Proceedings of the 29th International Static Analysis Symposium (SAS'22), Auckland, New Zealand. LNCS vol. 13790, pages 350-371, Springer Nature Switzerland AG, 2022.

R. Bruni, R. Giacobazzi, R. Gori and F. Ranzato. A correctness and incorrectness program logic. Journal of the ACM, vol. 70(2), article 15, 45 pages, 2023.

R. Bruni, R. Giacobazzi, R. Gori and F. Ranzato. Local completeness in abstract interpretation. In Challenges of Software Verification, ISRL vol. 238, pp. 145-156, Springer Singapore, March 2023.

N. Fassina, F. Ranzato and M. Zanella. Robustness Certification of k-Nearest Neighbors. In Proceedings of the 23rd IEEE International Conference on Data Mining (ICDM'23), Shanghai, China. IEEE, pages 110-119, 2023. Link to the open source software artifact NAVe on GitHub.

A. Pal, F. Ranzato, C. Urban and M. Zanella. Abstract interpretation-based feature importance for support vector machines. In Proceedings of the 25th International Conference on Verification, Model Checking and Abstract Interpretation (VMCAI'24), London, UK. Springer LNCS 14499, pages 27-49, 2024. Link to the open source software artifact AFI on GitHub.



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.