Aleksandar Nanevski

Date: 17:00, Thursday, August 16, 2018
Speaker: Aleksandar Nanevski
Venue: TU Wien, Favoritenstr. 9-11, Seminarraum Gödel

Abstract:

Verification of concurrent software is a notoriously difficult
subject, whose complexities stem from the inability of the
existing verification methods to modularize, and thus divide and
conquer the verification problem.

Dependent types are a formal method well-known for its ability to
modularize and scale complex mathematical proofs. But, when it
comes to programming, dependent types are considered limited to
the purely functional programming model.

In this talk I will present my recent work towards reconciling
dependent types with shared memory concurrency, with the goal of
achieving modular verification for the latter. Applying the
type-theoretic paradigm to concurrency have lead to interesting
reformulations of some classical verification ideas, and to the
discovery of novel and useful abstractions for modularizing the
proofs.

Posted in RiSE Seminar