Photo

Postdoc at Carnegie Mellon University in Corina Pasareanu's group at the Silicon Valley campus.

Research

My main research interest is software analysis. In particular, I am interested in analysing consumption of resources such as time, memory and energy. Within the ISSTAC project, we use the Symbolic PathFinder extension SPF-WCA to infer bounds on worst-case time and space complexity of Java programs. The goal is to identify security vulnerabilities (both denial-of-service and side-channel based attacks). These inferred bounds can then be verified with our tool JayHorn, a light-weight prover for Java.

Before joining CMU-SV, I was with the Open University of the Netherlands and Radboud University Nijmegen. My PhD at Radboud University was advised by Marko van Eekelen and concerned software analysis methods for resource-sensitive systems. This includes not only resource analysis, but also functional correctness and security. I worked on two projects at Radboud University: Go-Green, developing a green, self-learning, user-centric home automation system, and CHARTER, which developed a chain of tools for the generation of safe, correct and resource-efficient software for the aeronautical, automotive and surveillance industry.

During my PhD, I have co-developed an automated analysis for energy consumption of software (given a set of hardware models). This analysis is implemented in the tool ECAlogic. Results on loop-bound analysis and heap and stack space usage analysis for Java software are implemented in the tool ResAna.

Contact

NASA Research Park
Building 19, Room 1006
Moffett Field, CA 94035

Tools

JayHorn
SPF-WCA
ECAlogic
ResAna

Events

NASA Formal Methods 2017

Publications

Scientific peer-reviewed publications

Technical reports

Non-scientific

Poster presentations

PhD Thesis