Clément Pit-Claudel

Chattez avec Graph Search

Posez n’importe quelle question sur les cours, conférences, exercices, recherches, actualités, etc. de l’EPFL ou essayez les exemples de questions ci-dessous.

AVERTISSEMENT : Le chatbot Graph n'est pas programmé pour fournir des réponses explicites ou catégoriques à vos questions. Il transforme plutôt vos questions en demandes API qui sont distribuées aux différents services informatiques officiellement administrés par l'EPFL. Son but est uniquement de collecter et de recommander des références pertinentes à des contenus que vous pouvez explorer pour vous aider à répondre à vos 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

Chattez avec 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