Address book


Staff Structures


Back to the list


Professore Ordinario





Francesco Ranzato earned the Laurea degree cum laude in Mathematics and the Ph.D. in Computer Science, both at the University of Padova, Italy. On 1995 he visited the Laboratoire d'Informatique of Ecole Polytechnique, Paris, France. From 1997 to 1998 he held post-doc positions funded by CNR and the University of Padova. From 1999 to 2019 he was first assistant and, from 2002, associate professor in Computer Science at the University of Padova. Since 2019 he is a full professor in Computer Science at the University of Padova. On December 2006 he held a visiting "Directeur de Recherche" position of French CNRS. His research interests include abstract interpretation, static program analysis, program verification, verification of machine learning models, behavioral equivalences in process algebras. He has been co-recipient of a 2013 Microsoft Research Software Engineering Innovation Foundation Award, of a 2020 Facebook Research award on Probability and Programming research, and of a 2021 Amazon Research Award. He has been co-recipient of the Distinguished Paper Award at the ACM SIGPLAN POPL 2019 Symposium and at the ACM/IEEE LICS 2021 Symposium. He has been a member of program committees of international conferences (POPL, AAAI, ESOP, CSF, MFCS, SAS, etc) and is an editor of the Formal Methods in System Design journal. He has been invited speaker at international conferences and at international research institutes, and teacher of graduate courses on abstract interpretation. He has been member of international Ph.D. committees across Europe. He is author of about 80 publications in refereed international journals and conferences. As far as project funding and management is concerned, he has been or is principal investigator of several research projects concerning abstract interpretation and program analysis, that have been funded by MUR (Italian Minister of University and Research) under actions FIRB and PRIN, the University of Padova, Microsoft, Facebook and Amazon. He has been scientific supervisor of several post-doc research fellows. He has been elected chair of the Bachelor and Master degrees in Computer Science for the term 2015-2019.


Office hours

  • at Dipartimento di Matematica, Torre Archimede (VI piano), via Trieste 63, Padova
    Meeting by appointment: Please send a request by email.



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.

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.

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.

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.

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.

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.

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.

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.

Research Area

Francesco Ranzato’s research work has been mostly focused on abstract interpretation, static analysis and verification of software systems. Abstract interpretation is a general methodology for designing and formally proving the correctness of approximations of computing systems. This technique provides generic and powerful tools for designing static program analyzers, automatic verifiers of software/hardware systems, type systems, security protocol analyzers, algorithms for formal languages, etc. Abstract interpretation is a lively research area: SAS and VMCAI are the flagship annual conferences devoted to research in abstract interpretation and static analysis, while a significant portion of accepted papers in top-tier programming languages conferences, like ACM PLDI and ACM POPL, concerns topics in abstract interpretation (the top 5 most cited articles at ACM POPL include three articles on abstract interpretation, in particular the most cited article, which according to Google scholar has more than 7000 citations). Abstract interpretation has a wide active community of European (in particular Italian, as witnessed by many Italian PRIN-funded research projects on abstract interpretation), American and Asian researchers. Abstract interpretation had, and still has, a great industrial impact. Noteworthy examples include: (1) the Polyspace static analyzer for C/C++ and Ada programs has been fully conceived and designed by abstract interpretation and is successfully commercialized by TheMathWorks; (2) Microsoft Visual Studio IDE incorporates an abstract interpretation-based static analyzer of .NET bytecode that allows to automatically derive correctness specifications, the so-called Code Contracts; (3) Astre ́e is a C static analyzer based on abstract interpretation, conceived and designed by Patrick and Radhia Cousot’s research group at ENS Paris, marketed by AbsInt GmbH (Germany), and used in the defense/aerospace (Airbus, Honda), electronic (Siemens), and automotive industries (Daimler); (4) Infer is a static analysis tool for detecting memory and concurrency bugs in Java/C/C++/Objective-C code, developed by Facebook, based on abstract interpretation and routinely used by Facebook software engineers. For the invention of abstract interpretation together with his late wife Radhia Cousot (1947-2014), Patrick Cousot has been the recipient of: the 2018 IEEE John von Neumann Medal; the 2014 IEEE Computer Society Harlan D. Mills Award; the 2013 ACM SIGPLAN Programming Languages Achievement Award; a honorary doctorate from the Universitat des Saarlandes (Germany); the 1999 French CNRS Silver Medal.

Thesis proposals

Research topics:
-- abstract interpretation
-- static program analysis
-- software verification
-- program semantics
-- verification of machine learning models
-- algorithms for automata and formal languages