Alessandro Armando is professor at the University of Genoa, where he received his Laurea degree in Electronic Engineering in 1988 and his Ph.D in Electronic and Computer Engineering in 1994. His appointments include a postdoctoral research position at the University of Edinburgh (1994-1995) and one as visiting researcher at INRIA-Lorraine in Nancy (1998-1999).

He has been co-founder and director of the Artificial Intelligence Laboratory (AI-Lab) at DIST (2003-2011), of the Security and Trust Research Unit at the Center for Information Technologies of Bruno Kessler Foundation in Trento (2010-2016), and of the Computer Security Laboratory (CSec) at DIBRIS. He is co-founder of the Talos, a spin-off of DIBRIS focused on Cybersecurity.

He has been founder and director (Presidente del Comitato di Gestione) of the Master Universitario di II Livello on ``Cyber Security and Data Protection’’ of the University of Genova for the academic years 2014/2015 and 2016/2017.

He has contributed to the discovery of a vulnerability on the SAML-based Single Sign-On for Google Apps, an authentication flaw in emerging SSO protocols (namely SAML SSO v2.0 and OpenID), and a vulnerability that leads to a Denial of Service attack on all Android devices.

His focus is on developing cutting-edge automated reasoning techniques and on using them to build a new generation of push-button software verification and debugging tools supporting the development of complex, large-scale, distributed IT applications.

• Google Scholar

• Scopus

• DBLP

• “Securing Distributed Applications: Introduction to Cryptographic Protocols”, 29th Summer PhD School of Information Engineering SSIE 2019, Bressanone (Italy), July 8-12, 2019.

• “Formal Methods for Security: Challenges and Opportunities”, IACR Cryptology School on Security Correctness in the Internet of Things 2017, Graz (Austria), May 8-12, 2017.

• “Countering the Cyber Threat: Automated Vulnerability Assessment”, seminario internazionale “Il pericolo corre in rete la nuova frontiera della minaccia cibernetica” organizzato dalla Delegazione italiana presso l’Assemblea parlamentare della NATO in collaborazione con il Centro Studi Americani, Roma, Camera dei Deputati, 15 giugno 2017.

• “Automated Security Analysis of Applications”, Workshop “Cyber Risk e Mercato Assicurativo”, Genova, May 5, 2017.

• “Innovation in Cyber Security Research - Directions and Opportunities”, Workshop 4: “Technical Perspectives” at the NIAS2015 Cyber Security Symposium, Mons (Belgium), September 16, 2015.

• “Automated Analysis of Security Protocols and Multi-party Web Applications” at the Interdisciplinary Centre for Security, Reliability and Trust, University of Luxembourg, September 18, 2015.

• “Enforcing BYOD policies on Android Devices”, keynote speech at the Seminar on Road-mapping Cybersecurity Research and Innovation co-organized by the EU NIS platform WG3 and the European projects SECCORD and CAPITAL, Firenze, Oct 8, 2014.

• Invited talk on “Android Security Secure Meta-Markets”, NeSSoS Meeting, September 5, 2013, Bertinoro, Italy.

• “The SPaCIoS Tool: property-driven and vulnerability-driven security testing for Web-based apps”, lecture at the 13th International School on Foundations of Security Analysis and Design (FOSAD’13), September 4, 2013, Bertinoro, Italy.

• “Security and Privacy of Web-based Single Sign-On Protocols: Pitfalls and Solutions”, keynote speech at the IFIP Summer School on Privacy and Identity Management for Life, September 7, 2011, Trento, Italy.

• “The Rewriting Approach to Decision Procedures”, lecture at the Summer School on Verification Technology, Systems Applications (VTSA’11), September 23, 2011, Montefiore Institute (University of Liege), Belgium.

• “Automatic Symbolic Analysis of Access Control Policies”, lecture at the Summer School on Verification Technology, Systems Applications (VTSA’11), September 23, 2011, Montefiore Institute (University of Liege), Belgium.

• “Building SMT-based Software Model Checkers: an Experience Report”, 7th International Symposium on Frontiers of Combining Systems, Trento, Italy, September 16-18, 2009.

• “Formal Analysis of SAML 2.0 Web Browser Single Sign-On: Breaking the SAML-based Single Sign-On for Google Apps”, Istituto per la Ricerca Scientifica e Tecnologica, Trento, Italy, March 2, 2009.

