Low-level code verification based on CSP models

Abstract

This paper contributes to the broad field of software verification by proposing a methodology that uses CSP to verify implementations of real-life multithreaded applications. We therefore use CSP to formalize the compiler intermediate representation of a program. Our methodology divides the low-level representation into three parts: an application-specific part, describing the behavior of threads; a domain-specific part, which encapsulates low-level software concepts such as scheduling; and a platform-specific part, which is the hardware model. These three parts form a low-level CSP model that enables us to prove properties, e.g. the absence of race conditions in the model, by either model checking or theorem proving. The application-specific part is synthesized from the LLVM intermediate representation of a multithreaded program. © 2009 Springer-Verlag Berlin Heidelberg.