| 2023 | ESOP | Interpreting Knowledge-based Programs. | Alexander Knapp, Heribert Mhlberger, Bernhard Reus |
| 2020 | CAV | Towards Model Checking Real-World Software-Defined Networks. | Vasileios Klimis, George Parisis, Bernhard Reus |
| 2020 | FMCAD | Model Checking Software-Defined Networks with Flow Entries that Time Out. | Vasileios Klimis, George Parisis, Bernhard Reus |
| 2012 | ECOOP | Verifying the reflective visitor pattern. | Ben Horsfall, Nathaniel Charlton, Bernhard Reus |
| 2012 | VMCAI | Crowfoot: A Verifier for Higher-Order Store Programs. | Nathaniel Charlton, Ben Horsfall, Bernhard Reus |
| 2011 | CSL | Relative Completeness for Logics of Functional Programs. | Bernhard Reus, Thomas Streicher |
| 2011 | FCT | Specification Patterns and Proofs for Recursion through the Store. | Nathaniel Charlton, Bernhard Reus |
| 2011 | ICDE | Formal reasoning about runtime code update. | Nathaniel Charlton, Ben Horsfall, Bernhard Reus |
| 2011 | POPL | Step-indexed kripke models over recursive worlds. | Lars Birkedal, Bernhard Reus, Jan Schwinghammer, Kristian Stvring, Jacob Thamsborg, Hongseok Yang |
| 2010 | FOSSACS | A Semantic Foundation for Hidden State. | Jan Schwinghammer, Hongseok Yang, Lars Birkedal, Franois Pottier, Bernhard Reus |
| 2009 | CSL | Nested Hoare Triples and Frame Rules for Higher-Order Store. | Jan Schwinghammer, Lars Birkedal, Bernhard Reus, Hongseok Yang |
| 2008 | ICALP | A Simple Model of Separation Logic for Higher-Order Store. | Lars Birkedal, Bernhard Reus, Jan Schwinghammer, Hongseok Yang |
| 2006 | CSL | Separation Logic for Higher-Order Store. | Bernhard Reus, Jan Schwinghammer |
| 2005 | ESOP | Denotational Semantics for Abadi and Leino's Logic of Objects. | Bernhard Reus, Jan Schwinghammer |
| 2005 | ICALP | About Hoare Logics for Higher-Order Store. | Bernhard Reus, Thomas Streicher |
| 2003 | CSL | Modular Semantics and Logics of Classes. | Bernhard Reus |
| 2002 | LICS | Semantics and Logic of Object Calculi. | Bernhard Reus, Thomas Streicher |
| 2001 | FASE | A Hoare Calculus for Verifying Java Realizations of OCL-Constrained Design Models. | Bernhard Reus, Martin Wirsing, Rolf Hennicker |
| 1999 | CSL | Monadic Presentations of Lambda Terms Using Generalized Inductive Types. | Thorsten Altenkirch, Bernhard Reus |
| 1993 | MFCS | Verifying Properties of Module Construction in Type Theory. | Bernhard Reus, Thomas Streicher |