Verification of Higher-Order Concurrent Programs with Dynamic Resource Creation

We propose a sound and complete static verification method for (higher-order) concurrent programs with dynamic creation of resources, such as locks and thread identifiers. To deal with (possibly infinite) resource creation, we prepare a finite set of abstract resource names and introduce the notion of scope-safety as a sufficient condition for avoiding the confusion of different concrete resources mapped to the same abstract name. We say that a program is scope-safe if no resource is used after the creation of another resource of the same abstract name. We prove that the pairwise-reachability problem is decidable for scope-safe programs with nested locking. We also propose a method for checking that a given program is scope-safe and with nested locking.