Foundations of Software Systems (FoSS)

Martin Berger

Selected Publications

2024

  • Panayi, L., Gandhi, R., Whittaker, J., Chouliaras, V., Berger, M., & Kelly, P. (2024). Improving Memory Dependence Prediction with Static Analysis. Retrieved from http://arxiv.org/abs/2403.08056v3
    Preprint.
  • Valizadeh, M., Fijalkow, N., & Berger, M. (2024). LTL learning on GPUs. Retrieved from http://arxiv.org/abs/2402.12373v2
    Preprint.
  • Valizadeh, M., Fijalkow, N., & Berger, M. (2024). LTL Learning on GPUs. In Unknown Book (Vol. 14683 LNCS, pp. 209-231). doi:10.1007/978-3-031-65633-0_10
    Chapter. View online.
  • Panayi, L., Gandhi, R., Whittaker, J., Chouliaras, V., Berger, M., & Kelly, P. (2024). Improving Memory Dependence Prediction with Static Analysis. In Unknown Book (Vol. 14842 LNCS, pp. 301-315). doi:10.1007/978-3-031-66146-4_20
    Chapter. View online.
  • Valizadeh, M., Gorinski, P. J., Iacobacci, I., & Berger, M. (2024). Correct and Optimal: the Regular Expression Inference Challenge. In IJCAI International Joint Conference on Artificial Intelligence (pp. 6486-6494).
    Conference publication.

2023

  • Naseredini, S. A. H., Berger, M., Sammartino, M., & Xiong, S. (2023). ALARM: Active LeArning of Rowhammer Mitigations. In Proceedings of the 11th International Workshop on Hardware and Architectural Support for Security and Privacy (pp. 1-9). Chicago IL USA: ACM. doi:10.1145/3569562.3569563
    Conference publication. View on figshare.
  • Valizadeh, M., & Berger, M. (2023). Search-based regular expression inference on a GPU. In Proceedings of the ACM on Programming Languages Vol. 7 (pp. 1317-1339). Orlando, Florida, United States: Association for Computing Machinery (ACM). doi:10.1145/3591274
    Conference publication. View on figshare.
  • Valizadeh, M., & Berger, M. (2023). Search-Based Regular Expression Inference on a GPU. Retrieved from http://dx.doi.org/10.1145/3591274
    Preprint.
  • Berger, M., & Mulligan, D. P. (2023). A modest proposal: explicit support for foundational pluralism. Retrieved from http://arxiv.org/abs/2302.10137v1
    Preprint.

2022

  • Naseredini, A., Berger, M., Sammartino, M., & Xiong, S. (2022). ALARM: Active LeArning of Rowhammer Mitigations. Retrieved from http://arxiv.org/abs/2211.16942v1
    Preprint.
  • Eliott, H. P. G., & Berger, M. (2022). A program logic for fresh name generation. Science of Computer Programming, 223, pages. doi:10.1016/j.scico.2022.102860
    Article. View on figshare.
  • Eliott, H. P. G. (2022). A program logic for fresh name generation.
    Thesis. View on figshare.
  • Naseredini, S. A. H., Gast, S., Schwarzl, M., Bernardo, P., Smajic, A., Canella, C., . . . Gruss, D. (2022). Systematic analysis of programming languages and their execution environments for spectre attacks. In Proceedings of the 8th International Conference on Information Systems Security and Privacy (pp. 48-59). Online: SCITEPRESS - Science and Technology Publications. doi:10.5220/0010779300003120
    Conference publication. View on figshare.

2021

  • Naseredini, A., Gast, S., Schwarzl, M., Bernardo, P. M. S., Smajic, A., Canella, C., . . . Gruss, D. (2021). Systematic Analysis of Programming Languages and Their Execution Environments for Spectre Attacks. Retrieved from http://arxiv.org/abs/2111.12528v1
    Preprint.
  • Eliott, H. P. G., & Berger, M. (2021). A program logic for fresh name generation. In Fundamentals of Software Engineering Vol. 12818 (pp. 76-91). Tehran, Iran: Springer. doi:10.1007/978-3-030-89247-0_6
    Conference publication. View on figshare.
  • Eliott, H. P., & Berger, M. (2021). A program logic for fresh name generation. Retrieved from http://arxiv.org/abs/2101.10720v2
    Preprint.

