This paper presents a verification technique for a concurrent Java-like language with reentrant locks. The verification technique
is based on permissionaccounting separation logic. As usual, each lock is associated with a resource invariant, i.e., when
acquiring the lock the resources are obtained by the thread holding the lock, and when releasing the lock, the resources are
released. To accommodate for reentrancy, the notion of lockset is introduced: a multiset of locks held by a thread. Keeping
track of the lockset enables the logic to ensure that resources are not re-acquired upon reentrancy, thus avoiding the introduction
of new resources in the system. To be able to express flexible locking policies, we combine the verification logic with value-parameterized
classes. Verified programs satisfy the following properties: data race freedom, absence of null-dereferencing and partial
correctness. The verification technique is illustrated on several examples, including a challenging lock-coupling algorithm.