Concurrent programs are notoriously difficult to write, debug, test, and verify. The subtle problems that arise from concurrent execution of statements make reasoning about these programs extraordinarily complex. The proposed research explores a solution to this problem that focuses on the modular verification of safe and deterministic concurrent programs (that is, programs that exhibit identical input-output behavior whether run sequentially or concurrently) using an abstract specification of how a software component may be safely parallelized. Enabling modular verification of programs written to take advantage of the many-core machines of today will have far-reaching implications for the performance of formally-verified applications, which do not normally take advantage of multi-core hardware because it is at present difficult to verify the functional correctness of such programs.