Tue 17 Jan 2023 14:00 - 15:00 at Arlington - Keynote and contribution paper Chair(s): Michael Emmi

Algebraic commutativity has long been used as an effective abstraction technique for improving software performance and easing the burden of reasoning about program correctness. But how do we know whether code commutes, i.e. that C1;C2 = C2;C1? Commutativity is a somewhat off-beat property, spanning multiple executions yet foiling many well-known relational reasoning tricks such as alignment.

In this talk, I will highlight the challenges in automating commutativity reasoning, steps that have been made in the community, applications, and avenues for the road ahead. I will also discuss automatic synthesis of commutativity conditions, and how to enable parallelism by incorporating such commutativity conditions directly into the programming language.


Eric Koskinen is an Associate Professor at Stevens Institute of Technology. In 2021, he was appointed to the endowed Charles Berendsen Professor of Computer Science. Dr. Koskinen’s research focuses on reliable and efficient software, through automated software verification, parallelization, and language advances that improve the way programmers develop concurrent software. Previously, Dr. Koskinen received a Ph.D in Computer Science from the University of Cambridge, spent time at IBM Watson and Microsoft, and was a Software Engineer at Amazon.com.


In recent years, I have focused on new techniques and tools to verify commutativity conditions, synthesize commutativity conditions, or use them as part of our new programming language, Veracity.

Tue 17 Jan

Displayed time zone: Eastern Time (US & Canada) change

14:00 - 15:30
Keynote and contribution paperVMCAI at Arlington
Chair(s): Michael Emmi Amazon Web Services
Verifying, Inferring and Exploiting Code Commutativity
Eric Koskinen Stevens Institute of Technology