| Faculty name: | Azadeh Farzan |
|---|---|
| Research area: | Concurrent programs |
| Campus address: | BA 3252 |
| Campus phone: | (416) 946-3983 |
| Email address: |
azadeh [at] cs.toronto.edu
|
| Number of students: | 1-2 |
| Skills required: |
|
We are currently working on a static analysis tool for concurrent programs. The goal of our project is to automatically detect or prove the absence of defects in multi-threaded code without actually running it (for example, we might want to prove that an array access is never out of bounds, or that a pointer can not be null). If you're familiar with computability theory, you may recognize that this task is impossible in general, which is one of the more interesting things about our field. Despite this (minor) setback, similar tools (mostly for single-threaded code) have been successfully applied to improve our confidence in safety-critical code (for example, code that runs on space shuttles, cars, planes, etc). Our current line of research aims at making some of the classic techniques for program analysis work in the presence of concurrency. So if you'd like to spend the summer saving lives and doing impossible things, you're encouraged to apply.
This project has a strong theoretical basis. You will have the opportunity to learn a lot of things by participating. But, our goal is to propose useful algorithms that can help verify real-world softwares. Therefore, we put our ideas to test by implementing them and testing them.
The tool is primarily written in OCaml, so if you know OCaml (or another functional language like ML, Haskell, or Scheme), that's a big plus. Helpful courses to have taken include CSC324 (Principles of Programming Languages), CSC488 (Compilers and Interpreters), and CSC410 (Software Testing and Verification) (although, of course, we don't expect applicants to have taken all of these courses).