salle A. Turing CE4
7 janvier 2014 - 14h00
Automated verification of multi-threaded programs
par Corneliu Popeea de Technische Universitaet Muenchen
Résumé : My research aims to provide techniques for building automated
verification technology for the multi-core computing era. The last
fifteen years have provided significant progress in how automated
verification technology helps in building sequential software. Despite
this success, and despite significant advances in testing
multi-threaded programs, automated verification technology is still in
its infancy when applied to multi-threaded programs.
This talk describes how techniques used successfully to verify
sequential programs can be made effective for concurrent program
verification using compositional reasoning. Without compositionality,
automated reasoning seldom scales to the reign of concurrent
systems. The inspiration of this work lies in compositional methods
developed in the eighties, e.g., rely-guarantee and Owicki-Gries
reasoning. Based on these reasoning methods, verification of
interesting program properties including safety and termination can be
automated using a formalism based on Horn clauses.
