Supervision Activity

I have supervised the following people during their PhD:

Silvio Ranise. (XIV Ciclo) Integration of Decision Procedures in Automated Theorem Provers. Joint supervision with Dr. Michael Rusinowitch (LORIA, Nancy), 2002.
Luca Compagna. (XVI Ciclo) SAT-based Model Checking of Security Protocols. Joint supervision with Dr. Alan Smaill. (Division of Informatics, U. of Edinburgh), 2005.
Jacopo Mantovani. (XIX Ciclo) Automatic Software Verification for Robotics, 2007.
Pierre Ganty. (XVIII Ciclo) The Fixpoint Checking Problem: An Abstraction Refinement Perspective. Joint supervision with Prof. Giorgio Delzanno (DISI, U. of Genova) and Prof. Jean-Francois Raskin (Computer Science Department, Université Libre de Bruxelles), 2007.
Roberto Carbone. (XXI Ciclo) LTL Model-Checking for Security Protocols , 2009.
Lorenzo Platania. (XXI Ciclo) Software Verification using Satisfiability Modulo Theories, 2009

I am currently supervising the following PhD Students:

Serena Elisa Ponta. (XXIII Ciclo)

I have supervised the following people in their Laurea Thesis (in reverse chronological order):

Roberto Basile. Specification and security analysis of the Google Single Sign-On service Laurea Thesis in Computer Engineering - University of Genova,October 2008.

Serena Elisa Ponta. Modeling, Formalisation and Automatic Analysis of Security-sensitive Banking Workflows: the Loan Origination Process as a Case Study. Laurea Thesis in Computer Engineering - University of Genova, October 2007.

Lorenzo Platania. Combinazione di procedure di decisione nella verifica formale di software. Laurea Thesis in Computer Engineering - University of Genova, November 2005. Current position: PhD Student at DIST, University of Genova.

Roberto Carbone. Estensione del Problema di Pianificazione alla Logica Temporale: Applicazione all'Analisi Formale di Protocolli di Sicurezza. Laurea Thesis in Computer Engineering - University of Genova, November 2005. Current position: PhD Student at DIST, University of Genova.

Massimo Idini. Sviluppo ed analisi sperimentale di una procedura SAT-Based per la Separation Logic. Laurea Thesis in Computer Engineering - University of Genova, March 2004.

Cristina Frà. Estensione del Problema di Pianificazione Attraverso l'Utilizzo di Assiomi: Applicazione all'Analisi Formale di Protocolli di Sicurezza. Laurea Thesis in Computer Engineering - University of Genova, March 2004.

Corrado Giromini. La Logic Broker Architecture: Interconnessione di sistemi distribuiti per il ragionamento automatico. Laurea Thesis in Computer Engineering - University of Genova, December 2001.

Pasquale De Lucia. Model Checking di Programmi Imperativi nel Dominio dei Numeri Reali. Laurea Thesis in Computer Engineering - University of Genova, November 2001.

Felice Peccia. Valutazione Sperimentale di Procedure di Decisione per l'Aritmetica Lineare. Laurea Thesis in Computer Engineering - University of Genova, July 2001.

Luca Compagna. Progetto e sviluppo di un'architettura aperta per l'integrazione di procedure di decisione nella riscrittura. Laurea Thesis in Computer Engineering - University of Genova, October 2000. Current position: Senior Researcher at SAP Research, Sophia Antipolis, France.

Daniele Zini. Towards Interoperability of Verification Tools: the Logic Broker Architecture. Laurea Thesis in Computer Engineering - University of Genova, April 2000. Current position: Support Engineer at Microsoft Enterprise Services.

Claudio Castellini. Sviluppo ed analisi sperimentale di procedure di decisione per l'Aritmetica Lineare. Laurea Thesis in Computer Engineering - University of Genova, June 1998. Current position: Researcher at LIRA-Lab, DIST, University of Genova.

Silvio Ranise. Sistemi Aperti per il Ragionamento Meccanizzato: la procedura per l'aritmetica lineare di Boyer e Moore come Componente di Ragionamento. Laurea Thesis in Computer Engineering - University of Genova, December 1997. Current position: Researcher at INRIA-Lorraine, Nancy, France.

Alessandro Coglio. Definizione di un formalismo per la specifica delle strategie di inferenza dei sistemi di ragionamento meccanizzato e sua applicazione ad un sistema allo stato dell'arte. Laurea Thesis in Computer Engineering - University of Genova, April 1996. Current position: Computer Scientist at Kestrel Institute Palo Alto California (USA).

Corrado Cimatti. Una famiglia di procedure di decisione per la logica del prim'ordine. Laurea Thesis - University of Genova, October 1994.

Luca Viganò. Sintesi ed esecuzione di strategie di prova nella metateoria formale di un dimostratore interattivo. Laurea Thesis in Computer Engineering - University of Genova, January 1994. Current position: Associate Professor at the University of Verona.

Andrea Parodi. and Fulvio Rappa. Progetto e Sviluppo di un Ambiente per l'Integrazione di Algoritmi Decisionali in un Dimostratore Automatico Interattivo. Laurea Thesis in Computer Engineering - University of Genova, April 1993.