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


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.


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




NASA Formal Methods 2017


Scientific peer-reviewed publications

Technical reports


Poster presentations

PhD Thesis