Clément Pit-Claudel

32 papers A* 7A 1B 2Misc 1Journal 16Unranked 4
YearRankTypeTitle / Venue / Authors
2026 J jnl
Formal Verification for JavaScript Regular Expressions: A Proven Mechanized Semantics and Its Applications.
Proc. ACM Program. Lang.
Aurèle Barrière, Victor Deng, Clément Pit-Claudel
2026 J jnl
On the computational complexity of JavaScript regex matching.
CoRR
Victor Deng, Aurèle Barrière, Clément Pit-Claudel
2026 B conf
Precise Reasoning about Container-Internal Pointers with Logical Pinning.
CPP
Yawen Guan, Clément Pit-Claudel
2025 J jnl
Automatic layout of railroad diagrams.
CoRR
Shardul Chiplunkar, Clément Pit-Claudel
2025 J jnl
Fine-Grained Reasoning About Container-Internal Pointers with Logical Pinning.
CoRR
Yawen Guan, Clément Pit-Claudel
2025 J jnl
Formal Verification for JavaScript Regular Expressions: a Proven Semantics and its Applications.
CoRR
Aurèle Barrière, Victor Deng, Clément Pit-Claudel
2025 A* conf
Formally Verified Cloud-Scale Authorization.
ICSE
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, Tae Joon Byun, Joshua M. Cohen, Ruijie Fang, Junyoung Jang, Jakob Rath, Hira Taqdees Syeda, Dominik Wagner, Yongwei Yuan
2025 — conf
Verified and Optimized Implementation of Orthologic Proof Search.
CAV (3)
Simon Guilloud, Clément Pit-Claudel
2025 J jnl
Verified and Optimized Implementation of Orthologic Proof Search.
CoRR
Simon Guilloud, Clément Pit-Claudel
2024 J jnl
A Coq Mechanization of JavaScript Regular Expression Semantics.
CoRR
Noé De Santo, Aurèle Barrière, Clément Pit-Claudel
2024 J jnl
A Coq Mechanization of JavaScript Regular Expression Semantics.
Proc. ACM Program. Lang.
Noé De Santo, Aurèle Barrière, Clément Pit-Claudel
2024 J jnl
Foundational Integration Verification of a Cryptographic Server.
Proc. ACM Program. Lang.
Andres Erbsen, Jade Philipoom, Dustin Jamner, Ashley Lin, Samuel Gruetter, Clément Pit-Claudel, Adam Chlipala
2024 J jnl
Gradient: Gradual Compartmentalization via Object Capabilities Tracked in Types.
Proc. ACM Program. Lang.
Aleksander Boruch-Gruszecki, Adrien Ghosn, Mathias Payer, Clément Pit-Claudel
2024 J jnl
Incremental Proof Development in Dafny with Module-Based Induction.
CoRR
Son Ho, Clément Pit-Claudel
2024 J jnl
Linear Matching of JavaScript Regular Expressions.
Proc. ACM Program. Lang.
Aurèle Barrière, Clément Pit-Claudel
2024 A* conf
Practical Verification of System-Software Components Written in Standard C.
SOSP
Can Cebeci, Yong-Hao Zou, Diyu Zhou, George Candea, Clément Pit-Claudel
2024 A* conf
Specification and Verification of Strong Timing Isolation of Hardware Enclaves.
CCS
Stella Lau, Thomas Bourgeat, Clément Pit-Claudel, Adam Chlipala
2023 J jnl
Linear Matching of JavaScript Regular Expressions.
CoRR
Aurèle Barrière, Clément Pit-Claudel
2022 A* conf
Relational compilation for performance-critical applications: extensible proof-producing translation of functional models into low-level code.
PLDI
Clément Pit-Claudel, Jade Philipoom, Dustin Jamner, Andres Erbsen, Adam Chlipala
2022 — —
Relational compilation: Functional-to-imperative code generation for performance-critical applications.
Clément Pit-Claudel
2021 A* conf
Effective simulation and debugging for a high-level hardware language using software compilers.
ASPLOS
Clément Pit-Claudel, Thomas Bourgeat, Stella Lau, Arvind, Adam Chlipala
2020 — conf
Extensible Extraction of Efficient Imperative Programs with Foreign Functions, Manually Managed Memory, and Proofs.
IJCAR (2)
Clément Pit-Claudel, Peng Wang, Benjamin Delaware, Jason Gross, Adam Chlipala
2020 A* conf
The essence of Bluespec: a core language for rule-based hardware design.
PLDI
Thomas Bourgeat, Clément Pit-Claudel, Adam Chlipala, Arvind
2020 B conf
Untangling mechanized proofs.
SLE
Clément Pit-Claudel
2019 A conf
Meta-F ^\star : Proof Automation with SMT, Tactics, and Metaprograms.
ESOP
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
2019 J jnl
Narcissus: correct-by-construction derivation of decoders and encoders from binary formats.
Proc. ACM Program. Lang.
Benjamin Delaware, Sorawit Suriyakarn, Clément Pit-Claudel, Qianchuan Ye, Adam Chlipala
2018 Misc conf
Correct-by-Construction Implementation of Runtime Monitors Using Stepwise Refinement.
SETTA
Teng Zhang, John Wiegley, Theophilos Giannakopoulos, Gregory Eakman, Clément Pit-Claudel, Insup Lee, Oleg Sokolsky
2018 J jnl
Meta-F*: Metaprogramming and Tactics in an Effectful Program Verifier.
CoRR
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
2018 J jnl
Narcissus: Deriving Correct-By-Construction Decoders and Encoders from Binary Formats.
CoRR
Sorawit Suriyakarn, Clément Pit-Claudel, Benjamin Delaware, Adam Chlipala
2017 — conf
The End of History? Using a Proof Assistant to Replace Language Design with Library Design.
SNAPL
Adam Chlipala, Benjamin Delaware, Samuel Duchovni, Jason Gross, Clément Pit-Claudel, Sorawit Suriyakarn, Peng Wang, Katherine Ye
2016 — conf
Trigger Selection Strategies to Stabilize Program Verifiers.
CAV (1)
K. Rustan M. Leino, Clément Pit-Claudel
2015 A* conf
Fiat: Deductive Synthesis of Abstract Data Types in a Proof Assistant.
POPL
Benjamin Delaware, Clément Pit-Claudel, Jason Gross, Adam Chlipala