ÄûÃÊÊÓƵ

Foundations of Software Systems (FoSS)

Bernhard Reus

Selected Publications

2024

  • Loyal, L., Jürchott, K., Reimer, U., Meyer-Arndt, L., Henze, L., Mages, N., . . . Thiel, A. (2024). Aging and viral evolution impair immunity against dominant pan-coronavirus-reactive T cell epitope. doi:10.1101/2024.08.21.608923
    Preprint. .

2023

  • Fuhrmann, S., Reus, B., Frey, O., Pera, A., Picker, L., & Kern, F. (2023). Marked skewing of entire T-cell memory compartment occurs only in a minority of CMVinfected individuals and is unrelated to the degree of memory subset skewing among CMVspecific T-cells. Frontiers in Immunology, 14, pages. doi:10.3389/fimmu.2023.1258339
    Article. .
  • Knapp, A., Mühlberger, H., & Reus, B. (2023). Interpreting knowledge-based programs. In ESOP 2023 : 32st European Symposium on Programming Vol. 13990 (pp. pages). Paris, France: Springer. doi:10.1007/978-3-031-30044-8_10
    Conference publication. .
  • Knapp, A., Mühlberger, H., & Reus, B. (2023). Interpreting Knowledge-based Programs (Extended Version with Proofs). doi:10.48550/arxiv.2301.10807
    Preprint. .

2021

  • Reus, B., Caserta, S., Larsen, M., Morrow, G., Bano, A., Hallensleben, M., . . . Kern, F. (2021). In-depth profiling of T-cell responsiveness to commonly recognized CMV antigens in older people reveals important sex differences. Frontiers in Immunology, 12, 1-21. doi:10.3389/fimmu.2021.707830
    Article. .
  • Kirkham, F., Pera, A., Simanek, A. M., Bano, A., Morrow, G., Reus, B., . . . Kern, F. (n.d.). Cytomegalovirus infection is associated with an increase in aortic stiffness in older men which may be mediated in part by CD4 memory T-cells. Theranostics, pages. doi:10.7150/thno.58356
    Article. .

2020

  • Klimis, V., Parisis, G., & Reus, B. (2020). Model checking software-defined networks with flow entries that time out. In Proceedings of the 20th Conference on Formal Methods in Computer-Aided Design – FMCAD 2020 Vol. 1 (pp. 179-184). Wien: IEEE. doi:10.34727/2020/isbn.978-3-85448-042-6_25
    Conference publication. .
  • Klimis, V., Parisis, G., & Reus, B. (2020). Model Checking Software-Defined Networks with Flow Entries that Time Out (version with appendix). Retrieved from http://arxiv.org/abs/2008.06149v2
    Preprint.
  • Klimis, V., Parisis, G., & Reus, B. (2020, July 19). Towards model checking real-world software-defined networks. In Computer Aided Verification. CAV 2020. Lecture Notes in Computer Science Vol. 12225 (pp. 126-148). Los Angeles, California, USA: Springer Verlag. doi:10.1007/978-3-030-53291-8_8
    Conference publication. .
  • Klimis, V., Parisis, G., & Reus, B. (2020). Towards Model Checking Real-World Software-Defined Networks (version with appendix). Retrieved from http://arxiv.org/abs/2004.11988v5
    Preprint.

2018

  • Rojas, A. P., Caserta, S., Albanese, F., Blowers, P., Morrow, G., Terrazzini, N., . . . Kern, F. (2018). CD28null pro-atherogenic CD4 T-cells explain the link between CMV infection and an increased risk of Cardiovascular death. Theranostics, 8(16), 4509-4519. doi:10.7150/thno.27428
    Article. .

2017

  • Altenkirch, T., Capriotti, P., & Reus, B. (2017). Domain theory in type theory via QIITs. In Leibniz International Proceedings in Informatics, LIPIcs Vol. 104 (pp. 16-17).
    Conference publication.

