IC Colloquium: Building systems that we can trust: compilers, semantics, and tooling for end-to-end verified systems
Event details
| Date | 18.03.2021 |
| Hour | 14:00 › 15:00 |
| Location | Online |
| Category | Conferences - Seminars |
By: Clément Pit-Claudel - MIT
IC Faculty candidate
Abstract
Computer systems play a crucial role in our lives yet cannot be fully trusted, in part due to the persistence of software and hardware bugs. Beyond costs and lost revenue, these bugs put our privacy, our well-being, and sometimes even our lives at risk.
Writing systems in high-level programming languages increases developer productivity and eliminates common sources of errors, but compilers for these languages often produce relatively slow code. As a result, critical systems are still typically written in low-level languages — and remain full of bugs.
In this talk, I will discuss my efforts to build fast systems verified from end to end, starting from requirements formulated in high-level mathematical terms and deriving assembly code with uncompromising performance, backed by machine-checked proofs of correctness. The key component of this approach is a new way of phrasing program compilation as an existentially quantified proof-search problem; this enables users to customize their compilers and build systems in expressive languages without paying steep performance penalties.
Then, because pure-software verification cannot protect against hardware bugs, I will describe my recent efforts to characterize the semantics of rule-based hardware-design languages and develop compilers, verification technology, and simulators for hardware systems.
Finally, as part of a vision to make verification and formal methods a standard part of critical software and hardware development, I will describe my efforts to make verification work more approachable, focusing on tools to help developers craft and comprehend mechanized proofs.
Bio
Clément Pit-Claudel is a PhD candidate at MIT working in Adam Chlipala's lab. He received his BS and MSE at École Polytechnique in France and his MS at MIT in 2016. His research focuses on programming languages, extensible compilers, and verification; his broader interests include systems engineering, hardware design languages, security, optimization, databases, and type theory. Clément built the first end-to-end verified compilation pipeline from high-level specifications to assembly language, a fast simulator and the first verified compiler for a rule-based hardware-design language with EHRs, and multiple widely-used tools for the Coq proof assistant. His application materials are at https://pit-claudel.fr/clement/faculty-applications/
More information
IC Faculty candidate
Abstract
Computer systems play a crucial role in our lives yet cannot be fully trusted, in part due to the persistence of software and hardware bugs. Beyond costs and lost revenue, these bugs put our privacy, our well-being, and sometimes even our lives at risk.
Writing systems in high-level programming languages increases developer productivity and eliminates common sources of errors, but compilers for these languages often produce relatively slow code. As a result, critical systems are still typically written in low-level languages — and remain full of bugs.
In this talk, I will discuss my efforts to build fast systems verified from end to end, starting from requirements formulated in high-level mathematical terms and deriving assembly code with uncompromising performance, backed by machine-checked proofs of correctness. The key component of this approach is a new way of phrasing program compilation as an existentially quantified proof-search problem; this enables users to customize their compilers and build systems in expressive languages without paying steep performance penalties.
Then, because pure-software verification cannot protect against hardware bugs, I will describe my recent efforts to characterize the semantics of rule-based hardware-design languages and develop compilers, verification technology, and simulators for hardware systems.
Finally, as part of a vision to make verification and formal methods a standard part of critical software and hardware development, I will describe my efforts to make verification work more approachable, focusing on tools to help developers craft and comprehend mechanized proofs.
Bio
Clément Pit-Claudel is a PhD candidate at MIT working in Adam Chlipala's lab. He received his BS and MSE at École Polytechnique in France and his MS at MIT in 2016. His research focuses on programming languages, extensible compilers, and verification; his broader interests include systems engineering, hardware design languages, security, optimization, databases, and type theory. Clément built the first end-to-end verified compilation pipeline from high-level specifications to assembly language, a fast simulator and the first verified compiler for a rule-based hardware-design language with EHRs, and multiple widely-used tools for the Coq proof assistant. His application materials are at https://pit-claudel.fr/clement/faculty-applications/
More information
Practical information
- General public
- Free
- This event is internal
Contact
- George Candea