Lennart Beringer

According to our database, Lennart Beringer authored at least 42 papers between 2001 and 2024.

Collaborative distances:

• Dijkstra number of four.
• Erdős number of four.

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

Dataset, March, 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

Proceedings of the NASA Formal Methods - 16th International Symposium, 2024

Compositional Verification of Concurrent C Programs with Search Structure Templates.

Duc-Than Nguyen, Lennart Beringer, William Mansky, Shengyi Wang

Proceedings of the 13th ACM SIGPLAN International Conference on Certified Programs and Proofs, 2024

2023

Proving Logical Atomicity using Lock Invariants.

Roshan Sharma, Shengyi Wang, Alexander Oey, Anastasiia Evdokimova, Lennart Beringer, William Mansky

CoRR, 2023

Foundational Verification of Stateful P4 Packet Processing.

Qinshi Wang, Mengying Pan, Shengyi Wang, Ryan Doenges, Lennart Beringer, Andrew W. Appel

Proceedings of the 14th International Conference on Interactive Theorem Proving, 2023

2022

Verified Software Units for Simple DFA Modules and Objects in C.

Lennart Beringer

Proceedings of the Leveraging Applications of Formal Methods, Verification and Validation. Software Engineering, 2022

Functional Representations of SSA.

Lennart Beringer

Proceedings of the SSA-based Compiler Design, 2022

2021

Abstraction and subsumption in modular verification of C programs.

Lennart Beringer, Andrew W. Appel

Formal Methods Syst. Des., 2021

Verifying an HTTP Key-Value Server with Interaction Trees and VST.

Hengchu Zhang, Wolf Honoré, Nicolas Koh, Yao Li, Yishuai Li, Li-yao Xia, Lennart Beringer, William Mansky, Benjamin C. Pierce, Steve Zdancewic

Proceedings of the 12th International Conference on Interactive Theorem Proving, 2021

Verified Software Units.

Lennart Beringer

Proceedings of the Programming Languages and Systems, 2021

2019

From C to interaction trees: specifying, verifying, and testing a networked server.

Nicolas Koh, Yao Li, Yishuai Li, Li-yao Xia, Lennart Beringer, Wolf Honoré, William Mansky, Benjamin C. Pierce, Steve Zdancewic

Proceedings of the 8th ACM SIGPLAN International Conference on Certified Programs and Proofs, 2019

2018

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

2017

Verified Correctness and Security of mbedTLS HMAC-DRBG.

Katherine Q. Ye, Matthew Green, Naphat Sanguansin, Lennart Beringer, Adam Petcher, Andrew W. Appel

Proceedings of the 2017 ACM SIGSAC Conference on Computer and Communications Security, 2017

2015

Verified Correctness and Security of OpenSSL HMAC.

Lennart Beringer, Adam Petcher, Katherine Q. Ye, Andrew W. Appel

Proceedings of the 24th USENIX Security Symposium, 2015

Compositional CompCert.

Gordon Stewart, Lennart Beringer, Santiago Cuéllar, Andrew W. Appel

Proceedings of the 42nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 2015

2014

Verified Compilation for Shared-Memory C.

Lennart Beringer, Gordon Stewart, Robert Dockins, Andrew W. Appel

Proceedings of the Programming Languages and Systems, 2014

2013

Verifying pointer and string analyses with region type systems.

Lennart Beringer, Robert Grabowski, Martin Hofmann

Comput. Lang. Syst. Struct., 2013

2012

Panel on compiler certification: should we trust our compiler?

Lennart Beringer, Randall Brukardt, Thomas Plum, S. Tucker Taft

Proceedings of the 2012 ACM Conference on High Integrity Language Technology, 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

Proceedings of the Principles of Security and Trust - First International Conference, 2012

Verified heap theorem prover by paramodulation.

Gordon Stewart, Lennart Beringer, Andrew W. Appel

Proceedings of the ACM SIGPLAN International Conference on Functional Programming, 2012

End-to-end Multilevel Hybrid Information Flow Control.

Lennart Beringer

Proceedings of the Programming Languages and Systems - 10th Asian Symposium, 2012