2016

  • Reus, B. (2016). Limits of Computation. Springer International Publishing. doi:10.1007/978-3-319-27889-6
    Book. .

2015

  • Reus, B., Charlton, N., & Horsfall, B. (2015). Symbolic execution proofs for higher order store programs. Journal of Automated Reasoning, 54(3), 199-284. doi:10.1007/s10817-014-9319-8
    Article. .

2013

  • Charlton, N., & Reus, B. (2013). Specification patterns for reasoning about recursion through the store. Information and Computation, 231, 167-203. doi:10.1016/j.ic.2013.08.011
    Article. .

2012

  • Schwinghammer, J., Birkedal, L., Pottier, F., Reus, B., Stovring, K., & Yang, H. (2012). A step-indexed Kripke model of hidden state. Mathematical Structures in Computer Science, 23(1), 1-54. doi:10.1017/S0960129512000035
    Article. .
  • Horsfall, B., Charlton, N., & Reus, B. (2012). Verifying the reflective visitor pattern. In Proceedings for FTfJP 2012: The 14th Workshop on Formal Techniques for Java-Like Programs - Co-located with ECOOP 2012 and PLDI 2012, Papers Presented at the Workshop (pp. 27-34). doi:10.1145/2318202.2318208
    Conference publication. .
  • Reus, B., & Streicher, T. (2012). A synthetic theory of sequential domains. Annals of Pure and Applied Logic, 163(8), 1062-1074. doi:10.1016/j.apal.2011.12.028
    Article. .
  • Charlton, N., Horsfall, B., & Reus, B. (2012). Crowfoot: a verifier for higher-order store programs. In Verification, Model Checking, and Abstract Interpretation (Vol. 7148, pp. 136-151). Springer. doi:10.1007/978-3-642-27940-9_10
    Chapter. .

2011

  • Schwinghammer, J., Birkedal, L., Reus, B., & Yang, H. (2011). Nested Hoare Triples and Frame Rules for Higher-order Store. Logical Methods in Computer Science, 7(3), 1-42. doi:10.2168/LMCS-7(3:21)2011
    Article. .
  • Schwinghammer, J., Birkedal, L., Reus, B., & Yang, H. (2011). Nested Hoare Triples and Frame Rules for Higher-order Store. doi:10.48550/arxiv.1109.3031
    Preprint. .
  • Reus, B., & Streicher, T. (2011). Relative Completeness for Logics of Functional Programs. In Computer Science Logic, 25th International Workshop / 20th Annual Conference of the EACSL, CSL 2011. Bergen (Norway).
    Presentation. .
  • Charlton, N., & Reus, B. (2011). Specification patterns and proofs for recursion through the store. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) Vol. 6914 LNCS (pp. 310-321). doi:10.1007/978-3-642-22953-4_27
    Conference publication. .
  • Charlton, N., Horsfall, B., & Reus, B. (2011). Formal reasoning about runtime code update. In Proceedings - International Conference on Data Engineering (pp. 134-138). doi:10.1109/ICDEW.2011.5767624
    Conference publication. .
  • Birkedal, L., Reus, B., Schwinghammer, J., Støvring, K., Thamsborg, J., & Yang, H. (2011). Step-indexed kripke models over recursive worlds. In ACM SIGPLAN Notices Vol. 46 (pp. 119-131). doi:10.1145/1925844.1926401
    Conference publication. .
  • Birkedal, L., Reus, B., Schwinghammer, J., Stovring, K., Thamsborg, J., & Yang, H. (2011). Step-indexed kripke models over recursive worlds. In POPL '11 Proceedings of the 38th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages (Vol. 38, pp. 119-132). ACM.
    Chapter. .

2010

  • Reus, B., Jung, A., Keimel, K., & Streicher, T. (2010). Preface for the special issue on domains. Mathematical Structures in Computer Science, 20(2), 105-106. doi:10.1017/S0960129509990338
    Article. .
  • Schwinghammer, J., Yang, H., Birkedal, L., Pottier, F., & Reus, B. (2010). A semantic foundation for hidden state. In FOSSACS 2010. Paphos.
    Presentation. .

