Lennart Beringer
Department of Computer Science
Princeton University
35 Olden Street
Princeton, NJ 08540

Phone: ++1 - (609) - 258 0451


Associate research scholar in the Concurrent Cminor project.

Research interests:

• 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:

• Relational bytecode correlations To appear in Journal of Logic and Algebraic Programming. Here are the Isabelle/HOL sources

• Noninterference with Dynamic Security Domains and Policies (with Robert Grabowski). In Proceedings of the 13th Annual Asian Computing Science Conference (ASIAN'09), Seoul, Korea, December 14-16, 2009. To appear.
• 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, 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