Lennart Beringer

48 papers A* 3A 4B 11C 2Journal 10Unranked 16

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