| Certified programming with dependent types: a pragmatic introduction to the Coq proof assistant A Chlipala MIT Press, 2013 | 537* | 2013 |
| Using Crash Hoare logic for certifying the FSCQ file system H Chen, D Ziegler, T Chajed, A Chlipala, MF Kaashoek, N Zeldovich Proceedings of the 25th Symposium on Operating Systems Principles, 18-37, 2015 | 336 | 2015 |
| Generating tests from counterexamples D Beyer, AJ Chlipala, TA Henzinger, R Jhala, R Majumdar Proceedings. 26th International Conference on Software Engineering, 326-335, 2004 | 333 | 2004 |
| Parametric higher-order abstract syntax for mechanized semantics A Chlipala Proceedings of the 13th ACM SIGPLAN international conference on Functional …, 2008 | 272 | 2008 |
| Mostly-automated verification of low-level programs in computational separation logic A Chlipala Proceedings of the 32nd ACM SIGPLAN conference on Programming language …, 2011 | 225 | 2011 |
| Simple high-level code for cryptographic arithmetic: With proofs, without compromises A Erbsen, J Philipoom, J Gross, R Sloan, A Chlipala ACM SIGOPS Operating Systems Review 54 (1), 23-30, 2020 | 163 | 2020 |
| A verified compiler for an impure functional language A Chlipala ACM Sigplan Notices 45 (1), 93-106, 2010 | 159 | 2010 |
| Kami: a platform for high-level parametric hardware specification and its modular verification J Choi, M Vijayaraghavan, B Sherman, A Chlipala, Arvind Proceedings of the ACM on Programming Languages 1 (ICFP), 1-30, 2017 | 146 | 2017 |
| A certified type-preserving compiler from lambda calculus to assembly language A Chlipala ACM Sigplan Notices 42 (6), 54-65, 2007 | 139 | 2007 |
| The Bedrock structured programming system: Combining generative metaprogramming and Hoare logic in an extensible program verifier A Chlipala Proceedings of the 18th ACM SIGPLAN international conference on Functional …, 2013 | 136 | 2013 |
| Fiat: Deductive synthesis of abstract data types in a proof assistant B Delaware, C Pit-Claudel, J Gross, A Chlipala Acm Sigplan Notices 50 (1), 689-700, 2015 | 132 | 2015 |
| Static Checking of {Dynamically-Varying} Security Policies in {Database-Backed} Applications A Chlipala 9th USENIX Symposium on Operating Systems Design and Implementation (OSDI 10), 2010 | 132 | 2010 |
| Effective interactive proofs for higher-order imperative programs A Chlipala, G Malecha, G Morrisett, A Shinnar, R Wisnesky ACM Sigplan Notices 44 (9), 79-90, 2009 | 127 | 2009 |
| Ur: statically-typed metaprogramming with type-level record computation A Chlipala ACM Sigplan Notices 45 (6), 122-133, 2010 | 122 | 2010 |
| Chapar: certified causally consistent distributed key-value stores M Lesani, CJ Bell, A Chlipala ACM SIGPLAN Notices 51 (1), 357-370, 2016 | 112 | 2016 |
| Ur/Web: A simple model for programming the web A Chlipala Proceedings of the 42nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of …, 2015 | 110 | 2015 |
| Invited talk: the blast query language for software verification D Beyer, AJ Chlipala, TA Henzinger, R Jhala, R Majumdar Proceedings of the 2004 ACM SIGPLAN symposium on Partial evaluation and …, 2004 | 109 | 2004 |
| The essence of Bluespec: a core language for rule-based hardware design T Bourgeat, C Pit-Claudel, A Chlipala, Arvind Proceedings of the 41st ACM SIGPLAN Conference on Programming Language …, 2020 | 98 | 2020 |
| Jitk: A Trustworthy {In-Kernel} Interpreter Infrastructure X Wang, D Lazar, N Zeldovich, A Chlipala, Z Tatlock 11th USENIX Symposium on Operating Systems Design and Implementation (OSDI …, 2014 | 92 | 2014 |
| Verifying a high-performance crash-safe file system using a tree specification H Chen, T Chajed, A Konradi, S Wang, A İleri, A Chlipala, MF Kaashoek, ... Proceedings of the 26th Symposium on Operating Systems Principles, 270-286, 2017 | 88 | 2017 |
