Talk: Formal Reasoning About Programs

LIVE STREAM: https://uwmadison.zoom.us/j/97846701530?pwd=REZhVzBzMitrZExxTjNEdU1jSnBXdz09

Abstract: In this talk I will present my research in formal reasoning about programs using program logics. A program logic is a formal language based on mathematical logic for expressing and proving various properties of programs. They allow us to reason abstractly and modularly to prove properties of programs stated in terms of detailed models of program execution. State-of-the-art program logics have been extremely successful in verification of various correctness properties of intricate programs including concurrent and distributed systems. These range from reasoning about correctness of type systems of high-level functional and imperative programming languages to hardware security guarantees in assembly. This talk will focus on the application of state-of-the-art program logics to reasoning about various aspects of correctness of concurrent and distributed programs.

Bio: Amin Timany is a tenure-track assistant professor in the Logic and Semantics research group of the Department of Computer Science of Aarhus University, Aarhus, Denmark. Before joining Aarhus University in April 2020, he was a postdoctoral fellow of the Flemish research fund (FWO) at the DistriNet research group of the Department of Computer Science of KU Leuven, Leuven, Belgium. Prior to that, Amin obtained his PhD in May 2018 from KU Leuven under supervision of Prof. Bart Jacobs. Amin's research interests include formal program verification, program logics, compilers, distributed systems, type theory, proof assistants, formalization of mathematics in proof assistants, and category theory.