Parallel Proofs for Parallel Programs | Computer Science Department at Princeton University

Date and Time

Wednesday, March 25, 2015 - 12:30pm to 1:30pm

Location

Computer Science Small Auditorium (Room 105)

Type

CS Department Colloquium Series

Speaker

Zachary Kincaid, from University of Toronto

Host

David Walker

Zachary Kincaid

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.