Program Analysis and Verification

Understanding the behavior and verifying the correctness of computer-aided systems is one of the grand challenges of contemporary computer science motivated by the undesirable effects of computer failures on human society. We concentrate on developing methods for automatic analysis and verification of selected classes of systems, devoting special attention to probabilistic programs, programs with unbounded data types, and real-world programs written in C.

What We Do

No description

Infinite-State Systems

  • We develop efficient analysis techniques for infinite-state computational models. Special attention is devoted to Vector Addition Systems with States (VASS), a natural model for programs with unbounded integer variables and parameterized systems.
  • We also study stochastic and game-theoretic extensions of VASS and selected subclasses, such as population protocols. 
No description

Probabilistic Programs

  • Probabilistic computations arise in numerous application domains, including as machine learning, data analysis and security. To ensure the correctness of such computations, we develop automated techniques for proving temporal properties of probabilistic imperative programs.
  • We also investigate questions pertaining to efficient decision-making under probabilistic uncertainty, such as determining the complexity of optimal decision making under resource constraints.
No description

Real-World Program Analysis

  • We implement algorithms for program slicing, verification, and bug-detection.
  • We participate in SV-COMP where our tool Symbiotic has won multiple medals.  
  • Check out our code on Github:


Our Team


You are running an old browser version. We recommend updating your browser to its latest version.

More info