Silent CUDA Kernel Failures: Why My Error Checking Mechanism Failed Me

Recently, I hit a really frustrating bug: a specific issue that only appeared in Release Mode but vanished in Debug Mode (or any mode with debugging symbols). The program wasn’t crashing loudly, but the kernel outputs were consistently 0. Even worse, my error checking mechanism was completely silent. To catch CUDA kernel launch failures, you typically just need to call cudaGetLastError(); it returns an error code if the launch had an issue. In our case, it returned cudaSuccess. ...

January 28, 2026 · 2 min · Côme Eyraud

Introduction a la validation formelle avec TLA+ et Pluscal

Valider formellement un algorithme permet, de s’assurer que le design ne contient pas de faute de logique. Pour de petits algorithmes, il est plutôt simple d’avoir en tête la liste de tous les états possibles du systèmes. Mais lorsque l’on prend en compte de la concurrence ainsi que du non-déterminisme rajouté par le réseau, ce n’est pas possible d’avoir en tête l’entièreté des états possibles du système. La Vérification Formelle est le fait de prouver l’exactitude d’un système par rapport à une spécification formelle et des propriétés, utilisant des méthodes formelles mathématiques. Il existe différents types de vérification formelle, certaines permettent de vérifier des algorithmes, d’autres des implémentations. ...

January 15, 2025 · 7 min · Côme Eyraud

Introduction to formal validation with TLA+ and Pluscal

Formally validating an algorithm ensures that the design does not contain any logical errors. For small algorithms, it is fairly simple to keep track of all possible states of the system. However, when concurrency and non-determinism added by the network are taken into account, it is not possible to keep track of all possible states of the system. Formal verification is the process of proving the correctness of a system against a formal specification and properties, using formal mathematical methods. There are different types of formal verification, some of which can be used to verify algorithms, others to verify implementations. ...

January 15, 2025 · 7 min · Côme Eyraud

Introduction à RDF et au Web Sémantique

RDF Le Ressource Description Framework (RDF) est un standard du W3C1 pour représenter de la connaissance sous forme de graphe. Multigraphe signifie qu’il peut comporter des boucles et des arêtes multiples. Orienté signifie que les signifie que les arêtes ont un sens. Étiqueté signifie que les arêtes ainsi que les sommets portent une étiquette Un Multigraphe orienté étiqueté Triple RDF Les graphes RDF sont représentés avec des triples RDF au format Sujet - Prédicat - Objet, ou plutôt « S ; P ; O » (sujet pour le nœud de départ, prédicat pour l’arête et objet pour le nœud de destination). ...

January 7, 2025 · 4 min · Côme Eyraud

Introduction to RDF and the Semantic Web

RDF The Resource Description Framework (RDF) is a W3C1 standard for representing knowledge in graph form. Multigraph means that it can contain loops and multiple edges. Directed means that the edges have a direction. Labeled means that both the edges and the vertices have a label. A labeled directed multigraph RDF triples RDF graphs are represented with RDF triples in the format Subject - Predicate - Object, or rather « S ; P ; O » (subject for the starting node, predicate for the edge, and object for the destination node). ...

January 7, 2025 · 4 min · Côme Eyraud

My time in the IUT

After finishing highschool, i know i wanted to work in computer science and systems, but was not really sure of what specific part i wanted to play in them. To this end, i started in 2019 a DUT program (Diplome Universitaire Technologique) at the IUT (Institut Universitaire Technologique) Velizy Villacoublay, a two year formation with a major in Networks and Telecommunications. This program was a mix between scientific and technical courses, aimed at understanding the basis for computer science, the internet and mobile telecommunications, while providing the mathematical and physical tools needed. I had a great experience in this formation, the teachers passion about their topics enabled my curiosity, specifically in math and low level computer science. During my degree, i was fascinated about network protocols and how the internet was designed and scaled. ...

September 10, 2021 · 2 min · Côme Eyraud

My time in Brainsonic

Brainsonic was my second internship, and was my final internship for my IUT. I was the system administrator and basically the IT guy for a company of around a hundred people. Just a couple of month before my arrival, the head of IT left, and they didn’t found a replacement. During my time at Brainsonic, I worked on refreshing the IT department, by doing a hardware inventory, reparing laptops and servers. But else than my typical Technician role, i worked on a database backup system. ...

September 2, 2021 · 2 min · Côme Eyraud

My time in Axibio

During my IUT, i worked multiple times with Axibio. First with a month long internship and then working freelance for them. During my time with them, i developped a simple biowaste pallet tracker system and a simple filesharing website. Before my system, Biowaste pallets in this specific group of cities in France were tracked with color stickers. Drivers would put the specific color stickers on pallets before loading them to their truck. ...

August 16, 2020 · 2 min · Côme Eyraud