I am a postdoctoral researcher at ETH Zurich in the Networked Systems Group, advised by Prof. Dr. Laurent Vanbever. My research aims to improve network operations using formal methods. During (and after) my PhD, I published work on:

• safely applying network-wide configuration updates (SIGCOMM'21, SIGCOMM'23),
• verifying safety and performance properties of BGP configurations (NSDI'25, ICNP'25), and
• monitoring BGP networks at runtime (CoNEXT'25, SIGCOMM'26).

Motor-Imagery Brain-Machine Interfaces (MI-BMIs) promise direct and accessible communication between human brains and machines by analyzing brain activities recorded with Electroencephalography (EEG). Latency, reliability, and privacy constraints make it unsuitable to offload the computation to the cloud. Practical use cases demand a wearable, battery-operated device with low average power consumption for longterm use. Recently, sophisticated algorithms, in particular deep learning models, have emerged for classifying EEG signals. While reaching outstanding accuracy, these models often exceed the limitations of edge devices due to their memory and computational requirements. In this paper, we demonstrate algorithmic and implementation optimizations for EEGNET, a compact Convolutional Neural Network (CNN) suitable for many BMI paradigms. We quantize weights and activations to 8-bit fixed-point with a negligible accuracy loss of 0.4% on 4-class MI, and present an energy-efficient hardware-aware implementation on the Mr. Wolf parallel ultra-low power (PULP) System-on-Chip (SoC) by utilizing its custom RISC-VISA extensions and 8-core compute cluster. With our proposed optimization steps, we can obtain an overall speedup of 64 × and a reduction of up to 85% in memory footprint with respect to a single-core layer-wise baseline implementation. Our implementation takes only 5.82 ms and consumes 0.627 mJ per inference. With 21.0 GMAC/s/W, it is 256× more energy-efficient than an EEGNET implementation on an ARM Cortex-M7 (0.082 GMAC/s/W).

With Motor-Imagery (MI) Brain-Machine Interfaces (BMIs) we may control machines by merely thinking of performing a motor action. Practical use cases require a wearable solution where the classification of the brain signals is done locally near the sensor using machine learning models embedded on energy-efficient microcontroller units (MCUs), for assured privacy, user comfort, and long-term usage. In this work, we provide practical insights on the accuracy-cost tradeoff for embedded BMI solutions. Our proposed Multispectral Riemannian Classifier reaches 75.1% accuracy on 4-class MI task. We further scale down the model by quantizing it to mixed-precision representations with a minimal accuracy loss of 1%, which is still 3.2% more accurate than the state-of-the-art embedded convolutional neural network. We implement the model on a low-power MCU with parallel processing units taking only 33.39 ms and consuming 1.304 mJ per classification.

Operators go to great lengths to ensure their BGP networks are correct. Yet, despite their efforts, faults still happen due to software or hardware bugs, which can often have detrimental network-wide consequences. Today, all operators can do is react to such failures, often only once it is already too late. We present GhostBuster, a runtime system which monitors the execution of BGP routers and verifies their compliance with the protocol specification. Concretely, GhostBuster checks whether observed outgoing BGP messages could have been produced by incoming ones. The key challenge in doing so is that BGP routers do not necessarily process incoming messages in order, forcing one to consider all possible reorderings of input messages. While this obviously does not scale, we show that one can solve this problem efficiently by reasoning about sets of messages instead of orderings. We fully implemented GhostBuster and use it to detect (confirmed and unknown) bugs in production routers. Our evaluation on simulated networks further confirms that GhostBuster is both scalable and accurate: it never falsely reports a bug while detecting over 60% of the bugs.

Analyzing transient violations of reachability---that happen while routing protocols are re-converging---helps in improving network availability and offering more precise SLAs. The key challenge is analyzing transient violations accurately, as they can be short-lived, for all affected prefix destinations, and practically, without worsening the network's performance. Existing approaches fail to address at least one of these goals: measurement approaches are accurate but only for the prefixes they can probe or observe traffic for, while techniques that estimate the convergence time use the same crude proxy for all prefixes. To achieve all three goals, we present TRIX, a system that infers transient violation times for BGP events from logged routing events or collected BGP messages. TRIX' key insight is that we do not need to probe all destinations if we use available information to infer the router-local forwarding state, for all destinations, and reconstruct the network-wide violations from router-level state. However, the logged events contain control-plane information that is inaccurate in terms of the content and the times of the forwarding updates, while reconstructing network-wide violations requires reasoning about the flow of traffic through the network. TRIX solves these challenges by simulating the BGP control-plane, modeling the FIB-update rate, and combining the state across routers with propagation delays. To evaluate TRIX, we implement a testbed that relies on a programmable switch and uses 12 real routers. Our evaluation shows that TRIX' inferred reachability violation times are on average within 13--25ms from the ground truth, and inference scales to large networks.

