Publications de George Candea | EPFL Graph Search

The Case for Energy Clarity

The rapid expansion of cloud computing, especially machine learning, is leading to a significant increase in the global energy footprint of computing. Improvements in the energy efficiency of hardware and infrastructure are nearing the point of diminishing ...

ACM2025

A Conjecture Regarding SMT Instability

George Candea, Clément Pit-Claudel

Automated verifiers rely on SMT solvers as a backend for proof automation. This simplifies verification in the common case, but also creates usability challenges due to instability. Previous work proposes mitigation strategies motivated by the assumption t ...

Wiley2025

Practical Verification of System-Software Components Written in Standard C

George Candea, Clément Pit-Claudel

Systems code is challenging to verify, because it uses constructs (like raw pointers, pointer arithmetic, and bit twiddling) that are hard for tools to reason about. Existing approaches either sacrifice programmer friendliness, by demanding significant man ...

Association for Computing Machinery, Inc2024

Automatically Reasoning About How Systems Code Uses the CPU Cache

George Candea, Rishabh Ramesh Iyer, Aikaterini Argyraki

We present a technique, called CFAR, that developers can use to reason precisely about how their code, as well as third-party code, uses the CPU cache. Given a piece of systems code P, CFAR employs program analysis and binary instrumentation to automatical ...

2024

Transparent Multicore Scaling of Single-threaded Network Functions

George Candea, Sanidhya Kashyap

This paper presents NFOS, a programming model, runtime, and profiler for productively developing software network functions (NFs) that scale on multicore machines. Writing shared-state concurrent systems that are both correct and scalable is still a seriou ...

Assoc Computing Machinery2024

The Case for Performance Interfaces for Hardware Accelerators

George Candea, Rishabh Ramesh Iyer, Jiacheng Ma, Aikaterini Argyraki

While systems designers are increasingly turning to hardware accelerators for performance gains, realizing these gains is painstaking and error-prone. It can take several person-months to determine if a given accelerator is a good fit for a given piece of ...

2023

Achieving Microsecond-Scale Tail Latency Efficiently with Approximate Optimal Scheduling

George Candea, Rishabh Ramesh Iyer

Datacenter applications expect microsecond-scale service times and tightly bound tail latency, with future workloads expected to be even more demanding. To address this challenge, state-of-the-art runtimes employ theoretically optimal scheduling policies, ...

Assoc Computing Machinery2023

Performance Interfaces for Network Functions

George Candea, Rishabh Ramesh Iyer, Aikaterini Argyraki

Modern programmers routinely use third-party code, and infrastructure operators deploy software they did not write. This would not be possible without semantic interfaces---documentation, header files, specifications---that succinctly describe what that th ...

USENIX Association2022

Automated Verification of Network Function Binaries

George Candea, Solal Vincenzo Pirelli, Aikaterini Argyraki

Formally verifying the correctness of software network functions (NFs) is necessary for network reliability, yet existing techniques require full source code and mandate the use of specific data structures. We describe an automated technique to verify NF b ...

USENIX Association2022

A Simpler and Faster NIC Driver Model for Network Functions

George Candea, Solal Vincenzo Pirelli

The advent of software network functions calls for stronger correctness guarantees and higher performance at every level of the stack. Current network stacks trade simplicity for performance and flexibility, especially in their driver model. We show that p ...

2021