Clément Pit-Claudel

According to our database, Clément Pit-Claudel authored at least 21 papers between 2015 and 2024.

Collaborative distances:

• Dijkstra number of four.
• Erdős number of four.

2024

A Coq Mechanization of JavaScript Regular Expression Semantics.

Noé De Santo, Aurèle Barrière, Clément Pit-Claudel

Proc. ACM Program. Lang., 2024

Foundational Integration Verification of a Cryptographic Server.

Andres Erbsen, Jade Philipoom, Dustin Jamner, Ashley Lin, Samuel Gruetter, Clément Pit-Claudel, Adam Chlipala

Proc. ACM Program. Lang., 2024

Gradient: Gradual Compartmentalization via Object Capabilities Tracked in Types.

Aleksander Boruch-Gruszecki, Adrien Ghosn, Mathias Payer, Clément Pit-Claudel

Proc. ACM Program. Lang., 2024

Linear Matching of JavaScript Regular Expressions.

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

Proc. ACM Program. Lang., 2024

Incremental Proof Development in Dafny with Module-Based Induction.

Son Ho, Clément Pit-Claudel

CoRR, 2024

Practical Verification of System-Software Components Written in Standard C.

Can Cebeci, Yonghao Zou, Diyu Zhou, George Candea, Clément Pit-Claudel

Proceedings of the ACM SIGOPS 30th Symposium on Operating Systems Principles, 2024

Specification and Verification of Strong Timing Isolation of Hardware Enclaves.

Stella Lau, Thomas Bourgeat, Clément Pit-Claudel, Adam Chlipala

Proceedings of the 2024 on ACM SIGSAC Conference on Computer and Communications Security, 2024

2022

Relational compilation: Functional-to-imperative code generation for performance-critical applications.

Clément Pit-Claudel

PhD thesis, 2022

Relational compilation for performance-critical applications: extensible proof-producing translation of functional models into low-level code.

Clément Pit-Claudel, Jade Philipoom, Dustin Jamner, Andres Erbsen, Adam Chlipala

Proceedings of the PLDI '22: 43rd ACM SIGPLAN International Conference on Programming Language Design and Implementation, San Diego, CA, USA, June 13, 2022

2021

Effective simulation and debugging for a high-level hardware language using software compilers.

Clément Pit-Claudel, Thomas Bourgeat, Stella Lau, Arvind, Adam Chlipala

Proceedings of the ASPLOS '21: 26th ACM International Conference on Architectural Support for Programming Languages and Operating Systems, 2021

2020

Untangling mechanized proofs.

Clément Pit-Claudel

Proceedings of the 13th ACM SIGPLAN International Conference on Software Language Engineering, 2020

The essence of Bluespec: a core language for rule-based hardware design.

Thomas Bourgeat, Clément Pit-Claudel, Adam Chlipala, Arvind

Proceedings of the 41st ACM SIGPLAN International Conference on Programming Language Design and Implementation, 2020

Extensible Extraction of Efficient Imperative Programs with Foreign Functions, Manually Managed Memory, and Proofs.

Clément Pit-Claudel, Peng Wang, Benjamin Delaware, Jason Gross, Adam Chlipala

Proceedings of the Automated Reasoning - 10th International Joint Conference, 2020

2019

Narcissus: correct-by-construction derivation of decoders and encoders from binary formats.

Benjamin Delaware, Sorawit Suriyakarn, Clément Pit-Claudel, Qianchuan Ye, Adam Chlipala

Proc. ACM Program. Lang., 2019

Meta-F ^\star : Proof Automation with SMT, Tactics, and Metaprograms.

Guido Martínez, Danel Ahman, Victor Dumitrescu, Nick Giannarakis, Chris Hawblitzel, Catalin Hritcu, Monal Narasimhamurthy, Zoe Paraskevopoulou, Clément Pit-Claudel, Jonathan Protzenko, Tahina Ramananandro, Aseem Rastogi, Nikhil Swamy

Proceedings of the Programming Languages and Systems, 2019

2018

Meta-F*: Metaprogramming and Tactics in an Effectful Program Verifier.

Guido Martínez, Danel Ahman, Victor Dumitrescu, Nick Giannarakis, Chris Hawblitzel, Catalin Hritcu, Monal Narasimhamurthy, Zoe Paraskevopoulou, Clément Pit-Claudel, Jonathan Protzenko, Tahina Ramananandro, Aseem Rastogi, Nikhil Swamy

CoRR, 2018

Narcissus: Deriving Correct-By-Construction Decoders and Encoders from Binary Formats.

Sorawit Suriyakarn, Clément Pit-Claudel, Benjamin Delaware, Adam Chlipala

CoRR, 2018

Correct-by-Construction Implementation of Runtime Monitors Using Stepwise Refinement.

Teng Zhang, John Wiegley, Theophilos Giannakopoulos, Gregory Eakman, Clément Pit-Claudel, Insup Lee, Oleg Sokolsky

Proceedings of the Dependable Software Engineering. Theories, Tools, and Applications, 2018

2017

The End of History? Using a Proof Assistant to Replace Language Design with Library Design.

Adam Chlipala, Benjamin Delaware, Samuel Duchovni, Jason Gross, Clément Pit-Claudel, Sorawit Suriyakarn, Peng Wang, Katherine Ye

Proceedings of the 2nd Summit on Advances in Programming Languages, 2017

2016

Trigger Selection Strategies to Stabilize Program Verifiers.

K. Rustan M. Leino, Clément Pit-Claudel

Proceedings of the Computer Aided Verification - 28th International Conference, 2016

2015

Fiat: Deductive Synthesis of Abstract Data Types in a Proof Assistant.

Benjamin Delaware, Clément Pit-Claudel, Jason Gross, Adam Chlipala

Proceedings of the 42nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 2015