Verifying atomicity specifications for concurrent object-oriented software using model-checking

In recent work, Flanagan and Qadeer proposed atomicity declarations as a light-weight mechanism for specifying non-interference properties in concurrent programming languages such as Java, and they provided a type and effect system to verify atomicity properties. While verification of atomicity specifications via a static type system has several advantages (scalability, compositional checking), we show that verification via model-checking also has several advantages (fewer unchecked annotations, greater coverage of Java idioms, stronger verification). In particular, we show that by adapting the Bogor model-checker, we naturally address several properties that are difficult to check with a static type system.