Publications related to Practical Verification of System-Software Components Written in Standard C

Related publications (21)

Single-pass Detection of Jailbreaking Input in Large Language Models

Volkan Cevher, Grigorios Chrysos, Yongtao Wu, Elias Abad Rocamora

Defending aligned Large Language Models (LLMs) against jailbreaking attacks is a challenging problem, with existing approaches requiring multiple requests or even queries to auxiliary LLMs, making them computationally heavy. Instead, we focus on detecting ...

2025

Towards URLLC with Open-Source 5G Software

Haitham Al Hassanieh, Aoyu Gong, Dan Mihai Dumitriu, Arman Maghsoudnia, Raphael Cannatà

Ultra-Reliable Low-Latency Communication is a key feature of 5G, yet achieving its strict one-way latency target remains challenging in real-world deployments. While previous work proposes latency reduction techniques, most are theoretical or simulation-ba ...

Association for Computing Machinery2025

Automated Induction for Proving Program Equivalence

Dragana Milovancevic

Formal verification has made great advances in recent decades, resulting in tools that can verify strong correctness properties of important pieces of software infrastructure. In this thesis, we study a particular instance of formal verification: equivalen ...

EPFL2025

OpenMM–MiMiC Interface for Efficient and Flexible Multiscale Simulations

Ursula Röthlisberger, Andrea Levy, Andrej Antalik

MiMiC is a flexible and efficient framework for multiscale simulations in which different subsystems are treated by individual client programs. In this work, we present a new interface with OpenMM to be used as an MM client program and we demonstrate its e ...

American Chemical Society (ACS)2025

Course Recommender Systems Need to Consider the Job Market

Anna Dai, Tanja Christina Käser Jacober, Antoine Bosselut, Jibril Albachir Frej, Syrielle Mathilde Marie Montariol

Current course recommender systems primarily leverage learner-course interactions, course content, learner preferences, and supplementary course details like instructor, institution, ratings, and reviews, to make their recommendation. However, these system ...

Association for Computing Machinery, Inc2024

The Side-channel Metrics Cheat Sheet

Francesco Regazzoni, Mirjana Stojilovic, Ognjen Glamocanin

Side-channel attacks exploit a physical observable originating from a cryptographic device in order to extract its secrets. Many practically relevant advances in the field of side-channel analysis relate to security evaluations of cryptographic functions a ...

2023

Seismo-VLAB: An Open-Source Software for Soil-Structure Interaction Analyses

Antonio Joaquin Garcia Suarez

In the fields of structural and geotechnical engineering, improving the understanding of soil-structure interaction (SSI) effects is critical for earthquake-resistant design. Engineers and practitioners often resort to finite element (FE) software to advan ...

2023

Using machine learning to generate an open-access cropland map from satellite images time series in the Indian Himalayan region

Danya Li

Crop maps are crucial for agricultural monitoring and food management and can additionally support domain-specific applications, such as setting cold supply chain infrastructure in developing countries. Machine learning (ML) models, combined with freely-av ...

Elsevier2023

Visual Scene Understanding for Transportation: From Detecting Objects To Relationships

George Adaimi

Transportation, which deals with moving people and goods around, has a clear impact on the economic development of our society and our well-being. Traditionally, transportation was studied and analyzed using expensive sensors, such as induction loops, that ...

EPFL2022

Benchmark for Human-to-Robot Handovers of Unseen Containers with Unknown Filling

Pascal Frossard, Aude Billard, Andrea Cavallaro, Apostolos Modas, Nuno Ricardo Ferreira Duarte, Konstantinos Chatzilygeroudis

The real-time estimation through vision of the physical properties of objects manipulated by humans is important to inform the control of robots for performing accurate and safe grasps of objects handed over by humans. However, estimating the 3D pose and d ...

2020

A low-cost, autonomous mobile platform for limnological investigations, supported by high-resolution mesoscale airborne imagery

David Andrew Barry, Ulrich Lemmin, Anton Ivanov, Htet Kyi Wynn, Stepan Tulyakov, Abolfazl Irani Rahaghi, Ludovic Zulliger, Jean-Luc Liardon, Philippe Olivier Paccaud, Beat Marcel Geissmann

Two complementary measurement systems – built upon an autonomous floating craft and a tethered balloon – for lake research and monitoring are presented. The autonomous vehicle was assembled on a catamaran for stability, and is capable of handling a variety ...

2019

Object-Oriented Recovery for Non-volatile Memory

James Richard Larus, Nachshon Cohen, David Teksen Aksun

New non-volatile memory (NVM) technologies enable direct, durable storage of data in an application's heap. Durable, randomly accessible memory facilitates the construction of applications that do not lose data at system shutdown or power failure. Existing ...

ACM2018

Cross-Platform Language Design

Sébastien Jean Robert Doeraene

Programming languages are increasingly compiled to multiple runtimes, each featuring their own rich structures such as their object model. Furthermore, they need to interact with other languages targeting said runtimes. A language targeting only one runtim ...

EPFL2018

LMS-Verify: Abstraction without Regret for Verified Systems Programming’

Tiark Rompf, Nada Amin

Performance critical software is almost always developed in C, as programmers do not trust high-level languages to deliver the same reliable performance. This is bad because low-level code in unsafe languages attracts security vulnerabilities and because d ...

Assoc Computing Machinery2017

Late Data Layout: Unifying Data Representation Transformations

Martin Odersky, Eugene Burmako, Vlad Ureche

Values need to be represented differently when interacting with certain language features. For example, an integer has to take an object-based representation when interacting with erased generics, although, for performance reasons, the stack-based value re ...

ACM2014

Self-Assembly: Lightweight Language Extension and Datatype Generic Programming, All-in-One!

Philipp Haller, Heather Christine Klug

In this paper we show a general mechanism, called self-assembly, for lightweight language extensions (LLEs). LLEs allow users to define generic operations or properties that operate over a large class of types. With LLEs it is possible, for example, for us ...

2014

Inferring Scalability from Program Pseudocode

Mihai Letia

Recent trends have led hardware manufacturers to place multiple processing cores on a single chip, making parallel programming the intended way of taking advantage of the increased processing power. However, bringing concurrency to average programmers is c ...

EPFL2014

Lightweight Modular Staging and Embedded Compilers : Abstraction without Regret for High-Level High-Performance Programming

Tiark Rompf

Programs expressed in a high-level programming language need to be translated to a low-level machine dialect for execution. This translation is usually accomplished by a compiler, which is able to translate any legal program to equivalent low-level code. B ...

EPFL2012

On the Performance of Software Transactional Memory

Aleksandar Dragojevic

The recent proliferation of multi-core processors has moved concurrent programming into mainstream by forcing increasingly more programmers to write parallel code. Using traditional concurrency techniques, such as locking, is notoriously difficult and has ...

EPFL2012

Deadlock detection for synchronous Java

Duy Vo Duc

The aim of this thesis is to construct toolsets that support the Synchronous Java programming language, an extension to the Java language that introduces a new method of synchronization between threads. The contributions of this thesis include a State Spac ...

EPFL2007