Francesco Ranzato's research work is 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.