2011

Relational Decomposition.

Lennart Beringer

Proceedings of the Interactive Theorem Proving - Second International Conference, 2011

2010

Relational bytecode correlations.

Lennart Beringer

J. Log. Algebraic Methods Program., 2010

2009

Relational semantics for effect-based program transformations: higher-order store.

Nick Benton, Andrew Kennedy, Lennart Beringer, Martin Hofmann

Proceedings of the 11th International ACM SIGPLAN Conference on Principles and Practice of Declarative Programming, 2009

A Proof-Carrying-Code Infrastructure for Resources.

Hans-Wolfgang Loidl, Kenneth MacKenzie, Steffen Jost, Lennart Beringer

Proceedings of the Fourth Latin-American Symposium on Dependable Computing, 2009

Noninterference with Dynamic Security Domains and Policies.

Robert Grabowski, Lennart Beringer

Proceedings of the Advances in Computer Science, 2009

2008

A Bytecode Logic for JML and Types.

Lennart Beringer, Martin Hofmann

Arch. Formal Proofs, 2008

Secure information flow and program logics.

Lennart Beringer, Martin Hofmann

Arch. Formal Proofs, 2008

2007

A program logic for resources.

David Aspinall, Lennart Beringer, Martin Hofmann, Hans-Wolfgang Loidl, Alberto Momigliano

Theor. Comput. Sci., 2007

Relational semantics for effect-based program transformations with dynamic allocation.

Nick Benton, Andrew Kennedy, Lennart Beringer, Martin Hofmann

Proceedings of the 9th International ACM SIGPLAN Conference on Principles and Practice of Declarative Programming, 2007

Certification Using the Mobius Base Logic.

Lennart Beringer, Martin Hofmann, Mariela Pavlova

Proceedings of the Formal Methods for Components and Objects, 6th International Symposium, 2007

2006

Functional Elimination of Phi-instructions.

Lennart Beringer

Proceedings of the 5th International Workshop on Compiler Optimization meets Compiler Verification, 2006

Optimisation Validation.

David Aspinall, Lennart Beringer, Alberto Momigliano

Proceedings of the 5th International Workshop on Compiler Optimization meets Compiler Verification, 2006

MOBIUS: Mobility, Ubiquity, Security.

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

Proceedings of the Trustworthy Global Computing, Second Symposium, 2006

Reading, Writing and Relations.

Nick Benton, Andrew Kennedy, Martin Hofmann, Lennart Beringer

Proceedings of the Programming Languages and Systems, 4th Asian Symposium, 2006

2005

Mobile Resource Guarantees (project evaluation paper).

Donald Sannella, Martin Hofmann, David Aspinall, Stephen Gilmore, Ian Stark, Lennart Beringer, Hans-Wolfgang Loidl, Kenneth MacKenzie, Alberto Momigliano, Olha Shkaravska

Proceedings of the Revised Selected Papers from the Sixth Symposium on Trends in Functional Programming, 2005

2004

A Program Logic for Resource Verification.

David Aspinall, Lennart Beringer, Martin Hofmann, Hans-Wolfgang Loidl, Alberto Momigliano

Proceedings of the Theorem Proving in Higher Order Logics, 17th International Conference, 2004

Automatic Certification of Heap Consumption.

Lennart Beringer, Martin Hofmann, Alberto Momigliano, Olha Shkaravska

Proceedings of the Logic for Programming, 2004

2003

Grail: a functional form for imperative mobile code.

Lennart Beringer, Kenneth MacKenzie, Ian Stark

Proceedings of the 2nd EATCS Workshop on Foundations of Global Computing, 2003

A Programming Language Based Analysis of Operand Forwarding.

Lennart Beringer

Proceedings of the Correct Hardware Design and Verification Methods, 2003

2002

Asynchronous queue machines with explicit forwarding.

Lennart Beringer

PhD thesis, 2002

2001

Typing Assembly Programs with Explicit Forwarding.

Lennart Beringer

Proceedings of the Theoretical Aspects of Computer Software, 4th International Symposium, 2001