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.
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)