BGP reconfigurations are a daily occurrence for most network operators, especially in large networks. Yet, performing safe and robust BGP reconfiguration changes is still an open problem. Few BGP reconfiguration techniques exist, and they are either (i) unsafe, because they ignore transient states, which can easily lead to invariant violations; or (ii) impractical, as they duplicate the entire routing and forwarding states, and require special hardware. In this paper, we introduce Chameleon, the first BGP reconfiguration framework capable of maintaining correctness throughout a reconfiguration campaign while relying on standard BGP functionalities and minimizing state duplication. Akin to concurrency coordination in distributed systems, Chameleon models the reconfiguration process with happens-before relations. This modeling allows us to capture the safety properties of transient BGP states. We then use this knowledge to precisely control the BGP route propagation and convergence, so that input invariants are provably preserved at any time during the reconfiguration. We fully implement Chameleon and evaluate it in both testbeds and simulations, on real-world topologies and large-scale reconfiguration scenarios. In most experiments, our system computes reconfiguration plans within a minute, and performs them from start to finish in a few minutes, with minimal overhead.

Large-scale reconfiguration campaigns tend to be nerve-racking for network operators as they can lead to significant network downtimes, decreased performance, and policy violations. Unfortunately, existing reconfiguration frameworks often fall short in practice as they either only support a small set of reconfiguration scenarios or simply do not scale. We address these problems with Snowcap, the first network reconfiguration framework which can synthesize configuration updates that comply with arbitrary hard and soft specifications, and involve arbitrary routing protocols. Our key contribution is an efficient search procedure which leverages counter-examples to efficiently navigate the space of configuration updates. Given a reconfiguration ordering which violates the desired specifications, our algorithm automatically identifies the problematic commands so that it can avoid this particular order in the next iteration. We fully implemented Snowcap and extensively evaluated its scalability and effectiveness on real-world topologies and typical, large-scale reconfiguration scenarios. Even for large topologies, Snowcap finds a valid reconfiguration ordering with minimal side-effects (i.e., traffic shifts) within a few seconds at most.

Configuration Synthesis promises to increase automation in network hardware configuration but is generally assumed to constitute a computationally hard problem. We conduct a formal analysis of the computational complexity of network-wide Configuration Synthesis to establish this claim formally. To that end, we consider Configuration Synthesis as a decision problem, whether or not the selected routing protocol(s) can implement a given set of forwarding properties. We find the complexity of Configuration Synthesis heavily depends on the combination of the forwarding properties that need to be implemented in the network, as well as the employed routing protocol(s). Our analysis encompasses different forwarding properties that can be encoded as path constraints, and any combination of distributed destination-based hop-by-hop routing protocols. Many of these combinations yield NP-hard Configuration Synthesis problems; in particular, we show that the satisfiability of a set of arbitrary waypoints for any hop-by-hop routing protocol is NP-complete. Other combinations, however, show potential for efficient, scalable Configuration Synthesis.

In recent years, significant progress has been madetowards scalable network control-plane verification. Yet, opera-tors are still hesitant to deploy such systems. We argue that thisreluctance is in part due to a semantic gap between operatorsreasoning about routing states and verifiers exploring the spaceof environments. Indeed, operators express the specification interms of behavior of routing states, while verifiers usually rely onsolvers to find specific environments that violate the specification.This semantic gap prevents users from guiding these solvers todirectly explore routing states that violate the specification, or tosearch for states that are most relevant or likely. In this paper, we present a new approach for flexible control-plane verification. Instead of relying on rigid off-the-shelf solvers,we design a novel backtracking algorithm to directly explore thespace of routing states. This enables users to guide the explorationaccording to the specification and domain-specific knowledgefrom operators. This algorithm paves the way for novel use cases,ranging from finding relevant (e.g., likely) counterexamples toperforming verification of probabilistic specifications.

To meet ever more stringent requirements, network operators often need to reason about worst-case link loads. Doing so involves analyzing traffic forwarding after failures and BGP route changes. State-of-the-art systems identify failure scenarios causing congestion, but they ignore route changes. We present Viper, the first verification system that efficiently finds maximum link loads under failures and route changes. The key building block of Viper is its ability to massively reduce the gigantic space of possible route changes thanks to (i) a router-based abstraction for route changes, (ii) a theoretical characterization of scenarios leading to worst-case link loads, and (iii) an approximation of input traffic matrices. We fully implement and extensively evaluate Viper. Viper takes only a few minutes to accurately compute all worst-case link loads in large ISP networks. It thus provides operators with critical support to robustify network configurations, improve network management and take business decisions.