![](https://dblp.uni-trier.de/img/logo.ua.320x120.png)
![](https://dblp.uni-trier.de/img/dropdown.dark.16x16.png)
![](https://dblp.uni-trier.de/img/peace.dark.16x16.png)
Остановите войну!
for scientists:
![search dblp search dblp](https://dblp.uni-trier.de/img/search.dark.16x16.png)
![search dblp](https://dblp.uni-trier.de/img/search.dark.16x16.png)
default search action
Lennart Beringer
Person information
- affiliation: Ludwig Maximilian University of Munich, Germany
Refine list
![note](https://dblp.uni-trier.de/img/note-mark.dark.12x12.png)
refinements active!
zoomed in on ?? of ?? records
view refined list in
export refined list as
2020 – today
- 2024
- [c35]Duc-Than Nguyen, Lennart Beringer, William Mansky, Shengyi Wang:
Compositional Verification of Concurrent C Programs with Search Structure Templates. CPP 2024: 60-74 - [c34]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: 99-117 - 2023
- [c33]Qinshi Wang
, Mengying Pan, Shengyi Wang, Ryan Doenges, Lennart Beringer
, Andrew W. Appel
:
Foundational Verification of Stateful P4 Packet Processing. ITP 2023: 32:1-32:20 - [i3]Roshan Sharma, Shengyi Wang, Alexander Oey, Anastasiia Evdokimova, Lennart Beringer, William Mansky:
Proving Logical Atomicity using Lock Invariants. CoRR abs/2304.13898 (2023) - 2022
- [c32]Lennart Beringer:
Verified Software Units for Simple DFA Modules and Objects in C. ISoLA (2) 2022: 237-258 - [p1]Lennart Beringer:
Functional Representations of SSA. SSA-based Compiler Design 2022: 63-88 - 2021
- [j7]Lennart Beringer
, Andrew W. Appel
:
Abstraction and subsumption in modular verification of C programs. Formal Methods Syst. Des. 58(1-2): 322-345 (2021) - [c31]Lennart Beringer
:
Verified Software Units. ESOP 2021: 118-147 - [c30]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: 32:1-32:19
2010 – 2019
- 2019
- [c29]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: 234-248 - [c28]Lennart Beringer, Andrew W. Appel
:
Abstraction and Subsumption in Modular Verification of C Programs. FM 2019: 573-590 - 2018
- [j6]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): 367-422 (2018) - [i2]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 abs/1811.11911 (2018) - 2017
- [c27]Katherine Q. Ye, Matthew Green, Naphat Sanguansin, Lennart Beringer, Adam Petcher, Andrew W. Appel
:
Verified Correctness and Security of mbedTLS HMAC-DRBG. CCS 2017: 2007-2020 - [i1]Katherine Q. Ye, Matthew Green, Naphat Sanguansin, Lennart Beringer, Adam Petcher, Andrew W. Appel:
Verified Correctness and Security of mbedTLS HMAC-DRBG. CoRR abs/1708.08542 (2017) - 2015
- [c26]Gordon Stewart, Lennart Beringer, Santiago Cuéllar, Andrew W. Appel
:
Compositional CompCert. POPL 2015: 275-287 - [c25]Lennart Beringer, Adam Petcher, Katherine Q. Ye, Andrew W. Appel:
Verified Correctness and Security of OpenSSL HMAC. USENIX Security Symposium 2015: 207-221 - 2014
- [c24]Lennart Beringer, Gordon Stewart, Robert Dockins, Andrew W. Appel
:
Verified Compilation for Shared-Memory C. ESOP 2014: 107-127 - 2013
- [j5]Lennart Beringer, Robert Grabowski, Martin Hofmann:
Verifying pointer and string analyses with region type systems. Comput. Lang. Syst. Struct. 39(2): 49-65 (2013) - 2012
- [c23]Lennart Beringer:
End-to-end Multilevel Hybrid Information Flow Control. APLAS 2012: 50-65 - [c22]Gordon Stewart, Lennart Beringer, Andrew W. Appel
:
Verified heap theorem prover by paramodulation. ICFP 2012: 3-14 - [c21]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: 369-389 - [c20]Lennart Beringer, Randall Brukardt, Thomas Plum, S. Tucker Taft:
Panel on compiler certification: should we trust our compiler? HILT 2012: 103-104 - [e1]Lennart Beringer, Amy P. Felty:
Interactive Theorem Proving - Third International Conference, ITP 2012, Princeton, NJ, USA, August 13-15, 2012. Proceedings. Lecture Notes in Computer Science 7406, Springer 2012, ISBN 978-3-642-32346-1 [contents] - 2011
- [c19]Lennart Beringer:
Relational Decomposition. ITP 2011: 39-54 - 2010
- [j4]Lennart Beringer:
Relational bytecode correlations. J. Log. Algebraic Methods Program. 79(7): 483-514 (2010) - [c18]Lennart Beringer, Robert Grabowski, Martin Hofmann:
Verifying Pointer and String Analyses with Region Type Systems. LPAR (Dakar) 2010: 82-102
2000 – 2009
- 2009
- [c17]Robert Grabowski, Lennart Beringer:
Noninterference with Dynamic Security Domains and Policies. ASIAN 2009: 54-68 - [c16]Hans-Wolfgang Loidl, Kenneth MacKenzie, Steffen Jost, Lennart Beringer:
A Proof-Carrying-Code Infrastructure for Resources. LADC 2009: 127-134 - [c15]Nick Benton, Andrew Kennedy, Lennart Beringer, Martin Hofmann:
Relational semantics for effect-based program transformations: higher-order store. PPDP 2009: 301-312 - 2008
- [j3]Lennart Beringer, Martin Hofmann:
Secure information flow and program logics. Arch. Formal Proofs 2008 (2008) - [j2]Lennart Beringer, Martin Hofmann:
A Bytecode Logic for JML and Types. Arch. Formal Proofs 2008 (2008) - 2007
- [j1]David Aspinall, Lennart Beringer, Martin Hofmann, Hans-Wolfgang Loidl, Alberto Momigliano
:
A program logic for resources. Theor. Comput. Sci. 389(3): 411-445 (2007) - [c14]Lennart Beringer, Martin Hofmann:
Secure information flow and program logics. CSF 2007: 233-248 - [c13]Lennart Beringer, Martin Hofmann, Mariela Pavlova:
Certification Using the Mobius Base Logic. FMCO 2007: 25-51 - [c12]Nick Benton, Andrew Kennedy, Lennart Beringer, Martin Hofmann:
Relational semantics for effect-based program transformations with dynamic allocation. PPDP 2007: 87-96 - 2006
- [c11]Nick Benton, Andrew Kennedy, Martin Hofmann, Lennart Beringer:
Reading, Writing and Relations. APLAS 2006: 114-130 - [c10]Lennart Beringer, Martin Hofmann:
A Bytecode Logic for JML and Types. APLAS 2006: 389-405 - [c9]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: 10-29 - [c8]Lennart Beringer:
Functional Elimination of Phi-instructions. COCV@ETAPS 2006: 3-20 - [c7]David Aspinall, Lennart Beringer, Alberto Momigliano
:
Optimisation Validation. COCV@ETAPS 2006: 37-59 - 2005
- [c6]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: 211-226 - 2004
- [c5]Lennart Beringer, Martin Hofmann, Alberto Momigliano, Olha Shkaravska:
Automatic Certification of Heap Consumption. LPAR 2004: 347-362 - [c4]David Aspinall, Lennart Beringer, Martin Hofmann, Hans-Wolfgang Loidl, Alberto Momigliano:
A Program Logic for Resource Verification. TPHOLs 2004: 34-49 - 2003
- [c3]Lennart Beringer:
A Programming Language Based Analysis of Operand Forwarding. CHARME 2003: 270-276 - [c2]Lennart Beringer, Kenneth MacKenzie, Ian Stark
:
Grail: a functional form for imperative mobile code. FGC 2003: 3-23 - 2002
- [b1]Lennart Beringer:
Asynchronous queue machines with explicit forwarding. University of Edinburgh, UK, 2002 - 2001
- [c1]Lennart Beringer:
Typing Assembly Programs with Explicit Forwarding. TACS 2001: 514-534
Coauthor Index
![](https://dblp.uni-trier.de/img/cog.dark.24x24.png)
manage site settings
To protect your privacy, all features that rely on external API calls from your browser are turned off by default. You need to opt-in for them to become active. All settings here will be stored as cookies with your web browser. For more information see our F.A.Q.
Unpaywalled article links
Add open access links from to the list of external document links (if available).
Privacy notice: By enabling the option above, your browser will contact the API of unpaywall.org to load hyperlinks to open access articles. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the Unpaywall privacy policy.
Archived links via Wayback Machine
For web page which are no longer available, try to retrieve content from the of the Internet Archive (if available).
Privacy notice: By enabling the option above, your browser will contact the API of archive.org to check for archived content of web pages that are no longer available. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the Internet Archive privacy policy.
Reference lists
Add a list of references from ,
, and
to record detail pages.
load references from crossref.org and opencitations.net
Privacy notice: By enabling the option above, your browser will contact the APIs of crossref.org, opencitations.net, and semanticscholar.org to load article reference information. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the Crossref privacy policy and the OpenCitations privacy policy, as well as the AI2 Privacy Policy covering Semantic Scholar.
Citation data
Add a list of citing articles from and
to record detail pages.
load citations from opencitations.net
Privacy notice: By enabling the option above, your browser will contact the API of opencitations.net and semanticscholar.org to load citation information. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the OpenCitations privacy policy as well as the AI2 Privacy Policy covering Semantic Scholar.
OpenAlex data
Load additional information about publications from .
Privacy notice: By enabling the option above, your browser will contact the API of openalex.org to load additional information. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the information given by OpenAlex.
last updated on 2024-08-20 22:59 CEST by the dblp team
all metadata released as open data under CC0 1.0 license
see also: Terms of Use | Privacy Policy | Imprint