• “LTL Model Checking for Security Protocol Analysis”, Workshop on Logic and Information Security, September 22-28, 2008, Lorentz Center, Leiden, Holland.

• “Verifica Automatica della Sicurezza delle Applicazioni Web: come abbiamo scoperto la vulnerabilita al servizio di Single Sign-On di Google”, Security Seminar after the Silicon Valley Study Tour 2008, Genova, Italy, November 4, 2008.

• “LTL Model Checking for Security Protocol Analysis”, Workshop on Workshop Logic and Information Security, Leiden University, Holland, September 22-28, 2008.

• “Software Model Checking: new challenges and opportunities for Automated Reasoning”, invited talk at Workshop on Practical Aspects of Automated Reasoning (PAAR-2008) and at the Workshop on Complexity, Expressibility, and Decidability in Automated Reasoning (CEDAR’08), Sydney, Australia, August 10, 2008.

• “Automatic Validation of Internet Security Protocols”, lecture at the AEOLUS Summer School on Global Computing, Salerno, September 20, 2007.

• “Big proof engines as little proof engines: new results on rewrite-based satisfiability procedures”, CISA Talk, Division of Informatics, University of Edinburgh, August 23, 2007.

• “Decision Procedures for Automated Verification”, lecture at the Scuola Estiva di Logica, Palazzo Feltrinelli, Gargnano, September 5, 2006.

• “Bounded Model Checking of C Programs using a SMT solver instead of a SAT solver”, Forum on Decision Procedures, Microsoft Research, Cambridge (UK), September 13, 2005.

• “The AVISPA Project: Automatic Validation of Internet Security Protocols”, Security Area Advisory Group (SAAG) Meeting, in the context of the 62nd IETF Meeting, Minneapolis, March 5, 2005.

• “Automatic SAT-Compilation of Protocol Insecurity Problems via Reduction to Planning”, Computer Science Department, University of Texas, November 11, 2002.

• “Integration of Decision Procedures in Automated Reasoning” lecture series at the CALCULEMUS Autumn School, Pisa, September 30 - Oct 1, 2002.

• “An Overview of the AVISS Project”, Workshop on Specification, Analysis and Validation for Emerging Technologies (SAVE 2002), Copenhagen, Denmark, July 27, 2002.

• “Proof-planning: an Overview”, DEIS - University of Bologna, July 2, 2002.

• “A Rule-Based Approach to Specifying the Integration of Decision Procedures in Formula Simplification”, INRIA-Lorraine, Nancy, June 29, 2001.

• “An Overview of the Open Mechanized Reasoning Systems Project”, Prosper Research Workshop, University of Cambridge, November 22, 1999.

• “Integrating decision procedures with rewriting”, NASA Ames Research Center (California), November 7, 1997.

• “Constraint Contextual Rewriting”, Institute for Algorithms and Cognitive Systems, University of Karlsruhe (Germany), 1997.

I served in the Steering Committees of the following scientific events:

• International Workshop on Security Testing, 2011-present.

• Workshop on Semantic Computing for Security and Privacy, sponsored by the IEEE Computer Society’s Technical Committees Security and Privacy (TCSP) and Semantic Computing (TCSEM), 2011-2013.

• International Conference on Automated Deduction (ex officio, 2008-2009), http://www.cadeconference.org/.

• International Joint Conference on Automated Reasoning, (2002-2007 and ex-officio 2008-2009), http://www.ijcar.org/.

• The First Order Theorem Proving (FTP) Workshop Series. (Elected for the period 2001-2006), http://www.csc.liv.ac.uk/FTP-WS/

• Frontiers of Combining Systems (FroCoS) Workshop Series (ex-officio 2001-2005), http://combination.cs.uiowa.edu/frocos/.

• CALCULEMUS Interest Group. (Ex-officio from 1999 to 2001; elected for the period 2001-2004), http://www.calculemus.net.

I also served in the Management Committee of

• COST Action IC0901: Rich-Model Toolkit - An Infrastructure for Reliable Computer Systems (2009-2013).

I have been Program Chair of the following scientific events:

• (with Hilarie Orman) 2nd Workshop on Semantic Computing for Security and Privacy (WSCS’12), May 24, 2012.

