| Program logics for certified compilers AW Appel, R Dockins, L Beringer, A Hobor, J Dodds, S Blazy, X Leroy, ... Cambridge University Press, 2014 | 246 | 2014 |
| Verified Correctness and Security of OpenSSL {HMAC} L Beringer, A Petcher, QY Katherine, AW Appel 24th {USENIX} Security Symposium ({USENIX} Security 15), 207-221, 2015 | 147 | 2015 |
| Compositional compcert G Stewart, L Beringer, S Cuellar, AW Appel ACM SIGPLAN Notices 50 (1), 275-287, 2015 | 125 | 2015 |
| VST-Floyd: A separation logic tool to verify correctness of C programs Q Cao, L Beringer, S Gruetter, J Dodds, AW Appel Journal of Automated Reasoning 61 (1), 367-422, 2018 | 92 | 2018 |
| A program logic for resources D Aspinall, L Beringer, M Hofmann, HW Loidl, A Momigliano Theoretical Computer Science 389 (3), 411-445, 2007 | 83 | 2007 |
| Verified correctness and security of mbedTLS HMAC-DRBG KQ Ye, M Green, N Sanguansin, L Beringer, A Petcher, AW Appel Proceedings of the 2017 ACM SIGSAC Conference on Computer and Communications …, 2017 | 72 | 2017 |
| Secure information flow and program logics L Beringer, M Hofmann 20th IEEE Computer Security Foundations Symposium (CSF'07), 233-248, 2007 | 62 | 2007 |
| Automatic certification of heap consumption L Beringer, M Hofmann, A Momigliano, O Shkaravska International Conference on Logic for Programming Artificial Intelligence …, 2005 | 60 | 2005 |
| Position paper: the science of deep specification AW Appel, L Beringer, A Chlipala, BC Pierce, Z Shao, S Weirich, ... Philosophical Transactions of the Royal Society A: Mathematical, Physical …, 2017 | 59 | 2017 |
| Verified compilation for shared-memory C L Beringer, G Stewart, R Dockins, AW Appel European Symposium on Programming Languages and Systems, 107-127, 2014 | 59 | 2014 |
| From C to interaction trees: specifying, verifying, and testing a networked server N Koh, Y Li, Y Li, L Xia, L Beringer, W Honoré, W Mansky, BC Pierce, ... Proceedings of the 8th ACM SIGPLAN International Conference on Certified …, 2019 | 50 | 2019 |
| Relational semantics for effect-based program transformations with dynamic allocation N Benton, A Kennedy, L Beringer, M Hofmann Proceedings of the 9th ACM SIGPLAN international conference on Principles …, 2007 | 50 | 2007 |
| Reading, writing and relations N Benton, A Kennedy, M Hofmann, L Beringer Asian Symposium on Programming Languages and Systems, 114-130, 2006 | 50 | 2006 |
| A program logic for resource verification D Aspinall, L Beringer, M Hofmann, HW Loidl, A Momigliano International Conference on Theorem Proving in Higher Order Logics, 34-49, 2004 | 47 | 2004 |
| Mobius: Mobility, ubiquity, security G Barthe, L Beringer, P Crégut, B Grégoire, M Hofmann, P Müller, E Poll, ... International Symposium on Trustworthy Global Computing, 10-29, 2006 | 44 | 2006 |
| Grail: a functional form for imperative mobile code L Beringer, K MacKenzie, I Stark Electronic Notes in Theoretical Computer Science 85 (1), 3-23, 2003 | 44 | 2003 |
| Relational semantics for effect-based program transformations: higher-order store N Benton, A Kennedy, L Beringer, M Hofmann Proceedings of the 11th ACM SIGPLAN conference on Principles and practice of …, 2009 | 43 | 2009 |
| Relational decomposition L Beringer International Conference on Interactive Theorem Proving, 39-54, 2011 | 34 | 2011 |
| A certificate infrastructure for machine-checked proofs of conditional information flow T Amtoft, J Dodds, Z Zhang, A Appel, L Beringer, J Hatcliff, X Ou, ... International Conference on Principles of Security and Trust, 369-389, 2012 | 28 | 2012 |
| End-to-end multilevel hybrid information flow control L Beringer Asian Symposium on Programming Languages and Systems, 50-65, 2012 | 26 | 2012 |
Andrew W. AppelProfessor of Computer Science, Princeton UniversityVerified email at princeton.edu
