IMDEA Software

IMDEA initiative

Home > Events > Software Seminar Series > 2011 > Pattern-based verification of concurrent program

Tomas Poch

Thursday, January 20, 2011

11:00am Meeting room 302 (Mountain View), level 3

Tomas Poch, Research Intern, IMDEA Software Institute

Pattern-based verification of concurrent program

Abstract:

Reachability of a program location in the concurrent program is an undecidable problem. The pattern based verification is a technique deciding the related problem - whether the program location is reachable assuming that the threads are interleaved in a way corresponding to the given pattern. The pattern takes the form w_1* … w_n* - sequence of words, where each of them can repeat arbitrarily many times. The talk will formulate the task of pattern based verification as a language problem and present the decision procedure in this manner. The talk will also cover the application of the technique in context of parallel processes communicating in the rendez-vous style as well as parallel processes with shared memory, touch the recent complexity results and comment on the ongoing work on the tool implementation.