Clément Pit-Claudel

Publication Activity (10 Years)

Years Active: 2015-2024
Publications (10 Years): 18

Top Topics

Abstract Data Types

Theorem Proving

Regular Expressions

Deterministic Finite Automata

Top Venues

Proc. ACM Program. Lang.

Publications

Aurèle Barrière, Clément Pit-Claudel
Linear Matching of JavaScript Regular Expressions. Proc. ACM Program. Lang. 8 (PLDI) (2024)
Son Ho, Clément Pit-Claudel
Incremental Proof Development in Dafny with Module-Based Induction. CoRR (2024)
Andres Erbsen, Jade Philipoom, Dustin Jamner, Ashley Lin, Samuel Gruetter, Clément Pit-Claudel, Adam Chlipala
Foundational Integration Verification of a Cryptographic Server. Proc. ACM Program. Lang. 8 (PLDI) (2024)
Noé De Santo, Aurèle Barrière, Clément Pit-Claudel
A Coq Mechanization of JavaScript Regular Expression Semantics. CoRR (2024)
Aurèle Barrière, Clément Pit-Claudel
Linear Matching of JavaScript Regular Expressions. CoRR (2023)
Clément Pit-Claudel, Jade Philipoom, Dustin Jamner, Andres Erbsen, Adam Chlipala
Relational compilation for performance-critical applications: extensible proof-producing translation of functional models into low-level code. PLDI (2022)
Clément Pit-Claudel, Thomas Bourgeat, Stella Lau, Arvind, Adam Chlipala
Effective simulation and debugging for a high-level hardware language using software compilers. ASPLOS (2021)
Clément Pit-Claudel, Peng Wang, Benjamin Delaware, Jason Gross, Adam Chlipala
Extensible Extraction of Efficient Imperative Programs with Foreign Functions, Manually Managed Memory, and Proofs. IJCAR (2) (2020)
Thomas Bourgeat, Clément Pit-Claudel, Adam Chlipala, Arvind
The essence of Bluespec: a core language for rule-based hardware design. PLDI (2020)
Clément Pit-Claudel
Untangling mechanized proofs. SLE (2020)
Benjamin Delaware, Sorawit Suriyakarn, Clément Pit-Claudel, Qianchuan Ye, Adam Chlipala
Narcissus: correct-by-construction derivation of decoders and encoders from binary formats. Proc. ACM Program. Lang. 3 (ICFP) (2019)
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
Meta-F ^\star : Proof Automation with SMT, Tactics, and Metaprograms. ESOP (2019)
Teng Zhang, John Wiegley, Theophilos Giannakopoulos, Gregory Eakman, Clément Pit-Claudel, Insup Lee, Oleg Sokolsky
Correct-by-Construction Implementation of Runtime Monitors Using Stepwise Refinement. SETTA (2018)
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
Meta-F*: Metaprogramming and Tactics in an Effectful Program Verifier. CoRR (2018)
Sorawit Suriyakarn, Clément Pit-Claudel, Benjamin Delaware, Adam Chlipala
Narcissus: Deriving Correct-By-Construction Decoders and Encoders from Binary Formats. CoRR (2018)
Adam Chlipala, Benjamin Delaware, Samuel Duchovni, Jason Gross, Clément Pit-Claudel, Sorawit Suriyakarn, Peng Wang, Katherine Ye
The End of History? Using a Proof Assistant to Replace Language Design with Library Design. SNAPL (2017)
K. Rustan M. Leino, Clément Pit-Claudel
Trigger Selection Strategies to Stabilize Program Verifiers. CAV (1) (2016)
Benjamin Delaware, Clément Pit-Claudel, Jason Gross, Adam Chlipala
Fiat: Deductive Synthesis of Abstract Data Types in a Proof Assistant. POPL (2015)