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
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.
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.
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:
