Colloquium Speaker
Zachary Kincaid, University of Toronto
Wednesday, March 25, 12:30pm
Computer Science 105

Parallel Proofs for Parallel Programs

Today's software systems are large and complex - beyond the scope of comprehension of any one person.  My research is motivated by the question of how machines can help humans better understand their code and aid the construction of reliable, secure, and efficient systems.  Multi-threading is a long-standing obstacle to reasoning by both humans and machines.  Conventionally, this obstacle is met by developing clever ways to reason about the program as if it were executing sequentially.  In this talk, I will argue that we should embrace parallelism, not hide from it.  I will discuss new *fundamentally parallel* foundations for automated program analysis, which allow the parallelism present in a program to be explicitly maintained and enable tractable automated reasoning and succinct proofs.  In other words: my talk will be on parallel proofs for parallel programs.

Zachary Kincaid is a PhD candidate in the Department of Computer Science at the University of Toronto.  He is interested in developing automated reasoning techniques to facilitate the construction of high-performance, dependable software.  Zak's research focuses on static analysis and program verification, with a particular emphasis on multi-threaded programs.  He has also made contributions to theorem proving and program synthesis.