Mark van den Brand

Leonard Tudorache, Ivan Kurtev, Mark van den Brand

Security is critical for everything relying on modern digital systems. Because almost all digital interactions are governed by the Internet and cryptographic protocols, these protocols must serve as reliable mechanisms that guarantee core security properties, such as confidentiality and integrity. Formal verification of these protocols is a critical step in securing interconnected systems. Tools such as ProVerif and Tamarin are widely employed to perform automated verification. However, their effective use demands specialized domain knowledge, creating a significant learning curve for security protocol designers who often have a security, rather than a formal verification background. We therefore need structured, accessible resources to help protocol designers to express their design and requirements in the language of the formal verification tools. To address this, we introduce a systematic and evidence-based taxonomy of security properties. This taxonomy is derived from a literature review of 53 recent studies (2022-2025) that used ProVerif and Tamarin, providing an up-to-date view of verified properties. We systematically categorize and define these properties, providing both informal definitions for intuitive comprehension and rigorous formal definitions expressed in first-order logic for clarity and consistency. We further detail modeling patterns and implement executable examples in both ProVerif and Tamarin, collected in an open repository. This work advances the state of the art by bridging the gap between theoretical security property definitions and their practical, executable verification models.

Aneesh Deogan, Wout Beks, Peter Teurlings et al.

Annotated datasets are critical for training neural networks for object detection, yet their manual creation is time- and labour-intensive, subjective to human error, and often limited in diversity. This challenge is particularly pronounced in the domain of robotics, where diverse and dynamic scenarios further complicate the creation of representative datasets. To address this, we propose a novel method for automatically generating annotated synthetic data in Unreal Engine. Our approach leverages photorealistic 3D Gaussian splats for rapid synthetic data generation. We demonstrate that synthetic datasets can achieve performance comparable to that of real-world datasets while significantly reducing the time required to generate and annotate data. Additionally, combining real-world and synthetic data significantly increases object detection performance by leveraging the quality of real-world images with the easier scalability of synthetic data. To our knowledge, this is the first application of synthetic data for training object detection algorithms in the highly dynamic and varied environment of robot soccer. Validation experiments reveal that a detector trained on synthetic images performs on par with one trained on manually annotated real-world images when tested on robot soccer match scenarios. Our method offers a scalable and comprehensive alternative to traditional dataset creation, eliminating the labour-intensive error-prone manual annotation process. By generating datasets in a simulator where all elements are intrinsically known, we ensure accurate annotations while significantly reducing manual effort, which makes it particularly valuable for robotics applications requiring diverse and scalable training data.

Mauricio Verano Merino, Jurgen Vinju, Mark van den Brand

Block-based environments are visual programming environments, which are becoming more and more popular because of their ease of use. The ease of use comes thanks to their intuitive graphical representation and structural metaphors (jigsaw-like puzzles) to display valid combinations of language constructs to the users. Part of the current popularity of block-based environments is thanks to Scratch. As a result they are often associated with tools for children or young learners. However, it is unclear how these types of programming environments are developed and used in general. So we conducted a systematic literature review on block-based environments by studying 152 papers published between 2014 and 2020, and a non-systematic tool review of 32 block-based environments. In particular, we provide a helpful inventory of block-based editors for end-users on different topics and domains. Likewise, we focused on identifying the main components of block-based environments, how they are engineered, and how they are used. This survey should be equally helpful for language engineering researchers and language engineers alike.

Muhammad Hammad, Önder Babur, Hamid Abdul Basit et al.

Source code search plays an important role in software development, e.g. for exploratory development or opportunistic reuse of existing code from a code base. Often, exploration of different implementations with the same functionality is needed for tasks like automated software transplantation, software diversification, and software repair. Code clones, which are syntactically or semantically similar code fragments, are perfect candidates for such tasks. Searching for code clones involves a given search query to retrieve the relevant code fragments. We propose a novel approach called Clone-Seeker that focuses on utilizing clone class features in retrieving code clones. For this purpose, we generate metadata for each code clone in the form of a natural language document. The metadata includes a pre-processed list of identifiers from the code clones augmented with a list of keywords indicating the semantics of the code clone. This keyword list can be extracted from a manually annotated general description of the clone class, or automatically generated from the source code of the entire clone class. This approach helps developers to perform code clone search based on a search query written either as source code terms, or as natural language. In our quantitative evaluation, we show that (1) Clone-Seeker has a higher recall when searching for semantic code clones (i.e., Type-4) in BigCloneBench than the state-of-the-art; and (2) Clone-Seeker can accurately search for relevant code clones by applying natural language queries.

Sangeeth Kochanthara, Niels Rood, Arash Khabbaz Saberi et al.

The scope of automotive functions has grown from a single-vehicle as an entity to multiple vehicles working together as an entity, referred to as cooperative driving. The current automotive safety standard, ISO 26262, is designed for single vehicles. With the increasing number of cooperative driving capable vehicles on the road, it is now imperative to systematically assess the functional safety of architectures of these vehicles. Many methods are proposed to assess architectures with respect to different quality attributes in the software architecture domain, but to the best of our knowledge, functional safety assessment of automotive architectures is not explored in the literature. We present a method, that leverages existing research in software architecture and safety engineering domains, to check whether the functional safety requirements for a cooperative driving scenario are fulfilled in the technical architecture of a vehicle. We apply our method on a real-life academic prototype for a cooperative driving scenario, platooning, and discuss our insights.

Muhammad Hammad, Önder Babur, Hamid Abdul Basit et al.

Programmers often reuse code from source code repositories to reduce the development effort. Code clones are candidates for reuse in exploratory or rapid development, as they represent often repeated functionality in software systems. To facilitate code clone reuse, we propose DeepClone, a novel approach utilizing a deep learning algorithm for modeling code clones to predict the next set of tokens (possibly a complete clone method body) based on the code written so far. The predicted tokens require minimal customization to fit the context. DeepClone applies natural language processing techniques to learn from a large code corpus, and generates code tokens using the model learned. We have quantitatively evaluated our solution to assess (1) our model's quality and its accuracy in token prediction, and (2) its performance and effectiveness in clone method prediction. We also discuss various application scenarios for our approach.

Manoj Kannan Soundarapandian, Kunal Suri, Juan Cadavid et al.

The dawn of the fourth industrial revolution, Industry 4.0 has created great enthusiasm among companies and researchers by giving them an opportunity to pave the path towards the vision of a connected smart factory ecosystem. However, in context of automotive industry there is an evident gap between the requirements supported by the current automotive manufacturing execution systems (MES) and the requirements proposed by industrial standards from the International Society of Automation (ISA) such as, ISA-95, ISA-88 over which the Industry 4.0 is being built on. In this paper, we bridge this gap by following a model-based requirements engineering approach along with a gap analysis process. Our work is mainly divided into three phases, (i) automotive MES tool selection phase, (ii) requirements modeling phase, (iii) and gap analysis phase based on the modeled requirements. During the MES tool selection phase, we used known reliable sources such as, MES product survey reports, white papers that provide in-depth and comprehensive information about various comparison criteria and tool vendors list for the current MES landscape. During the requirement modeling phase, we specified requirements derived from the needs of ISA-95 and ISA-88 industrial standards using the general purpose Systems Modeling Language (SysML). During the gap analysis phase, we find the misalignment between standard requirements and the compliance of the existing software tools to those standards.