Clément Pit-Claudel

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

Collaborative distances:

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

2026

Source-to-Source Transformations for GPU Code Generation.

Julien de Castelnau, Thomas Koehler, Arthur Charguéraud, Clément Pit-Claudel

CoRR, May, 2026

Tracers for debugging and program exploration.

Shardul Chiplunkar, Clément Pit-Claudel

CoRR, April, 2026

On the computational complexity of JavaScript regex matching.

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

CoRR, March, 2026

Formal Verification for JavaScript Regular Expressions: A Proven Mechanized Semantics and Its Applications.

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

Proc. ACM Program. Lang., 2026

Precise Reasoning about Container-Internal Pointers with Logical Pinning.

Yawen Guan, Clément Pit-Claudel

Proceedings of the 15th ACM SIGPLAN International Conference on Certified Programs and Proofs, 2026

2025

Fine-Grained Reasoning About Container-Internal Pointers with Logical Pinning.

Yawen Guan, Clément Pit-Claudel

CoRR, September, 2025

Automatic layout of railroad diagrams.

Shardul Chiplunkar, Clément Pit-Claudel

CoRR, September, 2025

Formal Verification for JavaScript Regular Expressions: a Proven Semantics and its Applications.

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

CoRR, July, 2025

A Conjecture Regarding SMT Instability.

Can Cebeci, Nikolaj Bjørner, George Candea, Clément Pit-Claudel

Proceedings of the Joint Proceedings of the 23rd International Workshop on Satisfiability Modulo Theories and the 16th Pragmatics of SAT International Workshop co-located with the 31st International Conference on Principles and Practice of Constraint Programming, 2025

Formally Verified Cloud-Scale Authorization.

Aleks Chakarov, Jaco Geldenhuys, Matthew Heck, Michael Hicks, Sam Huang, Georges-Axel Jaloyan, Anjali Joshi, K. Rustan M. Leino, Mikael Mayer, Sean McLaughlin, Akhilesh Mritunjai, Clément Pit-Claudel, Sorawee Porncharoenwase, Florian Rabe, Marianna Rapoport, Giles Reger, Cody Roux, Neha Rungta, Robin Salkeld, Matthias Schlaipfer, Daniel Schoepe, Johanna Schwartzentruber, Serdar Tasiran, Aaron Tomb, Emina Torlak, Jean-Baptiste Tristan, Lucas G. Wagner, Michael W. Whalen, Remy Willems, Tongtong Xiang, Taejoon Byun, Joshua M. Cohen, Ruijie Fang, Junyoung Jang, Jakob Rath, Hira Taqdees Syeda, Dominik Wagner, Yongwei Yuan

Proceedings of the 47th IEEE/ACM International Conference on Software Engineering, 2025

Verified and Optimized Implementation of Orthologic Proof Search.

Simon Guilloud, Clément Pit-Claudel

Proceedings of the Computer Aided Verification - 37th International Conference, 2025

2024

Gradient: benchmark code.

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

Dataset, August, 2024

Gradient: migrated scala-xml.

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

Dataset, August, 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