 Most recently, formal methods for checking correctness based on a combination of logical and statistical analysis have given new stimulus to this research area: the ability of Separation Logics (Reynolds, 2002) to offer a representation of the logical behavior of the physical memory of computational systems, and the possibility of considering probabilistic distributions of inputs as statistical source of errors, have allowed formal correctness check of large interactive systems like the Facebook platform (see also Pym et al. 2019).