Parallel Proofs for Parallel Programs

Tuesday, February 17, 2015 -
4:00pm to 5:00pm
Room 1240, CS Building

Speaker Name: 

Zachary Kincaid

Speaker Institution: 

University of Toronto




Speaker's abstract:  Writing reliable multi-threaded software is hard. My research aims to make it easier by developing program analysis algorithms that automatically verify that multi-threaded programs are free of certain types of errors (e.g., dividing by zero, overflowing buffers, or de-referencing null pointers). The challenge posed by multi-threading to program analysis is that parallelism creates an explosion in the number of behaviors that must be examined by a program analyzer in order to prove the absence of faults. This challenge is typically 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 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 finding parallel proofs for parallel programs.

About the speaker:  Zachary Kincaid is a Ph.D. 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 reliable, secure and efficient 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.