• (with Maria Paola Bonacina) Rich-Model Toolkit Meeting, Torino, Italy October 3-4, 2011.

• (with G. Lowe) Joint Workshop on Automated Reasoning for Security Protocol Analysis and Issues in the Theory of Security (ARSPA-WITS 2010), Cyprus, March 2010.

• (with P. Baumgartner and G. Dowek) 4th International Joint Conference on Automated Reasoning (IJCAR 2008), Sidney, August 11-16, 2008.

• (with A. Cimatti) 3rd Workshop on Pragmatics of Decision Procedures in Automated Reasoning (PDPAR’05), Edinburgh (UK), July 12, 2005.

• (with Luca Vigano) Automated Reasoning for Security Protocols Analysis (ARSPA’04), Cork, Ireland, July 4, 2004.

• 4th International Workshop on Frontiers of Combining Systems (FroCoS 2002), Santa Margherita Ligure, April 8-10, 2002.

• (with Tudor Jabelean) 7th Symposium CALCULEMUS: Systems for Integrated Computation and Deduction held in Trento on July 11-12, 1999 in the context of the 1999 Federated Logic Conference (FLoC’99).

I served in the Program Committee of the following scientific events:

• 31st IEEE Computer Security Foundations Symposium (CSF 2018), 2018.

• 23rd ACM Symposium on Access Control Models and Technologies (SACMAT’18), 2018.

• Italian Conference on Cybersecurity (ITASEC), 2017 and 2018 (2 editions).

• 30th AAAI Conference on Artificial Intelligence (AAAI-16), 2016.

• 4th International Seminar on Program Verification, Automated Debugging and Symbolic Computation (PAS 2015), Beijing, China, October 21-23, 2015.

• Conference on Principles of Security and Trust (POST), 2015 and 2016 (2 editions).

• 10th International Symposium on Trustworthy Global Computing (TGC), 2015.

• International Conference on Security and Cryptography (SECRYPT), 2013, 2014, and 2015 (3 editions).

• 8th International Conference on Availability, Reliability and Security (AReS 2013).

• 1st Workshop on Automated Reasoning in Security (ARSEC 2013), 2013.

• 3rd IFIP WG 11.6 Working Conference on Policies Research in Identity Management (IFIP IDMAN 2013).

• European Symposium on Research in Computer Security (ESORICS), 2012, 2013, and 2015 (3 editions).

• International Workshop on Security and Trust Management (STM), 2011 and 2012 (2 editions).

• Theory of Security and Applications, 2011.

• Joint Workshop on Automated Reasoning for Security Protocol Analysis and Issues in the Theory of Security (FCS-ARSPA-WITS), 2010.

• Future Internet Symposium (FIS), 2008 and 2009 (2 editions).

• IEEE/ACM International Conference on Automated Software Engineering (ASE), 2008, 2009, 2010 (3 editions).

• International Workshop on Computational Intelligence in Security for Information Systems (CISIS), 2008 and 2009 (2 editions).

• International Conference on Artificial Intelligence and Symbolic Computation (AISC), 2008 and 2010 (2 editions).

• Joint Workshop on Foundations of Computer Security, Automated Reasoning for Security Protocol Analysis and Issues in the Theory of Security (FCS-ARSPA-WITS), 2008.

• International Symposium on Formal Methods (FM), 2008.

• International Symposium on Frontiers of Combining Systems (FroCoS), 2002, 2005, and 2007 (3 editions).

• International Symposium on the Integration of Symbolic Computation and Mechanized Reasoning (CALCULEMUS), 2000, 2001, 2002, 2005, 2007 (5 editions).

• Workshop on the Foundations of Computer Security and Automated Reasoning for Security Protocol Analysis (FCS-ARSPA), 2006, 2007 (2 editions).

• International Conference on Rewriting Techniques and Applications (RTA), 2007.

• Workshop on Information and Computer Security (ICS), 2006.

• International Workshop on Pragmatics of Decision Procedures in Automated Reasoning (PDPAR), 2003, 2004, 2005 and 2006 (4 editions).

• International Conference on Mathematical Knowledge Management (MKM), UK.

• International Joint Conference on Automated Reasoning (IJCAR), 2004, 2006, 2008, 2010 (4 editions).

• International Workshop on First-Order Theorem Proving (FTP), 2005.

• IJCAI Workshop on Agents and Automated Reasoning, 2003.

