True Concurrency and Atomicity

Concurrent software is notoriously error-prone due to the possible unexpected interactions between concurrently executing processes. Testing is often not effective in discovering such errors since such intereferences heavily depends on the chosen scheduling and can appear very rarely. In the book we propose an approach for statically proving the absence of undesired interferences in concurrent programs. The approach is based on the definition of a so-called true concurrent semantics of the program which explicitly describes the possibly concurrent computation steps and their mutual dependencies. In the analysis we focus on atomicity properties, which assert that a program block acts in any computation as it were executed in isolation.