Résumé | This talk will be based on the paper from POPL 2017:
Thread Modularity at Many Levels: a pearl of compositional verification
by
Jochen Hoenicke, Rupak Majumdar, and Andreas Podelski
In the paper the authors consider the problem of proving safety of (parametrized) concurrent programs. They do not propose new techniques but rather revisit some existing ones. I have found putting these techniques next to each other very interesting and thought provoking. Since the considered problem is a fundamental problem for verification, I think it is worth to see this work at the seminar.
This will not be a survey talk. Technically the talk will be very easy, as the results are straightforward. The goal is to present a view point on the problem that I have got from reading the paper. |