Typing Assembly Programs with Explicit Forwarding. - Lennart Beringer (TACS, 2001)

Asynchronous queue machines with explicit forwarding. - Lennart Beringer (2002)

A Programming Language Based Analysis of Operand Forwarding. - Lennart Beringer (CHARME, 2003)

Grail: a functional form for imperative mobile code. - Lennart Beringer; Kenneth MacKenzie; Ian Stark (FGC, 2003)

Automatic Certification of Heap Consumption. - Lennart Beringer; Martin Hofmann 001; Alberto Momigliano; Olha Shkaravska (LPAR, 2004)

A Program Logic for Resource Verification. - David Aspinall 001; Lennart Beringer; Martin Hofmann 001; Hans-Wolfgang Loidl; Alberto Momigliano (TPHOLs, 2004)

Mobile Resource Guarantees (project evaluation paper). - Donald Sannella; Martin Hofmann 001; David Aspinall 001; Stephen Gilmore; Ian Stark; Lennart Beringer; Hans-Wolfgang Loidl; Kenneth MacKenzie; Alberto Momigliano; Olha Shkaravska (Trends in Functional Programming, 2005)

Reading, Writing and Relations. - Nick Benton; Andrew Kennedy; Martin Hofmann 001; Lennart Beringer (APLAS, 2006)

MOBIUS: Mobility, Ubiquity, Security. - Gilles Barthe; Lennart Beringer; Pierre Crégut; Benjamin Grégoire; Martin Hofmann 001; Peter Müller 001; Erik Poll; Germán Puebla; Ian Stark; Eric Vétillard (TGC, 2006)

Optimisation Validation. - David Aspinall 001; Lennart Beringer; Alberto Momigliano (COCV@ETAPS, 2006)

Functional Elimination of Phi-instructions. - Lennart Beringer (COCV@ETAPS, 2006)

Certification Using the Mobius Base Logic. - Lennart Beringer; Martin Hofmann 001; Mariela Pavlova (FMCO, 2007)

Relational semantics for effect-based program transformations with dynamic allocation. - Nick Benton; Andrew Kennedy; Lennart Beringer; Martin Hofmann 001 (PPDP, 2007)

A program logic for resources. - David Aspinall 001; Lennart Beringer; Martin Hofmann 001; Hans-Wolfgang Loidl; Alberto Momigliano (Theor. Comput. Sci., 2007)

Secure information flow and program logics. - Lennart Beringer; Martin Hofmann 001 (Arch. Formal Proofs, 2008)

A Bytecode Logic for JML and Types. - Lennart Beringer; Martin Hofmann 001 (Arch. Formal Proofs, 2008)

Noninterference with Dynamic Security Domains and Policies. - Robert Grabowski; Lennart Beringer (ASIAN, 2009)

A Proof-Carrying-Code Infrastructure for Resources. - Hans-Wolfgang Loidl; Kenneth MacKenzie; Steffen Jost; Lennart Beringer (LADC, 2009)

Relational semantics for effect-based program transformations: higher-order store. - Nick Benton; Andrew Kennedy; Lennart Beringer; Martin Hofmann 001 (PPDP, 2009)

Relational bytecode correlations. - Lennart Beringer (J. Log. Algebraic Methods Program., 2010)

Relational Decomposition. - Lennart Beringer (ITP, 2011)

End-to-end Multilevel Hybrid Information Flow Control. - Lennart Beringer (APLAS, 2012)

Verified heap theorem prover by paramodulation. - Gordon Stewart 001; Lennart Beringer; Andrew W. Appel (ICFP, 2012)

A Certificate Infrastructure for Machine-Checked Proofs of Conditional Information Flow. - Torben Amtoft; Josiah Dodds; Zhi Zhang; Andrew W. Appel; Lennart Beringer; John Hatcliff; Xinming Ou; Andrew Cousino (POST, 2012)

Panel on compiler certification: should we trust our compiler? - Lennart Beringer; Randall Brukardt; Thomas Plum 003; S. Tucker Taft (HILT, 2012)

Verifying pointer and string analyses with region type systems. - Lennart Beringer; Robert Grabowski; Martin Hofmann 001 (Comput. Lang. Syst. Struct., 2013)

Verified Compilation for Shared-Memory C. - Lennart Beringer; Gordon Stewart 001; Robert Dockins; Andrew W. Appel (ESOP, 2014)

Compositional CompCert. - Gordon Stewart 001; Lennart Beringer; Santiago Cuéllar; Andrew W. Appel (POPL, 2015)

Verified Correctness and Security of OpenSSL HMAC. - Lennart Beringer; Adam Petcher; Katherine Q. Ye; Andrew W. Appel (USENIX Security Symposium, 2015)

Verified Correctness and Security of mbedTLS HMAC-DRBG. - Katherine Q. Ye; Matthew Green 001; Naphat Sanguansin; Lennart Beringer; Adam Petcher; Andrew W. Appel (CCS, 2017)

VST-Floyd: A Separation Logic Tool to Verify Correctness of C Programs. - Qinxiang Cao; Lennart Beringer; Samuel Gruetter; Josiah Dodds; Andrew W. Appel (J. Autom. Reason., 2018)

From C to interaction trees: specifying, verifying, and testing a networked server. - Nicolas Koh; Yao Li 004; Yishuai Li; Li-yao Xia; Lennart Beringer; Wolf Honoré; William Mansky; Benjamin C. Pierce; Steve Zdancewic (CPP, 2019)

Verified Software Units. - Lennart Beringer (ESOP, 2021)

Verifying an HTTP Key-Value Server with Interaction Trees and VST. - Hengchu Zhang; Wolf Honoré; Nicolas Koh; Yao Li 004; Yishuai Li; Li-yao Xia; Lennart Beringer; William Mansky; Benjamin C. Pierce; Steve Zdancewic (ITP, 2021)

Abstraction and subsumption in modular verification of C programs. - Lennart Beringer; Andrew W. Appel (Formal Methods Syst. Des., 2021)

Functional Representations of SSA. - Lennart Beringer (SSA-based Compiler Design, 2022)

Verified Software Units for Simple DFA Modules and Objects in C. - Lennart Beringer (ISoLA (2), 2022)

Foundational Verification of Stateful P4 Packet Processing. - Qinshi Wang; Mengying Pan; Shengyi Wang; Ryan Doenges; Lennart Beringer; Andrew W. Appel (ITP, 2023)

Proving Logical Atomicity using Lock Invariants. - Roshan Sharma; Shengyi Wang; Alexander Oey; Anastasiia Evdokimova; Lennart Beringer; William Mansky (CoRR, 2023)

Compositional Verification of Concurrent C Programs with Search Structure Templates. - Duc-Than Nguyen; Lennart Beringer; William Mansky; Shengyi Wang (CPP, 2024)

Verifying a C Implementation of Derecho's Coordination Mechanism Using VST and Coq. - Ramana Nagasamudram; Lennart Beringer; Ken Birman; Mae Milano; David A. Naumann (NFM, 2024)

Verifying a C implementation of Derecho's coordination mechanism using VST and Coq (artifact). - Ramana Nagasamudram; Lennart Beringer; Ken Birman; Mae Milano; David A. Naumann (Zenodo, 2024)