The ever-increasing deployment of autonomous Cyber-Physical Systems (CPSs) (e.g., autonomous cars, UAV) exacerbates the need for efficient formal verification methods. In this setting, the main obstacle to overcome is the huge number of scenarios to be evaluated. Statistical Model Checking (SMC) is a simulation-based approach that holds the promise to overcome such an obstacle by using statistical methods in order to sample the set of scenarios. Many SMC tools exist, and they have been reviewed in several works. In this paper, we will overview Monte Carlo-based SMC tools in order to provide selection criteria based on Key Performance Indicators (KPIs) for the verification activity (e.g., minimize verification time or cost) as well as on the environment features, the kind of system model, the language used to define the requirements to be verified, the statistical inference approach used, and the algorithm implementing it. Furthermore, we will identify open research challenges in the field of (SMC) tools.

Social media can be used as a data source for mining public opinion on online discrimination including gender stereotypes. Monitoring data from different social platforms (X, Facebook, Instagram) may provide useful insights on cyber-violence and misogyny. In this study, we compare two different topic modelling techniques and evaluate the different patterns that arise by analyzing Italian texts from these platforms, containing keywords related to gender violence. In particular, we compare Latent Dirichlet Allocation (LDA), a Bayesian method, with BERTopic, a clustering approach based on BERT embeddings. The latter has the advantage of classifying the text while the first one is purely probabilistic. Even though LDA results are sometime hardly interpretable, because the most frequent words tend to appear too often, while BERTopic tends to separate better at the price of having a big concentration in few clusters, LDA seems to outperform BERTopic in terms of number and topic quality.