Abstract Federated learning (FL) is a machine learning setting where clients keep the training data decentralized and collaboratively train a model either under the coordination of a central server (centralized FL) or in a peer-to-peer network (decentralized FL). Correct orchestration is one of the main challenges. In this paper, we formally verify the correctness of two generic FL algorithms, a centralized and a decentralized one, using the Communicating Sequential Processes (CSP) calculus and the Process Analysis Toolkit (PAT) model checker. The CSP models consist of CSP processes corresponding to generic FL algorithm instances. PAT automatically proves the correctness of the two generic FL algorithms by proving their deadlock freedom (safety property) and successful termination (reachability and liveness property). The CSP models are constructed as a faithful representation of the real Python code and are expressed directly in CSP# language that PAT uses. Then they are automatically checked top-down by PAT. The Python code follows a restricted actor-based programming model, and the construction of CSP# code from such Python code is performed systematically. The process is described in detail, ensuring that the models correspond to the actual code. It represents a basis for developing tools for automatic translation of certain classes of Python code to CSP models, expressed in CSP#.

Code smells are structures in code that often harm its quality. Manually detecting code smells is challenging, so researchers proposed many automatic detectors. Traditional code smell detectors employ metric-based heuristics, but researchers have recently adopted a Machine-Learning (ML) based approach. This paper compares the performance of multiple ML-based code smell detection models against multiple metric-based heuristics for detection of God Class and Long Method code smells. We assess the effectiveness of different source code representations for ML: we evaluate the effectiveness of traditionally used code metrics against code embeddings (code2vec, code2seq, and CuBERT). This study is the first to evaluate the effectiveness of pre-trained neural source code embeddings for code smell detection to the best of our knowledge. This approach helped us leverage the power of transfer learning – our study is the first to explore whether the knowledge mined from code understanding models can be transferred to code smell detection. A secondary contribution of our research is the systematic evaluation of the effectiveness of code smell detection approaches on the same large-scale, manually labeled MLCQ dataset. Almost every study that proposes a detection approach tests this approach on the dataset unique for the study. Consequently, we cannot directly compare the reported performances to derive the best-performing approach.