Pattern-based verification of concurrent programs
Decanato - Facoltà di scienze informatiche
Data d'inizio: 14 Luglio 2011
Data di fine: 15 Luglio 2011
The Faculty of Informatics is pleased to announce a seminar given by Tomas Poch
DATE: Thursday, July 14th, 2011
PLACE: USI Università della Svizzera italiana, room SI-006, Black building (Via G. Buffi 13)
TIME: 11.30
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.
BIO:
Tomas Poch received his PhD at Charles University in Prague. He is interested in software behavior modeling and verification. He worked on the technique presented in this talk during his internship at IMDEA Software Foundation under the supervision of Pierre Ganty.
HOST: Prof. Natasha Sharygina
