Lennart Beringer
Department of Computer Science
Princeton University
35 Olden Street
Princeton, NJ 08540
eberingeATcs.princeton.edu
Phone: ++1 - (609) - 258 0451


Associate research scholar in the Verified Software Toolchain project.

Upcoming events

• ITP 2013 (PC member)

• HILT 2012 (PC member, panelist)
• ITP 2012 (general co-chair and PC co-chair)
• Bytecode 2012 (PC member)
• Aplas 2010 (PC member)

• Theorem proving and certified compilation
• 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 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