2020

  • Jeffery, A., & Berger, M. (n.d.). Asynchronous sessions with implicit functions and messages. Science of Computer Programming, pages. doi:10.1016/j.scico.2019.05.004
    Article. View on figshare.
  • Evans, R., & Berger, M. (2020). Cathoristic Logic: A Logic for Capturing Inferences Between Atomic Sentences. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 12065 LNCS, pp. 17-85). doi:10.1007/978-3-030-41103-9_2
    Chapter. View online.

2018

  • Jeffery, A., & Berger, M. (2018, August 29). Asynchronous sessions with implicit functions and messages. In 2018 International Symposium on Theoretical Aspects of Software Engineering (TASE) (pp. pages). Guangzhou, China: Institute of Electrical and Electronics Engineers. doi:10.1109/TASE.2018.00010
    Conference publication. View on figshare.

2017

  • Berger, M., Tratt, L., & Urban, C. (2017). Modelling homogeneous generative meta-programming. In Proceedings 31st European Conference on Object-Oriented Programming Vol. 74 (pp. 5:1-5:23). Germany: Schloss Dagstuhl. doi:10.4230/LIPIcs.ECOOP.2017.0
    Conference publication. View on figshare.
  • Berger, M., Tratt, L., & Urban, C. (2017). Modelling homogeneous generative meta-programming. In Leibniz International Proceedings in Informatics, LIPIcs Vol. 74 (pp. 51-523). doi:10.4230/LIPIcs.ECOOP.2017.5
    Conference publication. View online.

2016

  • Berger, M., Tratt, L., & Urban, C. (2016). Modelling homogeneous generative meta-programming. Retrieved from http://arxiv.org/abs/1602.06568v2
    Preprint.

2015

  • Berger, M., & Tratt, L. (2015). Program logics for homogeneous generative run-time meta-programming. Logical Methods in Computer Science, 11(1), pages. doi:10.2168/LMCS-11(1:5)2015
    Article. View on figshare.

2014

  • Evans, R. P., & Berger, M. (2014). Cathoristic logic: A modal logic of incompatible propositions. Retrieved from http://arxiv.org/abs/1411.7158v1
    Preprint.
  • Berger, M., & Tratt, L. (2014). Program Logics for Homogeneous Generative Run-Time Meta-Programming. doi:10.48550/arxiv.1411.4256
    Preprint. View online.
  • Honda, K., Yoshida, N., & Berger, M. (2014). Process types as a descriptive tool for interaction. In Rewriting and Typed Lambda Calculi. RTA 2014 (pp. 1-20). Vienna, Austria: Springer. doi:10.1007/978-3-319-08918-8_1
    Conference publication. View on figshare.
  • Honda, K., Yoshida, N., & Berger, M. (2014). An observationally complete program logic for imperative higher-order functions. Theoretical Computer Science, 517, 75-101. doi:10.1016/j.tcs.2013.11.003
    Article. View on figshare.

2012

  • Berger, M. (2012). Specification and verification of meta-programs. In Conference Record of the Annual ACM Symposium on Principles of Programming Languages (pp. 3). doi:10.1145/2103746.2103750
    Conference publication. View online.

2010

  • Berger, M., & Tratt, L. (2010). Program logics for homogeneous meta-programming. In Logic for Programming, Artificial Intelligence, and Reasoning (Vol. 6355 L, pp. 64-81). Springer Verlag. doi:10.1007/978-3-642-17511-4_5
    Chapter. View on figshare.
  • Berger, M. (2010). Program logics for sequential higher-order control. In Fundamentals of software engineering: Third IPM International Conference, FSEN 2009, Kish Island, Iran, April 15-17, 2009, Revised Selected Papers (Vol. 5961, pp. 194-211). Berlin: Springer Verlag. doi:10.1007/978-3-642-11623-0_11
    Chapter. View on figshare.

