We investigate the pedagogical impact of Graphical Loop Invariant Based Programming (GLIBP) in an introductory programming course. This approach encourages students to visually model the objects and variables handled in the loop, before implementing it. To evaluate the efficiency of this GLI model, a four-condition A/B/C/D test was conducted across two problems, with students receiving varying levels of scaffolding (from no support to a fully constructed GLI). Analysis of students’ code showed that a well-designed GLI reduced errors related to the loop guard and the update of variables. However, many students struggled to understand or represent a GLI. The fill-in-the-blank GLI version, in particular, often added cognitive load rather than reducing it. Three recommendations emerged: train students to interpret a provided GLI when writing code; second, teach students to sketch their own model by recognizing similarities to previously solved problems; finally, guide students with questions to ensure all necessary variables and relationships are properly identified.

We present CAFÉ, a learning platform designed to introduce computer science students to Formal Methods (FM). CAFÉ aims to scaffold students' structural thinking (in contrast with operational thinking) by promoting the practice of Graphical Loop Invariant Based Programming (GLIBP). In the GLIBP approach, students solve loop-based problems by first constructing a Graphical Loop Invariant (GLI) before deriving the corresponding code. The GLI is an informal diagrammatic representation of the loop invariant. It illustrates the variables involved in the loop, their properties, and the relationships between them. To enable automated feedback, students complete a blank GLI, a box-based version of the GLI. Beyond evaluating the code students submit, CAFÉ provides personalized feedback on students' GLI and its alignment with the code. In this demo, we walk through CAFE from both a student's and a teacher's perspective. We show how the tool supports GLI design and provides feedback. We then present how a teacher can encode programming challenges together with a corresponding blank GLI.

Nowadays, employers highly value soft skills, yet many students lack these fundamental abilities. Teaching soft skills involves fostering active student participation and facilitating communication of technical knowledge among peers. This approach presents challenges: (i) creating an engaging learning environment; (ii) ensuring students get timely feedback; (iii) finding an approach that is not too time-consuming for instructors to prepare. The Collaborative Design & Build (CDB) activity, described in this paper, was designed to respond to these challenges. It simulates a real-life scenario, triggering students' interest. The success of this collaborative activity hinges on students working together in a structured chain, where each team builds upon and contributes to the success of the others. This fosters student engagement and accountability as they realize the impact of their actions on the entire chain. This pedagogical approach has already been adopted by four universities abroad. This paper shows how it can be deployed in different courses. Finally, it also discusses how students perceived the activity through four soft skills: collaboration, communication, problem solving and critical thinking. These skills were selected based on their relevance, both in the context of the collaborative activity and in the job market. They are also aligned with the ''4C's of 21st Century skills''. Results show that while students initially struggled with soft skills, consistent practice throughout the semester boosted their confidence, especially in communication. This makes the activity particularly relevant in the classroom, as communication is considered as the most important soft skill for the future.

This paper considers CAFE 2.0, an Automated Feedback system designed to support students' diagrammatic reasoning in STEM disciplines. CAFE 2.0 relies on a predefined error library, metamodels, and rules to correct students' solutions and deliver formative feedback. Implementing such a system requires a balance between constraining the solution syntax to enable AF and leaving freedom to students to reflect on their solution. This paper aims to evaluate whether the level of freedom provided by our AF system sufficiently prepares students for exams. In the exam, they must reason and construct solutions starting with a blank page. This study is conducted in an introductory programming course (CS1), based on two semesters (in 2022 and 2023), where CAFE 2.0 supports online homework. Findings reveal a discrepancy between students' performance in online homework and their success on exams. While many students feel comfortable with fill-in-the-blank diagrams in their homework, they struggle with the open-ended nature of exam tasks. Our results show that, among the students who succeeded in their online homework in 2023, 20% were still unable to produce any diagram in the exam. Additionally, 70% of them could not correctly provide a text description of their solution. To overcome this limitation, this paper proposes an enhanced system that integrates predefined rules with Large Language Models (LLMs). In this framework, LLMs serve as translators. Students can freely create their diagrams and annotate them with their own textual descriptions using a drawing editor. The LLM then maps these representations into a more structured format that aligns with predefined rules. In this way, CAFE 2.0 can generate accurate feedback. This transformed representation retains the same informational content as the original, differing only in format. This feature will offer students greater flexibility in constructing their solutions while ensuring that feedback remains precise and consistent by limiting the role of LLMs to translation rather than feedback generation.

In computer science, teaching first-year students to approach problems at varying levels of abstraction is both essential and challenging. While abstraction is a key component of problem solving, many students struggle with thinking abstractly. When presented with a problem, students often rush into coding, feeling closer to a solution through immediate feedback from the compiler or by simulating their code. However, this approach can cause them to overlook essential details, as their code may not account for all possible input scenarios. To address this issue, we introduced a programming methodology in our Introduction to Programming (CS1) course. This methodology requires students to first construct a graphical representation of their solution, ensuring coverage of all potential input cases, before translating it into code. To support regular practice in this diagrammatic reasoning process, we developed a learning tool called CAFÉ 2.0. Over the course of the semester, students use CAFÉ 2.0 to solve problems by submitting both a graphical model of their solution and the associated code implementation. In addition to evaluating the final code, CAFÉ 2.0 provides personalized feedback on the graphical model and how well it aligns with the code. This feedback guides students in refining their model and code, and resubmit them to get new feedback. CAFÉ 2.0's unique feature is its ability to automatically generate feedback on graphical models within an interactive online environment, fostering an engaging and supportive learning experience.

