Education

PhD in Computer Science

2015 - 2018 (graduated in May 30, 2019)

University of Verona, Italy

Scholarship holder


MSc in Computer Science and Engineering

2013 - 2015 (graduated in Oct 21, 2015)

University of Verona, Italy

Curriculum: Software Engineering and Security


BSc in Computer Science

2009 - 2013 (graduated in Oct 16, 2013)

University of Verona, Italy

Curriculum: General Computer Science


PhD Thesis

Hyper Static Analysis of Programs  
An Abstract Interpretation-Based Framework for Hyperproperties Verification
Pasqua, M.

  PDF file         $\TeX$ ref

In my PhD I developed a methodology to verify, trough static analysis, hyperproperties of computer programs. In particular, the focus is on information-flow hyperproperties, which are very pervasive in systems security. The approach is based on abstract interpretation, a very powerful formal framework for the approximation of programs semantics. My thesis represents the first systematic approach leveraging abstract interpretation to hyperproperties verification.

  Hyperproperties · Abstract interpretation · Verification

Advisor
Prof. Isabella Mastroeni (University of Verona, Italy)

Referees
Prof. Antoine Miné (Sorbonne Université, France)
Prof. David A. Naumann (Stevens Institute of Technology, United States)