2008

  • Yoshida, N., Honda, K., & Berger, M. (2008). Logical Reasoning for Higher-Order Functions with Local State. Logical Methods in Computer Science, 4(4), 1-68. doi:10.2168/LMCS-4(4:2)2008
    Article. View on figshare.
  • Berger, M., Honda, K., & Yoshida, N. (2008). Completeness and logical full abstraction in modal logics for typed mobile processes. In Automata, Languages and Programming (Vol. 5126, pp. 99-111). Springer Verlag.
    Chapter. View on figshare.

2007

  • Yoshida, N., Honda, K., & Berger, M. (2007). Linearity and bisimulation. Journal of Logic and Algebraic Programming, 72(2), 207-238. doi:10.1016/j.jlap.2007.02.011
    Article. View online.
  • Berger, M., Honda, K., & Yqshida, N. (2007). A logical analysis of aliasing in imperative higher-order functions. In Journal of Functional Programming Vol. 17 (pp. 473-546). doi:10.1017/S0956796807006417
    Conference publication. View online.
  • Berger, M., & Yoshida, N. (2007). Timed, distributed, probabilistic, typed processes. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) Vol. 4807 LNCS (pp. 158-174). doi:10.1007/978-3-540-76637-7_11
    Conference publication. View online.
  • Yoshida, N., Honda, K., & Berger, M. (2007). Logical reasoning for higher-order functions with local state. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) Vol. 4423 LNCS (pp. 361-377). doi:10.1007/978-3-540-71389-0_26
    Conference publication. View online.

2006

  • Honda, K., Berger, M., & Yoshida, N. (2006). Descriptive and relative completeness of logics for higher-order functions. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) Vol. 4052 LNCS (pp. 360-371). doi:10.1007/11787006_31
    Conference publication. View online.

2005

  • Berger, M., Honda, K., & Yoshida, N. (2005). A logical analysis of aliasing in imperative higher-order functions. In Proceedings of the ACM SIGPLAN International Conference on Functional Programming, ICFP (pp. 280-293). doi:10.1145/1086365.1086401
    Conference publication. View online.
  • Berger, M., Honda, K., & Yoshida, N. (2005). A logical analysis of aliasing in imperative higher-order functions. ACM SIGPLAN Notices, 40(9), 280-293. doi:10.1145/1090189.1086401
    Article. View online.
  • Berger, M., Honda, K., & Yoshida, N. (2005). Genericity and the π-calculus. Acta Informatica, 42(2-3), 83-141. doi:10.1007/s00236-005-0175-1
    Article. View online.
  • Honda, K., Yoshida, N., & Berger, M. (2005). An observationally complete program logic for imperative higher-order functions. In Proceedings - Symposium on Logic in Computer Science (pp. 270-279). doi:10.1109/LICS.2005.5
    Conference publication. View online.

2004

  • Yoshida, N., Berger, M., & Honda, K. (2004). Strong normalisation in the π-calculus. Information and Computation, 191(2), 145-202. doi:10.1016/j.ic.2003.08.004
    Article. View online.
  • Berger, M. (2004). Basic theory of reduction congruence for two timed asynchronous π-calculi. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), 3170, 115-130. doi:10.1007/978-3-540-28644-8_8
    Article. View online.

2003

  • Berger, M., & Honda, K. (2003). The two-phase commitment protocol in an extended π-calculus. In Electronic Notes in Theoretical Computer Science Vol. 39 (pp. 21-46). doi:10.1016/S1571-0661(05)82502-2
    Conference publication. View online.
  • Berger, M., Honda, K., & Yoshida, N. (2003). Genericity and the π-calculus. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), 2620, 103-119. doi:10.1007/3-540-36576-1_7
    Article. View online.

2002

  • Yoshida, N., Honda, K., & Berger, M. (2002). Linearity and bisimulation. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) Vol. 2303 (pp. 417-433). doi:10.1007/3-540-45931-6_29
    Conference publication. View online.

2001

  • Yoshida, N., Berger, M., & Honda, K. (2001). Strong normalisation in the π-calculus. In Proceedings - Symposium on Logic in Computer Science (pp. 311-322).
    Conference publication.
  • Berger, M., Honda, K., & Yoshida, N. (2001). Sequentiality and the π-calculus. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) Vol. 2044 LNCS (pp. 29-45). doi:10.1007/3-540-45413-6_7
    Conference publication. View online.