Verifying Parallel Loops with Separation Logic

Stefan Blom, Saeed Darabi, Marieke Huisman

This paper proposes a technique to specify and verify whether a loop can be parallelised. Our approach can be used as an additional step in a parallelising compiler to verify user…