Lennart Beringer

ORCID

Publication Activity (10 Years)

Years Active: 2001-2024
Publications (10 Years): 14

Top Venues

University of Edinburgh, UK (PHD)

Education History

University of Edinburgh, UK

PHD

Publications

Duc-Than Nguyen, Lennart Beringer, William Mansky, Shengyi Wang
Compositional Verification of Concurrent C Programs with Search Structure Templates. CPP (2024)
Ramana Nagasamudram, Lennart Beringer, Ken Birman, Mae Milano, David A. Naumann
Verifying a C Implementation of Derecho's Coordination Mechanism Using VST and Coq. NFM (2024)
Roshan Sharma, Shengyi Wang, Alexander Oey, Anastasiia Evdokimova, Lennart Beringer, William Mansky
Proving Logical Atomicity using Lock Invariants. CoRR (2023)
Qinshi Wang, Mengying Pan, Shengyi Wang, Ryan Doenges, Lennart Beringer, Andrew W. Appel
Foundational Verification of Stateful P4 Packet Processing. ITP (2023)
Lennart Beringer
Verified Software Units for Simple DFA Modules and Objects in C. ISoLA (2) (2022)
Lennart Beringer
Verified Software Units. ESOP (2021)
Hengchu Zhang, Wolf Honoré, Nicolas Koh, Yao Li, Yishuai Li, Li-yao Xia, Lennart Beringer, William Mansky, Benjamin C. Pierce, Steve Zdancewic
Verifying an HTTP Key-Value Server with Interaction Trees and VST. ITP (2021)
Lennart Beringer, Andrew W. Appel
Abstraction and subsumption in modular verification of C programs. Formal Methods Syst. Des. 58 (1-2) (2021)
Lennart Beringer, Andrew W. Appel
Abstraction and Subsumption in Modular Verification of C Programs. FM (2019)
Nicolas Koh, Yao Li, Yishuai Li, Li-yao Xia, Lennart Beringer, Wolf Honoré, William Mansky, Benjamin C. Pierce, Steve Zdancewic
From C to interaction trees: specifying, verifying, and testing a networked server. CPP (2019)
Nicolas Koh, Yao Li, Yishuai Li, Li-yao Xia, Lennart Beringer, Wolf Honoré, William Mansky, Benjamin C. Pierce, Steve Zdancewic
From C to Interaction Trees: Specifying, Verifying, and Testing a Networked Server. CoRR (2018)
Qinxiang Cao, Lennart Beringer, Samuel Gruetter, Josiah Dodds, Andrew W. Appel
VST-Floyd: A Separation Logic Tool to Verify Correctness of C Programs. J. Autom. Reason. 61 (1-4) (2018)
Katherine Q. Ye, Matthew Green, Naphat Sanguansin, Lennart Beringer, Adam Petcher, Andrew W. Appel
Verified Correctness and Security of mbedTLS HMAC-DRBG. CoRR (2017)
Katherine Q. Ye, Matthew Green, Naphat Sanguansin, Lennart Beringer, Adam Petcher, Andrew W. Appel
Verified Correctness and Security of mbedTLS HMAC-DRBG. CCS (2017)
Lennart Beringer, Adam Petcher, Katherine Q. Ye, Andrew W. Appel
Verified Correctness and Security of OpenSSL HMAC. USENIX Security Symposium (2015)
Gordon Stewart, Lennart Beringer, Santiago Cuellar, Andrew W. Appel
Compositional CompCert. POPL (2015)
Lennart Beringer, Gordon Stewart, Robert Dockins, Andrew W. Appel
Verified Compilation for Shared-Memory C. ESOP (2014)
Lennart Beringer, Robert Grabowski, Martin Hofmann
Verifying pointer and string analyses with region type systems. Comput. Lang. Syst. Struct. 39 (2) (2013)
Torben Amtoft, Josiah Dodds, Zhi Zhang, Andrew W. Appel, Lennart Beringer, John Hatcliff, Xinming Ou, Andrew Cousino
A Certificate Infrastructure for Machine-Checked Proofs of Conditional Information Flow. POST (2012)
Lennart Beringer
End-to-end Multilevel Hybrid Information Flow Control. APLAS (2012)
Gordon Stewart, Lennart Beringer, Andrew W. Appel
Verified heap theorem prover by paramodulation. ICFP (2012)
Lennart Beringer, Randall Brukardt, Thomas Plum, S. Tucker Taft
Panel on compiler certification: should we trust our compiler? HILT (2012)
Lennart Beringer
Relational Decomposition. ITP (2011)
Lennart Beringer
Relational bytecode correlations. J. Log. Algebraic Methods Program. 79 (7) (2010)
Lennart Beringer, Robert Grabowski, Martin Hofmann
Verifying Pointer and String Analyses with Region Type Systems. LPAR (Dakar) (2010)
Robert Grabowski, Lennart Beringer
Noninterference with Dynamic Security Domains and Policies. ASIAN (2009)
Nick Benton, Andrew Kennedy, Lennart Beringer, Martin Hofmann
Relational semantics for effect-based program transformations: higher-order store. PPDP (2009)
Hans-Wolfgang Loidl, Kenneth MacKenzie, Steffen Jost, Lennart Beringer
A Proof-Carrying-Code Infrastructure for Resources. LADC (2009)
Lennart Beringer, Martin Hofmann
A Bytecode Logic for JML and Types. Arch. Formal Proofs 2008 (2008)
Lennart Beringer, Martin Hofmann
Secure information flow and program logics. Arch. Formal Proofs 2008 (2008)
Lennart Beringer
Functional Elimination of Phi-instructions. Electron. Notes Theor. Comput. Sci. 176 (3) (2007)
Lennart Beringer, Martin Hofmann, Mariela Pavlova
Certification Using the Mobius Base Logic. FMCO (2007)
David Aspinall, Lennart Beringer, Alberto Momigliano
Optimisation Validation. Electron. Notes Theor. Comput. Sci. 176 (3) (2007)
Nick Benton, Andrew Kennedy, Lennart Beringer, Martin Hofmann
Relational semantics for effect-based program transformations with dynamic allocation. PPDP (2007)
Lennart Beringer, Martin Hofmann
Secure information flow and program logics. CSF (2007)
David Aspinall, Lennart Beringer, Martin Hofmann, Hans-Wolfgang Loidl, Alberto Momigliano
A program logic for resources. Theor. Comput. Sci. 389 (3) (2007)
Lennart Beringer, Martin Hofmann
A Bytecode Logic for JML and Types. APLAS (2006)
Gilles Barthe, Lennart Beringer, Pierre Crégut, Benjamin Grégoire, Martin Hofmann, Peter Müller, Erik Poll, Germán Puebla, Ian Stark, Eric Vétillard
MOBIUS: Mobility, Ubiquity, Security. TGC (2006)
Nick Benton, Andrew Kennedy, Martin Hofmann, Lennart Beringer
Reading, Writing and Relations. APLAS (2006)
Donald Sannella, Martin Hofmann, David Aspinall, Stephen Gilmore, Ian Stark, Lennart Beringer, Hans-Wolfgang Loidl, Kenneth MacKenzie, Alberto Momigliano, Olha Shkaravska
Mobile Resource Guarantees (project evaluation paper). Trends in Functional Programming (2005)
David Aspinall, Lennart Beringer, Martin Hofmann, Hans-Wolfgang Loidl, Alberto Momigliano
A Program Logic for Resource Verification. TPHOLs (2004)
Lennart Beringer, Martin Hofmann, Alberto Momigliano, Olha Shkaravska
Automatic Certification of Heap Consumption. LPAR (2004)
Lennart Beringer, Kenneth MacKenzie, Ian Stark
Grail: a functional form for imperative mobile code. Electron. Notes Theor. Comput. Sci. 85 (1) (2003)
Lennart Beringer
A Programming Language Based Analysis of Operand Forwarding. CHARME (2003)
Lennart Beringer
Typing Assembly Programs with Explicit Forwarding. TACS (2001)

Lennart Beringer.css-eqlu8i{font-size:small;padding-left:4px;}

Publication Activity (10 Years)

Top Topics

Top Venues

Lennart Beringer