2009

  • Schwinghammer, J., Birkedal, L., Reus, B., & Yang, H. (2009). Nested hoare triples and frame rules for higher-order store. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) Vol. 5771 LNCS (pp. 440-454). doi:10.1007/978-3-642-04027-6_32
    Conference publication. .
  • Charlton, N., & Reus, B. (2009). A decidable class of verification conditions for programs with higher order store. In Electronic Communications of the EASST Vol. 23. doi:10.14279/tuj.eceasst.23.318.303
    Conference publication. .

2008

  • Birkedal, L., Reus, B., Schwinghammer, J., & Yang, H. (2008). A simple model of separation logic for higher-order store. In 35th International Colloquium on Automata, Languages and Programming. Keykjavik, ICELAND, JUL 07-11, 2008. doi:10.1007/978-3-540-70583-3_29
    Presentation. .

2007

  • Reus, B. (1996). Synthetic domain theory in type theory: Another logic of computable functions. In Theorem Proving in Higher Order Logics (Vol. 1125, pp. 363-380). Springer Nature. doi:10.1007/bfb0105416
    Chapter. .

2006

  • Reus, B., & Schwinghammer, J. (2006). Separation Logic for Higher-Order Store. In Computer Science Logic 2006. Szeged, Hungary.
    Presentation. .
  • Reus, B., & Schwinghammer, J. (2006). Denotational semantics for a program logic of objects. Mathematical Structures in Computer Science, 16(2), :313-358. doi:10.1017/S0960129506005214
    Article. .

2005

  • Reus, B., & Streicher, T. (2005). About Hoare logics for higher-order store. In 32nd International Colloquium on Automata, Languages and Programming Languages (ICALP), LNCS. Lisbon. doi:10.1007/11523468
    Presentation. .
  • Reus, B., & Schwinghammer, J. (2005). Denotational semantics for Abadi and Leino's logic of objects. In Unknown Book (Vol. 3444, pp. 16.0 pages). Springer.
    Chapter. .
  • Pattinson, D., & Reus, B. (2005). A complete temporal and spatial logic for distributed dystems. In Frontiers of Combining Systems: Proceedings of the 5th International Workshop, FroCoS 2005, Vienna, Austria (Vol. 3717, pp. 122-137). Springer. doi:10.1007/11559306_7
    Chapter. .
  • Reus, B., & Streicher, T. (2005). About Hoare logics for higher-order store. In Automata, Languages and Programming: Proceedings of the 32nd International Colloquim, ICALP 2005, Lisbon, Portugal (Vol. 3580, pp. 1337-1348). Berlin, Germany: Springer Verlag. doi:10.1007/11523468_108
    Chapter. .
  • Reus, B., & Schwinghammer, J. (2005). Denotational Semantics for Abadi and Leino’s Logic of Objects. doi:10.1007/978-3-540-31987-0_19
    Presentation. .
  • Reus, B., & Schwinghammer, J. (2005). Denotational semantics for Abadi and Leino's logic of objects. In Programming Languages and Systems: Proceedings of the 14th European Symposium on Programming, ESOP 2005, Edinburgh, UK (Vol. 3444, pp. 263-278). Springer. doi:10.1007/b107380
    Chapter. .

2004

  • Reus, B., & Streicher, T. (2004). Semantics and logic of object calculi. Theoretical Computer Science, 316(1-3), 191-213. doi:10.1016/j.tcs.2004.01.030
    Article. .

