bring this page
with you
Structure Department of Mathematics
Telephone 0498271369
Qualification Professore associato confermato
Scientific sector INF/01 - COMPUTER SCIENCE
University telephone book  Show

Office hours
Dipartimento di Matematica, Torre Archimede (IV piano), via Trieste 63, Padova Ricevimento su appuntamento: Si prega di inviare una richiesta di ricevimento mediante email.
(updated on 09/04/2014 13:05)

Proposals for thesis
Research topics:
-- abstract interpretation
-- static program analysis
-- program verification

Curriculum Vitae
Francesco Ranzato received 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 doctoral positions funded by CNR (Italian National Research Council) and University of Padova. From 1999 to 2002 he was assistant professor in Computer Science at the University of Padova. From 2002 he is an associate professor in Computer Science at the University of Padova. On December 2006 he held a visiting "Directeur de Recherche" position of French CNRS at Ecole Polytechnique, Paris, France. His research interests include abstract interpretation, static program analysis, semantics of programming languages, automatic verification by model checking, behavioural equivalences in process algebras, lattice theory. He has been co-recipient of the 2013 Microsoft Research Software Engineering Innovation Foundation Award, monetary award of 25.000$. He has been or is member of program committees of international conferences and organizer of international workshops on programming languages, static analysis and abstract interpretation. He has been invited speaker at international conferences, workshops and at international research institutes (in Europe and US) and teacher of graduate courses on abstract interpretation. He has been member of international Ph.D. committees across Europe. He is author of about 60 publications on the aforementioned areas in refereed international journals and conferences. As far as project funding and management is concerned, he has been or is principal investigator of a number of research projects concerning abstract interpretation and model checking, that have been funded by MUR (Italian Minister of University and Research) under action FIRB (about 200.000 Euro) and action PRIN (about 70.000 Euro) and by University of Padova (about 40.000 Euro). He has been scientific supervisor of a number of post-doc research grants funded by University of Padova (about 40.000 Euro).

Research areas
Francesco Ranzato’s research work has been mainly concerned with abstract interpretation, static analysis and model checking of software/hardware systems. Abstract interpretation is a general methodology -- invented by French scientists Patrick and Radhia Cousot in late 1970s and recipients of the 2013 ACM SIGPLAN Programming Languages Achievement Award for this achievement -- for designing and formally proving the correctness of approximations of computing systems. This technique provides generic and powerful tools for designing, e.g., static program analyzers, automatic verifiers of sw/hw systems, type systems, security protocol analyzers, etc. Abstract interpretation is a lively research area -- SAS and VMCAI are the flagship annual conferences devoted to research in abstract interpretation, while a significant portion of accepted papers in top-tier programming languages conferences, like ACM PLDI and ACM POPL, concerns abstract interpretation topics -- with 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 a remarkable industrial impact. We can mention a couple of noteworthy examples: (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. Model checking is a well-known formal method for the algorithmic verification of finite/infinite state hw/sw systems. Basically, a formal correctness specification of some system, defined in a temporal logic like LTL or CTL, is verified/refuted by exploring the state space of a formal system model which is described through a transition system. Model checking is a remarkable and well-known success story in automatic system verification. E.M. Clarke, E.A. Emerson and J. Sifakis shared the 2007 ACM Turing Award for their work on model checking.

Francesco Ranzato contributed to defining a standard and widely used framework for the systematic design of domains in abstract interpretation and for their transformations through refinements and simplifications, in particular for achieving optimality properties like completeness. Moreover, he contributed to the integration and combination of typical tools and techniques of abstract interpretation and model checking.


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.

Lecturer's Publications (PDF): 61CC07FD2C9D275DEA197A74DD095A24.pdf

List of taught course units in A.Y. 2017/18
Degree course code (?) Degree course track Course unit code Course unit name Credits Year Period Lang. Teacher in charge
Details for students enrolled in A.Y. 2017/18
Current A.Y. 2017/18
Details for students enrolled in A.Y. 2016/17
Current A.Y. 2017/18
10 2nd Year First
Details for students enrolled in A.Y. 2017/18
Current A.Y. 2017/18
6 1st Year First