The strongest level of consistency in concurrent/distributed storage systems consists in ensuring that every issued write operation is immediately visible to all processes. However, for performance reasons, storage systems do not guarantee in general strong consistency, but they rather implement weaker consistency models where different processes may see different sets of writes along computations, sometimes in different orders. The conditions on the visibility order guaranteed by a system corresponds to its memory consistency model. Weak consistency models admit complex and unintuitive behaviors, making very hard the task of programming applications. This motivates investigating the two verification problems:

1.⁠ ⁠checking the correctness of an application program running over a weak consistency model;

2.⁠ ⁠checking the robustness of an application program w.r.t. consistency weakening, which means that the set of visible behaviors of the program stays unchanged under the weaker consistency model.

Solving these problems is nontrivial due to the fact that capturing program semantics under weak consistency models requires reasoning about infinite-state systems with queues, which threaten in general decidability. The talk gives a broad presentation of the issues related to the formal modeling and verification of correctness and robustness, and some of the main results in this area. The talk is based on several joint works with students and colleagues.