2003

  • Reus, B. (2003). Modular semantics and logics of classes. In 12th Annual Conference of the European-Association-for-Computer-Logic/8th Kurt Godel Colloquium/17th International Workshop on Computer Science Logic. Vienna, Austria. doi:10.1007/b13224
    Presentation. .
  • Altenkirch, T., & Reus, B. (1999). Monadic Presentations of Lambda Terms Using Generalized Inductive Types. In Lecture Notes in Computer Science (pp. 453-468). Springer Berlin Heidelberg. doi:10.1007/3-540-48168-0_32
    Chapter. .
  • Reus, B. (2003). Modular Semantics and Logics of Classes. In Lecture Notes in Computer Science (pp. 456-469). Springer Berlin Heidelberg. doi:10.1007/978-3-540-45220-1_37
    Chapter. .
  • Reus, B. (2003). Modular semantics and logics of classes. In Unknown Book (Vol. 2803, pp. 456-469). doi:10.1007/978-3-540-45220-1_37
    Chapter. .

2002

  • Reus, B., & Streicher, T. (2002). Semantics and logic of object calculi. In Proceedings of the 17th Annual IEEE Symposium on Logic in Computer Science (pp. 113-122). IEEE Publications. doi:10.1109/LICS.2002.1029821
    Chapter. .
  • Cenciarelli, P., Knapp, A., Reus, B., & Wirsing, M. (1999). An Event-Based Structural Operational Semantics of Multi-threaded Java. In Lecture Notes in Computer Science (pp. 157-200). Springer Berlin Heidelberg. doi:10.1007/3-540-48737-9_5
    Chapter. .
  • Reus, B. (2002). Class-based versus object-based: A denotational comparison. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) Vol. 2422 (pp. 473-488). doi:10.1007/3-540-45719-4_32
    Conference publication. .
  • Reus, B. (2002). Class-based versus object-based: a denotational comparison. In Algebraic Methodology and Software Technology: Proceedings of the 9th International Conference, AMAST 2002, Saint-Gilles-les- Bains, Reunion Island, France (Vol. 2422, pp. 45-88). London, UK.: Springer-Verlag. doi:10.1007/3-540-45719-4
    Chapter. .

2001

  • Reus, B., Wirsing, M., & Hennicker, R. (2001). A Hoare Calculus for Verifying Java Realizations of OCL-Constrained Design Models. In Lecture Notes in Computer Science (pp. 300-317). Springer Berlin Heidelberg. doi:10.1007/3-540-45314-8_22
    Chapter. .
  • Berger, U., Niggl, K. H., & Reus, B. (2001). Theoretical computer science: Preface. Theoretical Computer Science, 264(2), 169. doi:10.1016/S0304-3975(00)00220-6
    Article. .
  • Reus, B., Wirsing, M., & Hennicker, R. (2001). A hoare calculus for verifying java realizations of OCL-constrained design models. In Unknown Book (Vol. 2029, pp. 300-317). doi:10.1007/3-540-45314-8_22
    Chapter. .
  • Reus, B., Wirsing, M., & Hennicker, R. (2001). A Hoare calculus for verifying Java realizations of OCL-constrained design models. In Proceedings in Fundamental Approaches to Software Engineering: 4th International Conference, FASE 2001, Genova, Italy (Vol. 2029, pp. 300-317). Springer Berlin / Heidelberg. doi:10.1007/3-540-45314-8
    Chapter. .

2000

  • Reus, B., & Hein, T. (2000). Towards a machine-checked java specification book. In Unknown Book (Vol. 1869, pp. 480-497). doi:10.1007/3-540-44659-1_30
    Chapter. .
  • Reus, B., & Hein, T. (2000). Towards a Machine-Checked Java Specification Book. In Lecture Notes in Computer Science (pp. 480-497). Springer Berlin Heidelberg. doi:10.1007/3-540-44659-1_30
    Chapter. .
  • Reus, B., & Hein, T. (2000). Towards a machine-checked Java specification book. In Theorem Proving in Higher Order Logics: Proceedings of the 13th International Conference, TPHOLs 2000 Portland, OR, USA (Vol. 1869, pp. 480-497). Springer-Verlag. doi:10.1007/3-540-44659-1
    Chapter. .

