corina Corina Pasareanu, ACM Distinguished Scientist

Email: corina.pasareanu@sv.cmu.edu

I am doing research in software engineering at NASA Ames, in the Robust Software Engineering group. I am employed by Carnegie Mellon University, where I am Associate Research Professor with CMU CyLab at the Silicon Valley campus. I also hold a courtesy appointment with the CMU ECE department.

rody Rody Kersten, Postdoctoral Researcher

Email: rody.kersten@sv.cmu.edu
Website: https://www.andrew.cmu.edu/user/rkersten

My research interest is software analysis in the broad sense: automated techniques to establish program properties such as functional correctness, safety, security and efficiency. In particular, I am interested in analysing consumption of resources such as time, memory and energy.

Currently, I work on the ISSTAC project, sponsored by the DARPA STAC program. Here, I apply resource analysis in the search for vulnerabilities to algorithmic complexity based attacks (Denial-of-Service). If a certain input causes a software system to consume an impractically large amount of resources, an adversary could use this input to deny service to benign users or otherwise disable the system. My research aims to identify such vulnerabilities in a semi-automated manner.

kasper Kasper Søe Luckow, Postdoctoral Researcher

Email: kasper.luckow@sv.cmu.edu
Website: https://www.andrew.cmu.edu/user/kluckow

Researching for the Integrated Symbolic Execution for the Space-Time Analysis of Code (ISSTAC) project (funded by DARPA STAC). I also worked on a NASA project on safety analysis of flight critical systems. My current focus is on identifying algorithmic complexity vulnerabilities using symbolic execution with heuristic exploration.

Research Interests

  • Symbolic Analysis: I work on Symbolic PathFinder, a symbolic execution engine built on the software model checker Java PathFinder. I also maintain JDart, a dynamic symbolic execution engine.
  • Probabilistic Software Analysis: I’m working on analysis of software placed in stochastic environments, e.g., with the goal of quantifying how likely a target event is to occur.
  • Machine Learning: I’m investigating how to leverage machine learning techniques as a heuristic for symbolic analysis. I also used machine learning for mining log data from flight-critical systems.

Alumni

Following people have been associated with VeriS:

sang Quoc-Sang Phan, Postdoctoral Researcher

Website: http://qsphan.github.io/

My research aims to analyse programs and provide a quantitative assessment of security. To this end, I use symbolic execution for program analysis, and model counting for quantification of information.