While IPv6 was standardized in the 90’s, only the last decade has seen a growth in its global adoption. In addition to dealing with IPv4 addresses exhaustion, IPv6 comes with a mechanism, called IPv6 Extension Header (IPv6 EH), allowing the protocol to be more flexible and extensible. In this paper, we investigate how IPv6 EHs are processed in the network. In particular, we focus on the survivability of IPv6 EHs, i.e., the fact that an IPv6 EH traverses the Internet and arrives unmodified at the destination. We first design experiments in a controlled environment, testing different IPv6 EHs and sizes on different routers from various vendors. Then, we confront our observations with several measurement campaigns between vantage points hosted by different Cloud Providers (CPs) around the world, and we compare them to the responses received from a survey of operators. Our results show that the survivability of IPv6 EHs is quite limited (around 50

BGP communities are widely used by operators to encode routing metadata for traffic engineering, policy enforcement, and operational debugging. However, ≈90% of observed communities lack public documentation, limiting their utility for research and operational analysis. Among these, city-level communities offer valuable geographic insight into routing behavior, yet remain largely untapped. In this paper, we develop a scalable method to infer the geographic meaning of undocumented city communities using BGP data. We validate our approach against a ground truth dataset covering 1,482 city communities and through operator feedback. Applied to data from May 2025, our algorithm infers the locations of 80% of city communities with a precision of 70 km or better. We publish all code and datasets to support reproducibility and further research.

Over the past two decades, network measurement infrastructures have witnessed significant development and widespread adoption. Internet measurement platforms have become common and have demonstrated their relevance in Internet understanding and security observation. However, despite their popularity, those platforms lack of flexibility and reactivity, as they are usually used for longitudinal measurements. Consequently, critical security and Internet-related events may evade detection. Concurrently, the evolution of operating systems towards virtual machines (VMs) has been notable, particularly with the emergence of unikernels—ultra-lightweight VMs tailored for specific applications by including only the essential components. This paper advocates for the integration of unikernels into measurement infrastructures to enhance their flexibility and efficiency. We introduce $v\mathbf{TNT}$ , a proof-of-concept unikernel-based implementation of TNT, a traceroute extension capable of discovering MPLS tunnels. This paper documents the full toolchain for porting TNT into a unikernel and evaluates $v\mathbf{TNT}^{\prime}\mathbf{s}$ performance in comparison to conventional methodologies. Additionally, we explore a practical use case scenario demonstrating the utility of $v\mathbf{TNT}$ . The source code for $v\mathbf{TNT}$ is publicly available on Gitlab.

In-Situ Operations, Administration, and Maintenance (Ioam) gathers telemetry and operational information along a path, within packets. Up to now, Ioam header and data are carried in plain text without any protection against data-altering nodes or middleboxes. However, deploying Ioam in an un-trusted or semi-trusted environment requires at least integrity protection. This paper leverages and analyzes work in progress about Ioam integrity protection and explains why the currently proposed solution can be improved. Accordingly, several alternative solutions are discussed, implemented in the Linux kernel, and evaluated. Based on the results, guidance is provided for standardization. Our source code is publicly available.

This paper addresses the difficulties students face when learning and practicing pointers (i.e., variables storing the memory address of another variable as its value) in a computer programming class. To improve their understanding and practice, we have developed Tartare, an automatic C pointer statement and feedback generator. By creating statements with automatic feedback, students are given the opportunity to practice at will, each time on a different instance. In addition, if the statement must be done remotely and accounts in the final grade, Tartare discourages academic dishonesty since each student faces their own statement to solve. This paper describes the techniques implemented in Tartare, relying on a pattern template-based approach. The statement variety of Tartare is evaluated. Finally, current limitations and further improvements are discussed. We believe our approach for Tartare can be transposed for automatic exercises generation in various other fields.

Mastering abstraction skills is a crucial learning outcome for computer science students. However, students often struggle with these skills and can quickly feel overwhelmed when required to apply them. In our Introduction to Programming (CS1) course, we explicitly teach abstraction by providing a framework where students must solve problems from higher to lower levels of abstraction. This paper presents this framework and demonstrates its application through a collaborative activity that simulates large-scale development projects. This paper also examines students’ perception and performance at each level of abstraction over three sessions of the activity. The findings highlight the concepts that should be prioritized to better prepare students for each session. They also emphasize the importance of illustrating to students the function of abstraction in problem-solving and its relevance to their future work life, as a complement to traditional academic activities.

In the context of contemporary data center networks (DCNs), optimizing resource utilization and preventing congestion are critical objectives. This paper introduces Smoothie, a dynamic path load balancer specifically designed for real-time congestion management using Inband Network Telemetry (Int) for collecting network state pieces of information and Segment Routing Version 6 (SRv6) for rerouting traffic. Leveraging the programmable nature of the P4 programming language, Smoothie effectively achieves its goals. Our experimental results showcase Smoothie’s superiority over conventional Equal-Cost Multipath (ECMP) routing and its competitive performance compared to other congestion-aware load balancing solutions. We assert that these findings can be attributed to Smoothie’s proactive congestion response, which minimizes the necessity for TCP congestion window resizing, and its ability to intelligently reroute flows onto optimal paths, thereby substantially reducing route flapping. These outcomes highlight Smoothie’s potential to significantly enhance network performance within DCNs. Furthermore, Smoothie offers enhanced manageability, ease of maintenance, and simplified deployment through a centralized controller, further underscoring its value.

The Bitcoin protocol relies on scripts written in Script, a simple Turing-incomplete stack-based language, for locking the money carried over the Bitcoin network. This paper explores the usage of symbolic execution for finding transactions that permit to redeem the money without being the legitimate owner. In particular, we show in detail how using insecure scripts could have led to security breaches, resulting in bitcoins theft. Our contributions include (i) a quantification of the vulnerable script instances over the full Bitcoin history up to Feburary, 4th 2023; (ii) the development and open source publication of a symbolic execution tool, called Chaussette; (iii) the description of how to use Chaussette to perform the attack; and, (iv) a discussion around a way to secure vulnerable money.

This paper aims at evaluating how content distribution is spread between IPv4 and IPv6 within popular websites. Our measurement tool, based on a headless browser technology, has shown that most websites do not opt forIPv4 or IPv6 alone, but rather for a Mixed infrastructure where both protocols are required. Within this Mixed context, data shows that content delivery through IPv4 is predominant.

Shaping first-year students' minds to solve problems at different levels of abstraction is both important and challenging. Although abstraction is a crucial skill in problem-solving, especially in STEM subjects, students often struggle with abstract thinking. They tend to focus their efforts on concrete aspects of the problem, where they feel more comfortable and closer to the final solution. Unfortunately, this approach can cause them to overlook critical details related to the problem or its solution. To address this issue in our Introduction to Programming (CS1) course, we introduced a programming methodology that requires students to create a graphical representation of their solution and then derive the code from it. To enable them to practice this diagrammatic reasoning approach on a regular basis, we developed a learning tool called CAFE 2.0. It facilitates a semester-long activity in which students solve problems by submitting both a graphical representation of their solution and its implementation. Further to checking the final implementation, CAFE 2.0 also provides personalized feedback on how students have graphically modeled their solution and how consistent it is with their code. This paper presents an overview of the features of CAFE 2.0 and the methodology it currently supports in the context of our CS1 course. Then, using a survey and learning analytics, this paper evaluates students' interactions with CAFE 2.0. Finally, the potential for extending CAFE 2.0 to other STEM disciplines is discussed.

The rise of cryptocurrencies has created new avenues for criminal money exchanges. Among various techniques, Bitcoin address clustering plays a crucial role in detecting and grouping addresses owned by the same entity. This fundamental step is essential for deanonymizing addresses and analyzing the flow of funds in the blockchain. This advancement contributes to the battle against illicit commerce, money laundering, fraud, scams, and similar activities. In this paper, we introduce two new heuristics, NSS and PEKET. NSS leverages Bitcoin non-standard scripts, while PEKET exploits the re-use of public keys to establish connections controlled by the same entity. Our contributions encompass (i) the detailed explanation of these two novel methods; (ii) the open-source publication of the tools we developed; and, (iii) the assessment of these heuristics using a proprietary extensive dataset of labeled addresses, which achieve precision levels of 1.0 and 0.979 respectively.

The last few years in the software engineering field have seen a paradigm shift from monolithic applications towards architectures in which the application is split in various smaller entities (i.e., microservices) fueled by the improved availability and ease of use of containers technologies such as Docker and Kubernetes. Those microservices communicate with each other using networking technologies in place of function calls in traditional monolithic software. In order to be able to evaluate the potential, the modularity, and the scalability of this new approach, many tools, such as microservices benchmarking, have been developed with that objective in mind. Unfortunately, many of these tend to focus only on the application layer while not taking the underlying networking infrastructure into consideration, leading to difficulties in developing and testing telemetry tools. In this paper, we introduce and evaluate the performance of a new modular and scalable tool, MicroServices Topology Generator (MSTG), that allows one to simulate both the application and networking layers of a microservices architecture. Based on a topology described in Yaml format, Mstg generates the configuration file(s) for deploying the architecture on either Docker Compose or Kubernetes. Furthermore, Mstg encompasses telemetry tools, such as Application Performance Monitoring (APM) relying on OpenTelemetry and in-band telemetry (e.g., IOAM). This paper also discusses a use case in whic Mstg finds a suitable usage.