1999

  • Reus, B. (1999). Realizability models for type theories. In Electronic Notes in Theoretical Computer Science Vol. 23 (pp. 128-158). doi:10.1016/S1571-0661(04)00108-2
    Conference publication. .
  • Reus, B. (1999). Formalizing synthetic domain theory - the basic definitions. Journal of Automated Reasoning, 23(3-4), 411-444. doi:10.1023/A:1006258506401
    Article. .
  • Reus, B. (1999). Extensional S-spaces in type theory. Applied Categorical Structures, 7(1-2), 159-183.
    Article. .
  • Cenciarelli, P., Knapp, A., Reus, B., & Wirsing, M. (1999). An event-based structural operational semantics of multi-threaded java. In Unknown Book (Vol. 1523, pp. 157-200). doi:10.1007/3-540-48737-9_5
    Chapter. .
  • Reus, B. (1999). Extensional Σ-Spaces in Type Theory. Applied Categorical Structures, 7(1-2), 159-183. doi:10.1023/a:1008600521659
    Article. .
  • Altenkirch, T., & Reus, B. (1999). Monadic presentations of lambda terms using generalized inductive types. In Unknown Book (Vol. 1683, pp. 453-468). doi:10.1007/3-540-48168-0_32
    Chapter. .
  • Reus, B., & Streicher, T. (1999). General Synthetic Domain Theory - A Logical Approach.. Mathematical Structures in Computer Science, 9(2), 177-223. doi:10.1017/S096012959900273X
    Article. .
  • Altenkirch, T., & Reus, B. (1999). Monadic presentations of Lambda terms using generalized inductive types. In Computer Science Logic: Proceedings of the 13th International Workshop CSL '99, 8th Annual Conference of the EACSL, Madrid, Spain (Vol. 1863, pp. 453-468). Springer-Verlag. doi:10.1007/3-540-48168-0
    Chapter. .
  • Cenciarelli, P., Knapp, A., Reus, B., & Wirsing, M. (1999). An event-based structural operational semantics of multi-threaded Java. In Formal Syntax and Semantics of Java (Vol. 1523, pp. 157-200). Berlin, Germany: Springer-Verlag. doi:10.1007/3-540-48737-9
    Chapter. .

1998

  • Reus, B., Knapp, A., Cenciarelli, P., & Wirsing, M. (1998). Verifying a compiler optimization for multi-threaded java. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) Vol. 1376 (pp. 402-417). doi:10.1007/3-540-64299-4_47
    Conference publication. .
  • Streicher, T., & Reus, B. (1998). Classical logic, continuation semantics and abstract machines. Journal of Functional Programming, 8(6), 543-572. doi:10.1017/S0956796898003141
    Article. .

1997

  • Cenciarelli, P., Knapp, A., Reus, B., & Wirsing, M. (1997). From sequential to multi-threaded java: An event-based operational semantics. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) Vol. 1349 (pp. 75-90). doi:10.1007/bfb0000464
    Conference publication. .
  • Reus, B., & Streicher, T. (1997). General synthetic domain theory — a logical approach. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) Vol. 1290 (pp. 293-313). doi:10.1007/bfb0026995
    Conference publication. .

1996

  • Reus, B. (1996). Synthetic domain theory in type theory: Another logic of computable functions. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) Vol. 1125 (pp. 365-380). doi:10.1007/bfb0105416
    Conference publication. .

1993

  • Reus, B., & Streicher, T. (1993). Verifying properties of module construction in type theory. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) Vol. 711 LNCS (pp. 660-670). doi:10.1007/3-540-57182-5_57
    Conference publication. .

1992

  • Reus, B. (1992). Implementing higher-order functions in an algebraic specification language with narrowing. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) Vol. 631 LNCS (pp. 483-484). doi:10.1007/3-540-55844-6_160
    Conference publication. .