Lennart Beringer

Associate Director of the NSF Expedition "DeepSpec", 2016-2021

Research scholar in the Verified Software Toolchain project.

Recent (-ish) news and activities

• Conference co-chair of CPP 2022 and CPP 2021
• REMS-DeepSpec, with Peter Sewell (U Cambridge). Previous Deepspec workshops: DeepSpec 2019, DeepSpec 2018, Deep Specifications in the Wild 2017
• I was speaker at seL4 summit 2018, seL4 summit 2019 and seL4 summit 2020
• 04/23/2017: I was happy to speak at Sannellabration today and meet many old friends - happy birthday, Don!
• The book Program logics for certified compilers (Cambridge University Press) is now available, in hardcopy and various ebook formats.
  Update September 2021: The book is now available for free, here
• Transcript of an interview on the VST I gave to Luke Muehlhauser in May 2014.

Program Committee memberships

Research interests

• Interactive theorem proving
• Verification of cryptographic primitives
• Certified compilation in the presence of shared memory interaction
• Proof-carrying code and mobile computation
• Program logics and reasoning principles for low-level languages
• Program analysis and verification
• Reasoning techniques for (asynchronous) processor architectures

Publications

• Verifying a C implementation of Derecho's coordination mechanism using VST and Coq, by Ramana Nagasamudram, Lennart Beringer, Ken Birman, Mae Milano and David Nauman. In Nathan Benz, Divya Gopinath, and Nija Shi (eds.): Proceedings of the 16th NASA Formal Methods Symposium (NFM'24), Springer, June 2024 (accepted).
• Compositional Verification of Concurrent C Programs with Search Structure Templates, by Duc-Tan Nguyen, Lennart Beringer, Willam Mansky, and Shengyi Wang. In Brigitte Pientka and Sandrine Blazy (eds): Proceedings of 13th International Conference On Certified Programs And Proofs (CPP'24), pages 60 - 74, ACM, Janruary 2024.
• Foundational Verification of Stateful P4 Packet Processing, by Qinshi Wang, Mengying Pan, Shengyi Wang, Ryan Doenges, Lennart Beringer, and Andrew W. Appel. In: Adam Naumowicz and Rene Thiemann (eds): Proceedings of the14th International Conference On Interactive Theorem Proving (ITP'23), volume 268, pages 32:1 - 32:20, LIPIcs, Springer, 2023.
• Verified Software Units for Simple DFA Modules and Objects in C. In: Tiziana Margaria and Bernhard Steffen (eds): Proceedings of the11th International Symposium On Leveraging Applications of Formal Methods, Verification and Validation, volume 13702, pages 237--258, LNCS, Springer, 2022.
• Verifying an HTTP Key-Value Server with Interaction Trees and VST, by Hengchu Zhang, Wolf Honoré, Nicolas Koh, Yao Li, Yishuai Li, Li-Yao Xia, Lennart Beringer, William Mansky, Benjamin Pierce, and Steve Zdancewic. In: Liron Cohen and Cezary Kaliszyk (Eds.): Proceedings of the 12th International Conference on Interactive Theorem Proving (ITP 2021), volume 193, pages 32:1-32:19, LIPIcs, Springer, 2021.
• Verified Software Units. In: Nobuko Yoshida (ed):Programming Languages and Systems -- Proceedings of the 30th European Symposium on Programming (ESOP'21), volume 12648, pages 118-147, LNCS, Springer, 2021.
• Abstraction and Subsumption in Modular Verification of C Programs, by Lennart Beringer and Andrew W. Appel. In: Maurice H. ter Beek and Annabelle McIver: Formal Methods -- the next 30 years. Proceedings of the 23rd International Symposium on Formal Methods (FM'19), volume 11800, pages 573-590, LNCS, Springer, 2019.
  Journal version: Formal Methods in System Design (2021), Springer
• From C To Interaction Trees: specifying, verifying and testing a networked server, by Nicolas Koh, Yao Li, Yishuai Li, Li-Yao Xia, Lennart Beringer, Wolf Honore, William Mansky, Benjamin C Pierce, and Steve Zdancewic. CPP 2019 Proceedings of the 8th ACM SIGPLAN International Conference on Certified Programs and Proofs, Pages 234-248, ACM, 2019
• VST-Floyd: A separation logic tool to verify correctness of C programs, by Qinxiang Cao, Lennart Beringer, Samuel Gruetter, Josiah Dodds, and Andrew W. Appel. Journal of Automated Reasoning 61(1), pp. 367-422, Springer, 2018.
• Position paper: the science of deep specification, by Andrew W. Appel, Lennart Beringer, Adam Chlipala, Benjamin C. Pierce, Zhong Shao, Stephanie Weirich, and Steve Zdancewic. Philosophical Transactions of the Royal Society A, Volume 375, Issue 2104, 2017
• Verified Correctness and Security of mbedTLS HMAC-DRBG (with Katherine Q. Ye, Matthew Green, Naphat Sanguansin, Adam Petcher, and Andrew W. Appel). CCS'17: ACM Conference on Computer and Communications Security, October 2017.
• Verified Correctness and Security of OpenSSL HMAC (with Adam Petcher, Katherine Y. Ye, and Andrew W. Appel). Proceedings of the 24th USENIX Security Symposium, Washington DC, August 2015.
• Compositional CompCert (with Gordon Stewart, Santiago Cuellar, and Andrew W. Appel). Proceedings of the 42nd ACM SIGPLAN-SIGACT Symposium on Programming Languages (POPL'15), Mumbai, January 2015, pages 275-287, ACM 2015. (local copy)
• Verified Compilation for Shared-memory C (with Gordon Stewart, Robert Dockins, and Andrew W. Appel). In Zhong Shao (ed.): Proceedings of the 23rd European Symposium on Programming (ESOP'14), Grenoble, April 2014. Volume 8410, pages 107-127, LNCS, Springer, 2014
• Verifying pointer and string analyses with region type systems (with Robert Grabowski and Martin Hofmann). Computer Languages, Systems & Structures, volume 39, number 2, pages 49 - 65, Elsevier, 2013.
• End-to-end multilevel hybrid information flow control. In Ranjit Jhala and Atsushi Igarashi: Proceedings of the Tenth Asian Symposium on Programming Languages and Systems (APLAS '12), Kyoto, December 2012. Volume 7705, pages 50-65, LNCS, Springer, 2012
• Verified Heap Theorem Prover by Paramodulation (with Gordon Stewart and Andrew W. Appel). In ICFP'12: The 17th ACM SIGPLAN International Conference on Functional Programming, Copenhagen, Denmark, September 2012.
• A Certificate Infrastructure for Machine-Checked Proofs of Conditional Information Flow (with Torben Amtoft, Josiah Dodds, Zhi Zhang, Andrew Appel, John Hatcliff, Xinming Ou, and Andrew Cousino). In Pierpaolo Degano and Joshua Guttman (eds.): Proceedings of the First Conference on Principles of Security and Trust (POST 2012), Tallinn, Estonia, March 2012. Volume 7215, pages 369-389, LNCS, Springer, 2012.
• Relational Decomposition. In Herman Geuvers et al. (eds.): Proceedings of the Second International Conference on Interactive Theorem Proving (ITP 2011), Nijmegen, The Netherlands, August 22-25, 2011. Volume 6898, pages 39 -54, LNCS, Springer 2011. The original publication is available at www.springerlink.com. Here are the Isabelle/HOL sources.
• Relational program logics and self-composition. Accepted at VSTTE-theory (informal proceedings). Here are the Isabelle/HOL sources.
• Verifying pointer and string analyses with region type systems (with Robert Grabowski and Martin Hofmann). In Ed Clarke and Andrei Voronkov (eds.): Proceedings of the 16th International Conference on Logic for Programming Artificial Intelligence and Reasoning (LPAR-16), Dakar, Senegal, April 25 - May 1, 2010. Volume 6355 , pages 82--102, LNCS, Springer 2010.
• Relational bytecode correlations. In Tarmo Uustalu and Jüri Vain (eds.): 20th Nordic Workshop on programming theory (NWPT2008), Tallinn, Estonia, 20-22 November 2008. Journal of Logic and Algebraic Programming. Volume 79, Number 7, Elsevier, 2010. An earlier version is here. Here are the Isabelle/HOL sources. And this is the offical page at Elsevier.

• Noninterference with Dynamic Security Domains and Policies (with Robert Grabowski). In Anupam Datta (ed.): Proceedings of the 13th Annual Asian Computing Science Conference (ASIAN'09), Seoul, Korea, December 14-16, 2009. Pages 54--69, volume 5913, LNCS, Springer 2009.
• Relational semantics for effect-based program transformations: higher-order store (with Nick Benton, Martin Hofmann, and Andrew Kennedy). In Antonio Porto, Francisco Javier Lopez-Fraguas (Eds.): Proceedings of the the 11th International ACM SIGPLAN Symposium on Principles and Practice of Declarative Programming (PPDP'09), Coimbra, Portugal, September 7-9, Pages 301-312. ACM Press, 2009.
• A proof-carrying-code infrastructure for resources (with Hans-Wolfgang Loidl, Kenneth MacKenzie, and Steffen Jost). In Proceedings of the Fourth Latin-American Symposium on Dependable Computing (LADC'09), Joao Pessoa, Brazil, September 1-4, pages 127--134, IEEE, 2009.
• Certification using the Mobius Base Logic (with Martin Hofmann and Mariela Pavlova). In Revised Selected Papers of the Sixth Symposium on Software Technologies Concertation on Formal Methods for Components and Objects (FMCO'07), Amsterdam, October 2007, Pages 25-51. LNCS 5382, Springer, 2008
• Secure information flow and program logics (with Martin Hofmann). Proceedings of the 20th IEEE Computer Security Foundations Symposium (CSF'07), Venice, July 2007. IEEE, 2007.
• Relational Semantics for Effect-Based Program Transformations with Dynamic Allocation (with Nick Benton, Andrew Kennedy, and Martin Hofmann). Proceedings of the 9th International ACM SIGPLAN Symposium on Principles and Practice of Declarative Programming (PPDP'07), Wrozlaw, July 2007. ACM, 2007.
• A program logic for resources (with David Aspinall, Martin Hofmann, Hans-Wolfgang Loidl, and Alberto Momigliano). Pages 411-445, Theoretical Computer Science, Volume 389, Number 3, December 2007, Elsevier 2007.
• Optimisation Validation (with Alberto Momigliano and David Aspinall). In Proceedings of the 5th International Workshop on Compiler Optimization Meets Compiler Verification (COCV 2006), Vienna, Austria, April 2, 2006. Volume 176, Issue 3, Pages 37 - 59. Electronic Notes in Theoretical Computer Science, Elsevier Science, 2007.
• Functional Elimination of $\Phi$-instructions . In Proceedings of the 5th International Workshop on Compiler Optimization Meets Compiler Verification (COCV 2006), Vienna, Austria, April 2, 2006. Volume 176, Issue 3, Pages 3 - 20. Electronic Notes in Theoretical Computer Science, Elsevier Science 2007. Here is an extended version.
• MOBIUS: Mobility, Ubiquity, Security. Objectives and progress report (with Gilles Barthe, Pierre Cregut, Benjamin Gregoire, Martin Hofmann, Peter Mueller, Erik Poll, German Puebla, Ian Stark, and Eric Vetillard). In: Ugo Montanari and Donald Sannella and Roberto Bruni (editors), Revised Selected Papers of the Second Symposium on Trustworthy Global Computing (TGC'06), Lucca. Pages 10-29, LNCS 4661, Springer, November 2006.
• Reading, Writing and Relations: Towards Extensional Semantics for Effect Analyses (with Nick Benton, Andrew Kennedy, and Martin Hofmann). In Naoki Kobayashi (editor): Proceedings of the Fourth Asian Symposium on Programming Languages and Systems (APLAS '06). Pages 114-130, LNCS 4279, Springer, November 2006.
• A Bytecode Logic for JML and Types (with Martin Hofmann). In Naoki Kobayashi (editor): Proceedings of the Fourth Asian Symposium on Programming Languages and Systems (APLAS '06). Pages 389-405, LNCS 4279, Springer, November 2006.
• Mobile Resource Guarantees (project evaluation paper) (with Donald Sannella, Martin Hofmann, David Aspinall, Stephen Gilmore, Ian Stark, Hans-Wolfgang Loidl, Kenneth MacKenzie, Alberto Momigliano, and Olha Shkaravska). Pages 211-226 of Marko C. J. D. van Eekelen (editor): Revised Selected Papers from the Sixth Symposium on Trends in Functional Programming (TFP 2005), Tallinn, Estonia, 23-24 September 2005. Intellect, Trends in Functional Programming (volume 6), 2007.
• Certification of Resource Consumption: from Types to Logic (Programming) (with Alberto Momigliano). In Enrico Pontelli (editor): Newsletter of the Association for Logic Programming (ALP), Volume 18 No. 2, May 2005.
• Automatic Certification of Heap Consumption (with Martin Hofmann, Alberto Momigliano, and Olha Shkaravska). In Franz Baader and Andrei Voronkov (editors): Proceedings of the 11th International Conference on Logic for Programming, Artificial Intelligence and Reasoning (LPAR2004), Montevideo, Uruguay, March 14-18th, 2005. Volume 3452 of Lecure Notes in Artificial Intelligence, Springer.
• A Program Logic for Resource Verification (with David Aspinall, Martin Hofmann, Hans-Wolfgang Loidl and Alberto Momigliano). In Konrad Slind, Annette Bunker, and Ganesh C.Gopalakrishnan (editors): Proceedings of the 17th International Conference on Theorem Proving in Higher Order Logics (TPHOLs2004), Park City, Utah, September 14-17, 2004. Volume 3223 of Lecture Notes in Computer Science, Springer.
• Towards certificate generation for linear heap consumption (with Martin Hofmann, Alberto Momigliano and Olha Shkaravska). Proceedings of the ICALP/LICS Workshop on Logics for Resources, Processes, and Programs (LRPP2004), Turku, July 2004.
• A programming language based analysis of operand forwarding. Proceedings of the 12th Advanced Research Working Conference on Correct Hardware Design and Verification Methods (CHARME'03), L'Aquila, October 2003. Volume 2860 of Lecture Notes in Computer Science, Springer.
• The Dr Jekyll and Mr Hyde paper: Grail: A Functional Form for Imperative Mobile Code (with Kenneth MacKenzie and Ian Stark). Proceedings of the 2nd EATCS Workshop on Foundations of Global Computing (FGC'03), Eindhoven, June 2003. Volume 85(1), 2003 of Electronic Notes in Theoretical Computer Science.
• Asynchronous Queue Machines with explicit forwarding. PhD thesis, School of Informatics, University of Edinburgh, 2002.
• Typing assembly programs with explicit forwarding. Proceedings of the 4th International Symposium on Theoretical Aspects of Computer Software (TACS'01), Sendai, October 2001. Volume 2215 of Lecture Notes in Computer Science, Springer.
• Type-correct Forwarding in Asynchronous Processors. Presented at the 9th UK Asynchronous forum, Cambridge, 2000.
• Deadlock-free Scheduling in Micronet-based Asynchronous Processors. Diplomarbeit, Technical University of Berlin, 1998