Clément Pit-Claudel

Chat with Graph Search

Ask any question about EPFL courses, lectures, exercises, research, news, etc. or try the example questions below.

DISCLAIMER: The Graph Chatbot is not programmed to provide explicit or categorical answers to your questions. Rather, it transforms your questions into API requests that are distributed across the various IT services officially administered by EPFL. Its purpose is solely to collect and recommend relevant references to content that you can explore to help you answer your questions.

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 ...

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 ...

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 ...

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 ...

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 ...

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 ...

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 ...

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 ...

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 ...

Clément Pit-Claudel

Chat with Graph Search

Foundational Integration Verification of a Cryptographic Server

Specification and Verification of Strong Timing Isolation of Hardware Enclaves

Gradient: Gradual Compartmentalization via Object Capabilities Tracked in Types

A Conjecture Regarding SMT Instability

Linear Matching of JavaScript Regular Expressions

Practical Verification of System-Software Components Written in Standard C

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

A Coq Mechanization of JavaScript Regular Expression Semantics

Diagrammatic notations for interactive theorem proving