Certificate translation for the verification of concurrent programs

Abstract

The increasing presence of multicore execution environments is stimulating the development of concurrent software, an inherently error-prone task that affects the trust on the reliability of third-party code. There is thus a pressing need of providing verifiable evidence on a concurrent software correctness. Certificate Translation provides a means to generate verification certificates for complex functional properties. This technique, consists on progressively transferring verification results for source programs along a sequence of compilation steps. In previous work, we have shown how to transform certificates of a sequential program in the presence of compiler optimizations. In this article, we have shown that it is possible to extend certificate translation to the verification of concurrent programs, based on an Owicki/Gries-like proof system for a shared memory model. © 2010 Springer-Verlag Berlin Heidelberg.