Refereed Research Papers

P. Ganty, N. Manini, and F. Ranzato. Reachability-guided Abstraction Refinement. In Proceedings of the 27th International Symposium on Formal Methods (FM'26), Tokyo, Japan. Springer LNCS, to appear, 2026.

F. Ranzato, A. Shakeel, and M. Zanella. Exact Robustness Certification of k-Nearest Neighbors. In David Lie and Veronique Cortier editors, Proceedings of the 32nd ACM SIGSAC Conference on Computer and Communications Security (CCS'25), Taipei, Taiwan. Pages 4439-4453, ACM, 2025.
Distinguished CCS paper award
Link to the open source software artifact ERC on Zenodo, with artifact appendix.

P. Baldan, R. Bruni, F. Ranzato, and D. Rigo. Model Checking as Program Verification by Abstract Interpretation. In Patricia Bouyer and Jaco van de Pol editors, Proceedings of the 36th International Conference on Concurrency Theory (CONCUR'25), Aarhus, Sweden. Leibniz International Proceedings in Informatics (LIPIcs) vol. 348, Article No. 8, 2025.

P. Ganty, N. Manini and F. Ranzato. The reachable simulation problem. ACM Transactions on Computational Logic, Volume 26, Issue 3 Article No.: 12, Pages 1-35, 2025.

R. Giacobazzi and F. Ranzato. The Best of Abstract Interpretations. In Proceedings of the 52nd ACM SIGPLAN Symposium on Principles of Programming Languages (POPL'25), Denver, Colorado, Proc. ACM Program. Lang., volume 9, issue POPL, article 46, January 2025. Video of the talk.

P. Ganty, N. Manini and F. Ranzato. Computing Reachable Simulations on Transition Systems. In Proceedings of the 18th International Conference on Reachability Problems (RP'24), Vienna, Austria. Springer LNCS 15050, pages 21-37, 2024.

N. Fassina, F. Ranzato and M. Zanella. Robustness Verification of k-Nearest Neighbors by Abstract Interpretation. Knowledge and Information Systems, vol. 66(8), pages 4825-4859, ICDM 2023 invited paper, Springer, 2024.

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.

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.

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.

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.

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.

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.

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.

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

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.

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.

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.

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.

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.

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.

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

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

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.

P. Cousot, R. Giacobazzi and F. Ranzato. A²I: Abstract² 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

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. 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. Abstracting Nash equilibria of supermodular games. Formal Methods in System Design, 53(2):259-285, 2018.

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. A new characterization of complete Heyting and co-Heyting algebras. Logical Methods in Computer Science, 13(3:25), 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, 2017.

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.

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.

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. 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 and F. Ranzato. Correctness kernels of abstract interpretations. Information and Computation, 237:187-203, 2014.

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

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

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.

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.

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. 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, F. Ranzato and F. Tapparo. Saving space in a time efficient simulation algorithm. Fundamenta Informaticae, 108(1-2):23-42, 2011.

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.

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.

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

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

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.

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

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

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. Generalized strong preservation by abstract interpretation. Journal of Logic and Computation, 17(1):157-197, 2007.

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

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

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.

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

F. Ranzato. Pseudocomplements of closure operators on posets. Discrete Mathematics, 248(1-3):143-155, 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 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.

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. A counterexample to a result concerning closure operators. Portugaliæ Mathematica, 58(1):121-125, 2001.

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

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

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

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

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, 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. Some properties of complete congruence lattices. Algebra Universalis, 40(2):189-200, 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. Optimal domains for disjunctive abstract interpretation. Science of Computer Programming, 32(1-3):177-210, 1998.

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

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, C. Palamidessi, and F. Ranzato. Weak relative pseudo-complements of closure operators. Algebra Universalis, 36(3):405-412, 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.

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.

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

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.

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.

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.

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.