Skip to main content

Program Analysis Research

Our program analysis research focuses on verifying concurrent programs through various methods.

Our research

We use formal verification techniques to ensure correctness and security in software programs. We use a variety of methods for program analysis, including:

  • summary-based approaches
  • rely-guarantee reasoning
  • concurrent separation logic
  • type systems

Our Advanced Model-Based Engineering and Reasoning (AMBER) group leads our program analysis research. 

Research projects