The LSV seminar takes place on Tuesday at 11:00 AM. The usual location is the conference room at Pavillon des Jardins (venue). If you wish to be informed by e-mail about upcoming seminars, please contact Stéphane Le Roux and Matthias Fuegger.
The seminar is open to public and does not require any form of registration.
Automated verification of multi-threaded programs requires explicit identification of the interplay between interacting threads, so-called environment assumptions, to enable scalable reasoning. Once identified, these assumptions can be used for reasoning with one program thread at a time, which is possible by using the respective environment assumption to model the interleaving with other threads. Finding adequate assumptions that are sufficiently precise to yield conclusive results and yet keep track only of necessary facts about the execution environment in order to scale well is a major challenge. In this talk I will present a constraint-based technique for the inference of such assumptions. Our technique automatically steers towards an optimal precision/efficiency trade-off between the extremes of efficient, but incomplete thread-modular reasoning and complete, but prohibitively expensive consideration of all interleavings. For this task, we pinpoint a declarative formulation of modular verification that allows one to express requisite environment assumptions using constraints and admits algorithmic solutions based on abstract fixpoint checking. I will describe an application of our environment assumption inference for the verification of reachability and termination properties of multi-threaded programs. Joint work with Ashutosh Gupta and Corneliu Popeea