Publications by Clément Pit-Claudel

A Conjecture Regarding SMT Instability

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

Lessons learned from the first edition of a large second-year course in software construction

Clément Pit-Claudel

This paper lays out a case study of Software Construction, a new course in the undergraduate computer and communication sciences curriculum at EPFL. We hope to share some generalizable lessons we learned from running its first edition in Fall 2023. The cou ...

EPFL2024

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

A Coq Mechanization of JavaScript Regular Expression Semantics

Clément Pit-Claudel, Aurèle Aimé Aubin Barrière

We present an executable, proven-safe, faithful, and future-proof Coq mechanization of JavaScript regular expression (regex) matching, as specified by the latest published edition of ECMA-262 section 22.2. This is, to our knowledge, the first time that an ...

2024

Linear Matching of JavaScript Regular Expressions

Clément Pit-Claudel, Aurèle Aimé Aubin Barrière

Modern regex languages have strayed far from well-understood traditional regular expressions: They include features that fundamentally transform the matching problem. In exchange for these features, modern regex engines at times suffer from exponential com ...

2024

Gradient: Gradual Compartmentalization via Object Capabilities Tracked in Types

Mathias Josef Payer, Clément Pit-Claudel

Modern software needs fine-grained compartmentalization, i.e., intra-process isolation. A particularly important reason for it are supply-chain attacks, the need for which is aggravated by modern applications depending on hundreds or even thousands of libr ...

ASSOC COMPUTING MACHINERY2024

Foundational Integration Verification of a Cryptographic Server

Clément Pit-Claudel

We present verification of a bare-metal server built using diverse implementation techniques and languages against a whole-system input-output specification in terms of machine code, network packets, and mathematical specifications of elliptic-curve crypto ...

2024

Specification and Verification of Strong Timing Isolation of Hardware Enclaves

Clément Pit-Claudel, Thomas Emile Bourgeat

The process isolation enforceable by commodity hardware and operating systems is too weak to protect secrets from malicious code running on the same machine: attacks exploit timing side channels derived from contention on shared microarchitectural resource ...

Association for Computing Machinery, Inc2024

Diagrammatic notations for interactive theorem proving

Clément Pit-Claudel

Diagrams are ubiquitous in the development and presentation of proofs, yet surprisingly uncommon in computerized mathematics. Instead, authors and developers rely almost exclusively on line-oriented notations (textual abbreviations and symbols). How might ...

EPFL2023