• International Conference on Automated Deduction (CADE), 2003, 2011, 2013, and 2015 (4 editions).

• Workshop on Specification, Analysis and Validation for Emerging Technologies (SAVE), 2002.

• International Workshop on Strategies in Automated Deduction (STRATEGIES), 2001.

• Workshop Future Directions in Automated Reasoning (FUTURE), 2001.

• Conference Automated Deduction: Putting Theory into Practice, 2000.

I am (or have been) scientific coordinator of the following research projects:

• Advanced Research Workshop - ``New Generation CERT: from Response to Readiness - Strategy and Guidelines’’, to be held at the School of Telecommunications of the Italian Armed Forces of Chiavari (Italy), March 28-30, 2017. Co-Directors: Alessandro Armando and Marc Henauer (Reporting and Analysis Centre for Information, Bern, Switzerland). Funded by NATO in the context of the NATO Science for Peace and Security (SPS) Programme.

• A European Industrial Doctorate on Security and Trust of Next Generation Enterprise Information Systems (SECENTIS) funded by the European Commission in the context of the 2012 PEOPLE Work Programme. Partner Institutions: FBK and SAP AG (main beneficiaries), University of Trento and TrentoRISE (associated partners). Duration: 48 months, starting on April 1, 2013.

• Security Threat Identification and Testing (STIATE) funded by the European Institute of Innovation and Technology (EIT ICT Labs) in the context of Action Line on Privacy, Security and Trust 2014. Partner institutions: FBK (coordinator), SAP, Reply, and DFKI. Duration: 12 months, starting on January 1, 2014.

• Formal specification of security model for the High Assurance Automated Guard, funded by the NATO Communications and Information Agency. Duration: 6 months, starting on July 15, 2012 and then renewed in 2013 (6 months) and 2014 (8 months).

• BYODroid Demonstrator, funded by NATO Communications and Information (NCI) Agency. Duration: 3 months, starting on March 1, 2015.

• Mobile Application Verification Cluster (MAVERIC), funded by Poste Italiane. Duration: 24 months, starting on January 1, 2014.

• Integrating automated reasoning in model checking: towards push-button formal verification of large-scale and infinite-state systems (20079E5KM8) funded by the Italian Ministry of Scientific and Technological Research in the context of the PRIN 2007 Programme. Partner Institutions: DIST, U. di Genova (Prof. A. Armando, coordinator); U. di Napoli (Prof. M. Benerecetti); U. di Trento (Prof. R. Sebastiani); U. di Verona (Prof. M. P. Bonacina). Duration: 24 months, starting on September 23, 2008.

