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.
The reachability problem is undecidable for programs with both recursive procedures and multiple threads with shared memory. One approach to resolve this problem is to use context-bounded reachability, i.e. to consider only those runs in which the active thread changes at most k times, where k is fixed. However, until recently, context-bounded reachability has been only a theoretical possibility, primarily because of its prohibitive worst-case runtime. In the talk, which presents joint work with Dejvuth Suwimonteerabuth and Javier Esparza, I will talk about an improvement that alleviates this problem. The approach has been implemented in the tool jMoped.