Bernhard Reus
About me
Publications
Research Students
Projects
Teaching
Roles
Contact
The app
The textbook
The prover
The me
Designed by Lazarus Lazaridis

About me


Head of the Foundations of Software Systems (FoSS) research group
University profile


My research interests lie in the following areas:

I am happy to supervise any talented PhD student at the University of Sussex (Brighton is also an excellent place to live). We sometimes offer scholarships to exceptional students. Appropriate candidates are invited to contact me but need to officially apply here.

PC chair and organiser of the British Logic Colloquium 2017

Publications
Public research profiles: Sussex Repository, DBLP

  • Fuhrmann S, Reus B, Frey O, Pera A, Picker L, Kern F: Marked skewing of entire T-cell memory compartment occurs only in a minority of CMV infected individuals and is unrelated to the degree of memory subset skewing among CMV specific T-cells. Frontiers in Immunology 14:1258339, 2023.
  • Knapp A., Mühlberger H., Reus B.: Interpreting Knowledge-based Programs, ESOP 23, LNCS 13990, pp.253-280, 2023.
  • Reus B, Caserta S, Larsen M, Morrow G, Bano A, Hallensleben M, Rajkumar C, Pera A, Kern F: In-depth profiling of T-cell responsiveness to commonly recognized CMV antigens in older people reveals important sex differences, Frontiers in Immunology, 12, 2021.
  • Kirkham, Frances, Pera, Alejandra, Simanek, Amanda M, Bano, Aalia, Morrow, George, Reus, Bernhard, Caserta, Stefano, Smith, Helen E, Davies, Kevin A, Rajkumar, Chakravarthi and Kern, Florian: 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, 2021.
  • Klimis, Vasileios, Parisis, Georgei and Reus, Bernhard: Model checking software-defined networks with flow entries that time outi. Formal Methods in Computer-Aided Design (FMCAD 2020), Online, Sep. 21 - 24, 2020. Published in: Proceedings of the 20th Conference on Formal Methods in Computer-Aided Design – FMCAD 2020. 1 179-184. IEEE digital library, Wien.(2020)
  • Klimis, Vassilis, Parisis, Georgei and Reus, Bernhard: Towards model checking real-world software-defined networks. 32nd International Conference on Computer-Aided Verification, Los Angeles, California, USA, July 19-24, 2020. Published in: Computer Aided Verification. CAV 2020. Lecture Notes in Computer Science. 12225 126-148. Springer Verlag (2020).
  • Pera Rojas, Alejandra, Caserta, Stefano, Albanese, Fabio, Blowers, Pinar, Morrow, George, Terrazzini, Nadia, Smith, Helen E, Rajkumar, Chakravarthi, Reus, Bernhard, Msonda, James R, Verboom, Murielle, Hallenensleben, Michael, Blasczyk, Rainer, Davies, Kevin A and Kern, Florian: CD28null pro-atherogenic CD4 T-cells explain the link between CMV infection and an increased risk of cardiovascular death. Theranostics, 8 (16). pp. 4509-4519. (2018)
  • B. Reus: Limits of Computation. Undergraduate Textbooks in Computer Science Series. Springer. 2016
  • B. Reus, N.A. Charlton, B. Horsfall: Symbolic execution proofs for higher order store programs. Journal of Automated Reasoning 54.3: 199-284, 2015.
  • J. Schwinghammer, L. Birkedal, F. Pottier, B. Reus, K. Stovring, H. Yang: A step-indexed Kripke model of hidden state. Mathematical Structures in Computer Science 23(1): 1-54, Cambridge University Press, 2013.
  • N.A. Charlton, B. Reus: Specification patterns for reasoning about recursion through the store. Information and Computation, 231:167-203, Elsevier, 2013.
  • B. Horsfall, N.A. Charlton, B. Reus: Verifying the reflective visitor pattern. In Proc. of the 14th Workshop on Formal Techniques for Java-like Programs, pp. 27-34, ACM Digital Library, 2012.
  • B. Reus, Th. Streicher: A Synthetic Theory of Sequential Domains. Ann. Pure Appl. Logic 163(8): 1062-1074, 2012.
  • N.A. Charlton, B. Horsfall, B. Reus: Crowfoot: A Verifier for Higher-Order Store Programs. VMCAI 2012, LNCS 7148, pp. 136-151, 2012.
  • B. Reus, Th. Streicher: Relative Completeness for Logics of Functional Programs. CSL 2011, pp. 470-480, 2011.
  • N.A. Charlton, B.Horsfall, B. Reus: Formal Reasoning about Runtime Code Update. In S.Abiteboul, K.Böhm, C. Koch, K.-L.~Tan (eds.): Int. Conf. on Data Engineering, ICDE, Hot Topics in Software Upgrades (HotSWUp), pp. 134-138. IEEE, 2011.
  • J. Schwinghammer, L. Birkedal, B. Reus, H. Yang: Nested Hoare Triples and Frame Rules for Higher-order Store. Logical Methods in Computer Science 7(3), 2011.
  • N.A. Charlton, B. Reus: Specification Patterns and Proofs for Recursion through the Store, FCT 2011, LNCS 6914, pp 310-321, 2011.
  • L. Birkedal, B. Reus, J. Schwinghammer, Kristian Stovring, Jacob Thamsborg, and H. Yang: Step-Indexed Kripke Models over Recursive Worlds. POPL 2011, ACM pp. 119-132, 2011.
  • N. Charlton, B. Reus: A deeper understanding of the deep frame axiom (extended abstract), 9 pages, presented at Workshop LoLA'10, Edinburgh, 2010.
  • B. Reus, A. Jung, K. Keimel, Th. Streicher (eds.): Special Issue on Domains, MSCS 20(2), 2010.
  • J. Schwinghammer, H. Yang, L. Birkedal, F. Pottier, A semantic foundation for hidden state, Fossacs, LNCS 6014, pp.2-17, 2010.
  • N. Charlton, B. Reus: A decidable class of verification conditions for programs with higher order store, AVOCS 09, Electronic Communications of the Association of Software Science and Technology (EASST) 23, 2010. Also in University of Swansea, Technical Report CSR-2-2009.
  • J. Schwinghammer, L. Birkedal, B. Reus, H. Yang: Nested Hoare Triples and Frame Rules for Higher-Order Store, CSL 09, LNCS 5771, pp.440-454, 2009.
  • L.Birkedal, B.Reus, J.Schwinghammer, H.Yang: A Simple Model of Separation Logic for Higher-order Store, ICALP (II), LNCS 5126, pp. 348-360, 2008.
  • B.Reus, J. Schwinghammer: Separation Logic for Higher-Order Store, CSL '06, LNCS 4207, pp. 575-590, Springer-Verlag, Berlin, 2006.
  • B.Reus, J. Schwinghammer: Denotational Semantics for Program Logic of Objects MSCS, vol.16:313-358. Cambridge University, 2006.
  • D. Pattinson, B.Reus : A Complete Temporal And Spatial Logic For Distributed Systems. FroCos 05, LNAI 3717, pp.122-137, Springer Berlin, 2005.
  • B.Reus, Th. Streicher: About Hoare Logic for Higher-Order Store. ICALP 05, LNCS 3580, pp.1337-1348, 2005.
  • B.Reus, J. Schwinghammer: Denotational Semantics for Abadi and Leino's Logic of Objects. ETAPS 05, LNCS 3444, pp. 263-178, Springer Berlin, 2005.
  • B.Reus, Th. Streicher: Semantics and logics of object calculi. TCS(316):191-213, 2004.
  • B.Reus: Modular Semantics and Logics of Classes. CSL'03. LNCS 2803, pp.456-469, Springer Verlag, Berlin, 2003.
  • B. Reus: Class-based versus Object-based: A Denotational Comparison. AMAST '02. LNCS 2422, pp. 473-488, Springer Verlag, Berlin, 2002.
  • B. Reus, Th. Streicher: Semantics and Logics of Objects. LICS '02, Copenhagen. (version 24/09/02 including some corrections). IEEE Press 2002.
  • U. Berger, K-H. Niggl, B. Reus (guest editors) Theoretical Computer Science Vol. 264(2), Workshop On Domains III (Selected Papers), 2001.
  • B. Reus, M. Wirsing, R. Hennicker: A Hoare Calculus for Verifying Java Realizations of OCL-Constrained Design Model. FASE'01, ETAPS, Genova, LNCS 2029, pp. 300-316, Springer Berlin, 2001.
  • B. Reus, T. Hein: Towards a Machine-Checked Java Specification Book. Theorem Proving in Higher Order Logics: TPHOLs 2000, LNCS 1869, p.479-496, Springer Berlin 2000.
  • Th. Altenkirch, B. Reus: Monadic presentations of lambda terms using generalized inductive types. CSL'99. LNCS Springer Berlin, 1999.
  • Th. Altenkirch, W. Naraschewski, B. Reus (Eds.): Types for Proofs and Programs. Proceedings of the Types Working Group Meeting at Kloster Irsee, 1998. LNCS 1657, Springer, Berlin, 1999.
  • B. Reus: Formalizing a variant of Synthetic Domain Theory. Journ. of Automated Reasoning 23(3):411-444, 1999.
  • P. Cenciarelli, A. Knapp, B. Reus, M. Wirsing : An Event-Based Structual Operational Semantcis of Multi-Threaded Java: , In Jim Alves-Foss (Ed.) Formal Syntax and Semantics Of Java, LNCS 1523, pp. 157-200, Springer, Berlin, 1999.
  • B. Reus: Extensional Sigma-Spaces in Type Theory. Journal of Applied Categorical Structures 7(1):159-183, Kluwer Academic Publishers, 1999.
  • B. Reus, Th. Streicher: General Synthetic Domain Theory - A Logical Approach. MSCS 9:177--223. Cambridge University Press, 1999.
  • Th. Streicher, B. Reus: Classical logic: Continuation Semantics and Abstract Machines. Journal of Functional Programming. Vol 8(6):543-572, 1998. This is the original extended version also containing cbv, not the Journal version
  • P. Cenciarelli, A. Knapp, B. Reus, M. Wirsing : From Sequential To Multi-Threaded Java: An Event-Based Operational Semantics, AMAST'97, LNCS 1349, pp. 402-417, Springer Berlin, 1997.
  • B. Reus, A. Knapp, P. Cenciarelli, M. Wirsing : Verifying a Compiler Optimization for Multi-Threaded Java, WADT Workshop 97, LNCS 1376, Springer, Berlin, 1998
  • U. Berger, K.-H. Niggl, B. Reus (eds.): Workshop Domains III (Proceedings), Technical Report 9712, Ludwig-Maximilians-Universität, München, 1997.
  • B. Reus, T. Streicher : General Synthetic Domain Theory -- A Logical Approach (extended abstract), CTCS'97, Santa Margherita, Italy. LNCS 1290, pp. 293-313, Springer, Berlin, 1997.
  • B. Reus: Synthetic Domain Theory in Type Theory : Another Logic of Computable Functions, TPHOL 96, Turku, 1996, LNCS 1125, Springer Verlag, 1996.
  • B. Reus: Program Verification in Synthetic Domain Theory. Thesis, November 1995. Shaker Verlag Aachen, 1996.
  • Y. Lafont, B. Reus, T. Streicher: Continuations Semantics or Expressing Implication by Negation. Technical Report 9321, Ludwig-Maximilians-Universität, München, 1993. Since there have been some requests for this here is a PS version.
  • B. Reus, T. Streicher: Naive Synthetic Domain Theory - A Logical Approach. Unpublished internal report, Universität München, 1993. It is the precursor of the MSCS journal paper.
  • B. Reus, Th. Streicher: Verifying Properties of Module Construction in Type Theory. In A.M.Borzyszkowski, S.Sokolowski (eds.) MFCS'93, Springer Verlag, LNCS 711, Berlin, September 1993. See also Lifting the laws of module algebra to deliverables. Technical Report 9203, Ludwig-Maximilians-Universität, München, August 1992.

    • Research Students

    Projects

    • at Sussex (PI)
    • at LMU (member)
      • SENSORIA (EU IST project, Software Engineering for Service-Oented Overlay Computers), Associated member 2008.
      • HCM project MeDiCiS (Methodologies for the Development of Computer System Specifications)
      • DAAD-project Vigoni, with the University of Genoa (Italy) about Synthetic Domain Theory
      • DAAD-project Vigoni, with the University of Rome (Italy) about Denotational Semantics of Object-Oriented Languages
    • Events organised
      • Annual Meeting of the British Logic Colloquium 2017.
      • Domains IX Int. Conference, 22-24 September 2008, Sussex University
      • Spring School Categorical Methods in Logic and Comp.Sci., Munich '99
      • Types Working Group Meeting 1998, Kloster Irsee
      • Workshop Domains III-97, LMU Munich
      • Type-Club with Thorsten Altenkirch in Munich

    Teaching

    Roles

    Contact

    Location: CHICHESTER 2 2R307
    Email: bernhard@sussex.ac.uk
    University Profile: http://www.sussex.ac.uk/profiles/115097
    Telephone numbers
    Internal: 7477
    UK: 01273 877477
    International: +44 1273 877477
    Download vCard
    Download vCard to your mobile