Symbolically Modeling Concurrent MCAPI Executions ∗

Improper use of Inter-Process Communication (IPC) within con-current systems often creates data races which can lead to bugs that are challenging to discover. Techniques that use Satisfiability Mod-ulo Theories (SMT) problems to symbolically model possible exe-cutions of concurrent software have recently been proposed for use in the formal verification of software. In this work we describe a new technique for modeling executions of concurrent software that use a message passing API called MCAPI. Our technique uses an execution trace to create an SMT problem that symbolically models all possible concurrent executions and follows the same sequence of conditional branch outcomes as the provided execution trace. We check if there exists a satisfying assignment to the SMT prob-lem with respect to specific safety properties. If such an assignment exists, it provides the conditions that lead to the violation of the property. We show how our method models behaviors of MCAPI applications that are ignored in previously published techniques