• IST FET Open Project AVISPA: Automated Validation of Internet Security Protocols and Applications (IST-2001-39252) funded by the European Commission in the context of the 5th Framework Programme. Partner Institutions: DIST, U. di Genova (Prof. A. Armando, coordinator); Eidgenoessische Technische Hochschule Zurich (ETHZ), Switzerland (Prof. D. Basin); INRIA Lorraine, France (Dr. M. Rusinowitch); Siemens AG, Munich, Germany (Dr. J. Cuellar). Duration: 30 months, starting on January 1, 2003.
  In 2006 the AVISPA Project received the nomination for the Descartes Prize for excellence in scientific collaborative research. (It was one the 13 projects shortlisted out of 65 submissions.) From the Descartes Prizes web page (http://cordis.europa.eu/science-society/descartes/home.html): ``This prize is awarded to teams of researchers who have achieved outstanding scientific or technological results through collaborative research in any field of science, including the social sciences, humanities and economics.’’

• International project for the co-tutoring of PhD students and mutual recognition of the degree in the area of integration of Deduction and Symbolic Computation. The project has been funded by the Italian Ministry of Scientific and Technological Research in the context of the Program of Internationalisation of the Italian University System (D.M. 21.6.99, art.7 - Internazionalizzazione, URL: interlink.murst.it). Duration: 4 years starting from November 1, 2000.

• Verifica automatica dei protocolli di sicurezza (RBAU01P5SS) funded by the Italian Ministry of Scientific and Technological Research in the context of the FIRB 2001 Programme. Partner Institutions: DIST, U. di Genova (Prof. A. Armando, coordinator); University of Trento (Prof. F. Massacci); University of Napoli (Prof.M. Benerecetti). Duration: 36 months starting from July 1, 2003.

Principal investigator of the following research projects:

• [Special projects for advanced research and technology in Europe (SPARTA)(https://www.sparta.eu/), project number 786727 (call H2020-SU-ICT-2018-2), funded by the EU in the context of H2020 Programme. Grant agreement No 830892. Partner institutions: CEA (coordinator), CINI-Cybersecurity National Lab together with 42 other institutions. Duration: 36 months from Feb 1, 2019.

• Integrated Framework for Predictive and Collaborative Security of Financial Infrastructures (FINSEC), Innovation Action, project number 786727 (call CIP-2016-2017-2), funded by the EU in the context of H2020 Programme. Partner institutions: GFT (coordinator), CINI-Cybersecurity National Lab together with 20 other entities. Duration: 36 months from May 1, 2018.

• FilieraSicura (Securing the Supply Chain of Domestic Critical Infrastructures from Cyber Attacks) funded by CISCO. Partner institutions: U. of Rome “La Sapienza” (coordinator), U. of Genova, U. of Napoli ``Federico II’’, U of Trento, U. of Venice “Ca’ Foscari”, Politecnico di Milano, Politecnico di Torino, IMT School for Advanced Studies Lucca. Duration: 36 months, starting on January, 2017.

• FIDES (Federated Identity Management in Europe) funded by the European Institute of Innovation and Technology (EIT ICT Labs) in the context of Action Line on Privacy, Security and Trust 2015. Partner institutions: Poste Italiane (coordinator), FBK, Reply, DFKI, and Politecnico di Torino, Eotvos Lorand University, Telecom Italia, TNO. Duration: 12 months, starting on January 1, 2015.

• Security Horizons (2010XSEMLC006), funded by the Italian Ministry of Scientific and Technological Research in the context of the PRIN 2011 Programme.

• Secure Provision and Consumption in the Internet of Services (SPaCIoS), STREP project number 257876, funded by the EU in the context of the 7th Framework Programme, THEME ICT-1-1.4 – Secure, dependable and trusted Infrastructures. Partner Institutions: U. of Verona (coordinator), U. of Genova, ETHZ, SAP Research, Siemens AG, Karlsruhe Institute of Technology, Institut Polytechnique de Grenoble. Duration: 36 months from October 11, 2010.

• Automated Validation of Trust and Security of Service-oriented Architectures (AVANTSSAR), STREP project number 216471, funded by the EU in the context of the 7th Framework Programme, THEME ICT-1-1.4 – Secure, dependable and trusted Infrastructures. Partner Institutions: U. of Verona (coordinator), U. of Genova, ETHZ, SAP Research, Siemens AG, INRIA-Lorraine, IRIT, OpenTrust, Institute e-Austria Timisoara. Duration: 36 months from January 1, 2008.

• Sistema INTEgrato per la Sicurezza ad Intelligenza diStribuita (SINTESIS), Distretto Tecnologico Ligure. Duration: 18 months from March 1, 2009.

• Decision Procedures for Software Model Checking (2003097383-002) funded by the Italian Ministry of Scientific and Technological Research in the context of the PRIN 2003 Programme. Duration: 24 months from November 20, 2003.

• AVISS: Automated Verification of Infinite State Systems (IST-2000-26410) funded by the European Commission in the context of the Future and Emerging Technologies Programme of the 5th Framework Programme. Duration: 12 months from May 1, 2001.

• Integration of Decision Procedures in Automated Deduction in collaboration with Dr.Michael Rusinowitch (INRIA Lorraine). Funded by the French Ministry of Foreign Affairs and CRUI (Conferenza dei Rettori delle Universita Italiane) through the Italian Ministry of Scientific and Technological Research (MURST) in the context of the Programme Galileo 1999. Research Training Network CALCULEMUS: Systems for Integrated Computation and Deduction (HPRN-CT-2000-00102),

• Funded by the European Commission in the context of the Programme Improving Human Research Potential and the Socio-Economic Knowledge Base of the 5th Framework Program. Duration: 48 months from January 1, 2000.

• The Use of Metatheoretic and Analogical Reasoning in Proof Planning in collaboration with Prof.Jorg Siekmann of the Department of Computer Science of the University of Saarbrucken (Germania). Funded by CRUI (Conferenza dei Rettori delle Universita Italiane) and DAAD in the context of the Programme Vigoni 1996.

• Automation of Program Synthesis in Proof-Planning in collaboration with Prof.Alan Bundy of the Department of Artificial Intelligence of the University of Edinburgh. Funded by CRUI (Conferenza dei Rettori delle Universita Italiane) and the British Council in the context of the British-Italian Cooperation Programme for Research and High Education (1996 Edition).

• Reflective Architectures for Automated Deduction in collaboration with Prof.Alan Bundy (University of Edinburgh), Prof.David Basin (Max-Planck Institut fur Informatik – Saarbrucken), Prof. Fausto Giunchiglia (University of Trento). Funded by CNR (Consiglio Nazionale delle Ricerche).

• L. Compagna, A. Sudhodanan, R. Carbone, A. Armando. Dynamic Analysis Security Testing of Multi-Party Web Applications Via Attack Patterns. Publication number: US 20170109534 A1, April 20, 2017.

I have contributed to the design and/or development of the following software tools:

• RDL (Rewrite and Decision Procedures Laboratory). RDL is a fully automatic tool for formula simplification in quantifier-free first-order theories (Linear Arithmetics, Theory of Equality,and their combination). RDL is based on the Constraint Contextual Rewriting paradigm and features a tight integration of rewriting and decision procedures.

• TSAT++ is an open platform for satisfiability modulo theories (SMT) based on a tight coupling of satisfiability procedures and a SAT-solver. The current version of TSAT++ supports Separation Logic (also known as Difference Logic).

• The AVISS Tool is a fully automatic security protocol analyser. It is capable to analyse a large portion of the protocols collected in the Clark \& Jacob library of security protocols. It is the predecessor of the AVISPA Tool.

• The AVISPA Tool is a fully automatic analyser for large-scale Internet security-sensitive protocols. It comprises 4 back-ends implementing a variety of security protocol verification techniques.

• SATMC (SAT-based Model Checker) is a bounded model checker for security protocols. SATMC reduces the problem of checking whether a protocol is vulnerable to attacks of bounded length to the satisfiability of a propositional formula which is then solved by a state-of-the-art SAT solver taken off-the-shelf. SATMC is one of the back-ends of the AVISPA Tool.

• The AVANTSSAR Platform is an integrated toolset supporting the formal specification and automated validation of the trust and security of service-oriented architectures.

• The SPaCiOS Tool is an automated tool that supports security analysts in the security analysis of on-line applications. This is achieved by leveraging several techniques, including formal modeling, abstract attacks detection, and security testing.

• Eureka is a model checker for sequential software (C code) based on the counterexample-guided abstraction refinement (CEGAR) paradigm. Unlike many other software model checkers based on the CEGAR paradigm Eureka analyses arrays precisely.

• SMT-CBMC is a bounded model checker for sequential software (C code). SMT-CBMC reduces the problem of checking whether an input program has an execution path of bounded length violating an assertion to the satisfiability of a formula with respect to a decidable theory which is then solved by a state-of-the-art SMT solver taken off-the-shelf.

• BYODroid implements the Bring Your Own Device (BYOD) paradigm on Android devices. This is done by automatically checking mobile applications against the security policy set by the organization. The innovation potential of BYODroid is witnessed by the following recognitions:

  • BYODroid has been selected (1st place in the ranking) in the Start Cup of the University of Genova, 2013 edition.

  • BYODroid entered the final of the Idea Challenge 2014 of the EIC ICT Labs of the European Institute of Innovation and Technology.

  • BYODroid has been selected by the NATO Communications and Information Agency (NCIA) in the context of the Cyber Security Incubator 2015 Program.

• MAVERIC is a platform for the automatic security analysis and monitoring of mobile applications whose development has been funded by Poste Italiane. MAVERIC is now routinely used by the Computer Emergency Response Team (CERT) of Poste Italiane to monitor and analyze the Poste Italiane mobile apps ecosystem.

• President of the Management Committee (Presidente del Comitato di Gestione) of the Master Universitario di II Livello on ``Cyber Security and Data Protection’’, academic years 2014/2015 and 2016/2017, University of Genova.

• 2014–present (3 academic years) Computer Security, MSc in Computer Engineering, University of Genova.

• 2010–2013 (3 academic years) Sistemi Operativi e Sicurezza Informatica, (Operating Systems and Computer Security), MSc in Computer Engineering, University of Genova.

• 2007–2009 (2 academic years) Tecnologie Software per il Web 1 (Software Technologies for the Web 1), MSc in Computer Engineering, University of Genova.

• 2005–2009 (4 academic years) Sicurezza Informatica 1 (Computer Security 1), MSc in Computer Engineering, University of Genova.

• 2005–2007 (2 academic years) Fondamenti di Informatica (Fundamentals of Computer Science), MSc in Mechanical Engineering, University of Genova.

• 2003–2005 (2 academic years) Internet e E-Government (Internet and E-Government), MSc in Science of Communication, University of Genova.

• 1999–2009 (10 academic years) Intelligenza Artificiale 1 (Artificial Intelligence 1), MSc in Computer Engineering, University of Genova.

• 2001–2002 (1 academic year) Fondamenti di Informatica (Fundamentals of Computer Science), MSc in Telecommunication Engineering, University of Genova.

• 1999–2001 (2 academic years) Fondamenti di Informatica – II Modulo (Fundamentals of Computer Science – Module 2), MSc in Computer Engineering and MSc in Telecommunication Engineering, University of Genova.

• 1995–1999 (4 academic years) Fondamenti di Informatica (Fundamentals of Computer Science), MSc in Computer Engineering and MSc in Telecommunication Engineering, University of Genova.

• 1995–98 (3 academic years) Fondamenti di Informatica (Fundamentals of Computer Science), course of ``Diploma Universitario’’ in Logistics and Production Engineering, University of Genova.

Supervision

I have supervised more than 30 students during the preparation of their M.Sc. Thesis. I have also been PhD advisor of the following people:

• Metoui Nadia, ``Privacy-Aware Risk-Based Access Control Systems’’, University of Trento, 2018.

• Avinash Sudhodanan, “Automatic Security Testing of Browser-Based Security Protocols”, U. of Trento \& FBK in the context of the SECENTIS project, 2017. Joint supervision with Luca Compagna and Roberto Carbone. Current Position: Researcher at IMDEA.

• Tuan Anh Truong, “Efficient Automated Security Analysis of Complex Authorization Policies”, University of Trento and FBK, 2015. Joint supervision with Silvio Ranise. Current Position: Lecturer at the University of Technology, Vietnam.

• Luca Verderame, “Security Analysis of the Android Operating System”, University of Genova, 2012. Joint supervision with Alessio Merlo and Gabriele Costa. Current Position: CEO at Talos, Genova.

• Serena Elisa Ponta, “Formal Specification and Automatic Analysis of Security-sensitive Business Processes”, University of Genova, 2011. Current position: Researcher at SAP Research, Sophia Antipolis.

• Roberto Carbone, “LTL Model-Checking for Security Protocols”, University of Genova 2009. The PhD thesis has been awarded the the CLUSIT Prize in 2009. Current position: researcher at FBK, Trento.

• Lorenzo Platania, “Software Verification using Satisfiability Modulo Theories”, University of Genova, 2009.

• Jacopo Mantovani, “Automatic Software Verification for Robotics”, University of Genova, 2007.

• Pierre Ganty, “The Fixpoint Checking Problem: An Abstraction Refinement Perspective”, 2007. Joint supervision with Prof. Prof. Jean-Francois Raskin (Computer Science Department, Universite Libre de Bruxelles) and Prof. Giorgio Delzanno (DISI, University of Genova) in the context of a bilateral agreement between the University of Genova and the Universite Libre de Bruxelles. Current position: Assistant Research Professor at IMDEA Software Institute, Madrid.

• Luca Compagna, “SAT-based Model Checking of Security Protocols”, 2004. Joint supervision with Dr.Alan Smaill (Division of Informatics of the University of Edinburgh) in the context of a bilateral agreement between the University of Genova and the University of Edinburgh. Current position: Senior Researcher at SAP Research, Sophia Antipolis.

• Silvio Ranise, “Integration of Decision Procedures in Automated Theorem Provers”, 2001. Joint supervision with Dr.Michael Rusinowitch of INRIA Lorraine (Nancy, France) in the context of a bilateral agreement between the University of Genova and the University of Henri Poincare–Nancy 1. Current position: Senior Researcher at FBK, Trento.