About
- since 2023: Senior software engineer at Arm
- 2021-2023: Head of competence field Safety and Security at fortiss
- 2019–2021: Scientist, competence field Safety and Security at fortiss
- 2015–2019: Senior Lecturer for Computer Science (Akademischer Oberrat), LMU München
- 04/2018–08/2018: Professor interim after Martin Hofmann's tragic accident, LMU München
- 04/2015: Habilitation in Computer Science, LMU München
- 04/2014–06/2014: Thematic Trimester Proofs and Types, Institut Henri Poincaré, Paris
- 02/2009–08/2009: Early Stage Fellowship, Institute of Advanced Studies, University of Bologna
- 2008–2015: Lecturer for Computer Science (Akademischer Rat), LMU München
- 2005–2008: Researcher, DFG project Pro.Platz, LMU München
- 2001–2005: Ph.D. at LFCS, University of Edinburgh. Supervisor: Ian Stark
- 2000–2001: M.Sc. at LFCS, University of Edinburgh. Supervisor: Alex Simpson
- 1996–2000: Informatics studies at Universität Leipzig
Publications, Slides and Drafts
- Specifying a Usage Control System
-
Ulrich Schöpp, Chuangjie Xu, Amjad Ibrahim, Fathiyeh Faghih, Theo Dimitrakos.
- In Symposium on Access Control Models and Technologies (SACMAT), Trento, Italy, 2023.
- A Toolchain for Synthesizing and Validating Safety Architectures
- Yuri Gil Dantas, Tiziano Munaro, Carmen Cârlan, Vivek Nigam, Simon Barner, Shiqing Fan, Alexander Pretschner, Ulrich Schöpp and Sergey Tverdyshev.
- In SN Computer Science, 2023, to appear.
- Automating Vehicle SOA Threat Analysis using a Model-Based Methodology
-
Yuri Gil Dantas, Vivek Nigam, Ulrich Schöpp, Simon Barner and Pei Ke.
- In International Conference on Information Systems Security and Privacy (ICISSP 2023), 2023.
- Safety-Aware Deployment Synthesis and Trade-Off Analysis of Apollo Autonomous Driving Platform
- Tarik Terzimehić, Simon Barner, Yuri Gil Dantas, Ulrich Schöpp, Vivek Nigam and Pei Ke.
- In International Workshop on Automotive System/Software Architectures (WASA) co-located with ICSA 2023, 2023.
- SeCloud: Computer-Aided Support for Selecting Security Measures for Cloud Architectures
-
Yuri Gil Dantas and Ulrich Schöpp.
- In International Conference on Information Systems Security and Privacy (ICISSP 2023), 2023.
- Inferring Region Types via an Abstract Notion of Environment Transformation
- With Chuangjie Xu.
- In Asian Symposium on Programming Languages and Systems (APLAS 2022), 2022.
- Special Issue of Mathematical Structures in Computer Science: In Homage to Martin Hofmann (Part 1)
- Co-Editor with Don Sannella and Jan Hoffmann.
- In Mathematical Structures in Computer Science, 2022.
- A Category Theoretic View of Contextual Types: from Simple Types to Dependent Types
- Jason Hu, Brigitte Pientka, and Ulrich Schöpp.
- In Transactions on Computational Logic, 2022.
- Using a Semantic Knowledge Base to Improve the Management of Security Reports in Industrial DevOps Projects
- Markus Voggenreiter and Ulrich Schöpp.
- In International Conference on Software Engineering: Software Engineering in Practice (ICSE-SEIP 2022), Pittsburgh, USA, 2022.
- A Model-based System Engineering Plugin for Safety Architecture Pattern Synthesis
- Yuri Gil Dantas, Tiziano Munaro, Carmen Cârlan, Vivek Nigam, Simon Barner, Shiqing Fan, Alexander Pretschner, Ulrich Schöpp, and Sergey Tverdyshev.
- In Model-Driven Engineering and Software Development (MODELSWARD 2022), 2022.
- A Generic Region Type System for Featherweight Java
- With Chuangjie Xu.
- In Formal Techniques for Java-like Programs, 2021.
- Type-based Enforcement of Infinitary Trace Properties for Java
- Serdar Erbatur, Ulrich Schöpp, and Chuangjie Xu.
- In Principles and Practice of Declarative Programming (PPDP 2021), 2021.
- Accountable Federated Machine Learning in Government: Engineering and Management Insights
- Dian Balta, Mahdi Sellami, Peter Kuhn, Ulrich Schöpp, Matthias Buchinger, Nathalie Baracaldo, Ali Anwar, Heiko Ludwig, Mathieu Sinn, Mark Purcell, Bashar Altakrouri.
- In Electronic Participation, 2021.
- Requirements-based Code Model Checking
- With Andreas Schweiger, Marina Reich, Tatiana Chuprina, Levi Lucio, and Hartmut Bruning.
- In Workshop on Formal Requirements (FORMREQ 2020), Zurich, 2020.
- Semantical Analysis of Contextual Types
- With Brigitte Pientka.
- In Foundations of Software Science and Computation Structures (FOSSACS20), Dublin, Ireland, 2020.
- The Geometry of Interaction as a Module System
- In Asian Symposium on Programming Languages and Systems (APLAS 2018), Wellington, New Zealand, 2018
- Slides from Shonan School Semantics of Effects, Resources, and Applications:
- Lecture 1, Lecture 2
- Defunctionalisation as Modular Closure Conversion
- prototype implementation
- In Principles and Practice of Declarative Programming (PPDP 2017), Namur, Belgium, 2017
- Computation-by-Interaction for Space-Bounded Functional Programming (preprint)
- With Ugo Dal Lago.
In Information and Computation, 2016 - From Call-by-Value to Interaction by Typed Closure Conversion
- In Asian Symposium on Programming Languages and Systems (APLAS 2015), 2015
- Computation-by-Interaction for Structuring Low-Level Computation
- Habilitation Thesis, 2015
- On the Relation of Interaction Semantics to Continuations and Defunctionalization
- (long version of TLCA 2013 paper)
- In Logical Methods in Computer Science, LMCS-10(4:10) 2014.
- Call by Value in a Basic Logic for Interaction
- In
Asian Symposium on Programming Languages and Systems (APLAS 2014), Singapore, 2014
Slides from talk at Workshop on Higher Order Computation: Types, Complexity, Applications - Organising Low-Level Programs using Higher Types
- In Principles and Practice of Declarative Programming (PPDP 2014), Canterbury, UK, 2014
- On Interaction, Continuations and Defunctionalization
- In Typed Lambda Calculi and Applications (TLCA 2013), Eindhoven, 2013, ©Springer-Verlag
- Pure Pointer Programs and Tree Isomorphism
- With Ramyaa and Martin Hofmann.
- In Foundations of Software Science and Computation Structures (FOSSACS13), Rome, 2013, ©Springer-Verlag
- Computation-by-Interaction with Effects
- In ASIAN Symposium on Programming Languages and Systems (APLAS 2011), Taiwan, 2011, ©Springer-Verlag
- Type Inference for Sublinear Space Functional Programming
- With Ugo Dal Lago.
- Revised version appears in ASIAN Symposium on Programming Languages and Systems (APLAS 2010), Shanghai, China, 2010.
- Last revision: 17.06.2010
- Functional Programming in Sublinear Space
- With Ugo Dal Lago.
- Last revision: 18.03.2010; This version corrects a few typographical errors. The original paper is available at www.springerlink.com.
- In European Symposium on Programming (ESOP2010), Zypern, 2010, LNCS 6012, ©Springer-Verlag
- Slides: OASIS Seminar, Oxford University (December 2009)
- Pointer Programs and Undirected Reachability
- With Martin Hofmann.
- In Logic in Computer Science (LICS09), Los Angeles, USA, ©IEEE
- Slides: LICS09 (August 2009)
- Pointer Programs and Undirected Reachability (long version)
- With Martin Hofmann.
- Electronic Colloquium on Computational Complexity (ECCC)
- ECCC Technical Report TR08-090
- (last revision: 16 January 2009)
- Pure Pointer Programs with Iteration (long version)
- With Martin Hofmann.
- In Transactions on Computational Logic (ToCL), 2009
- A Formalised Lower Bound on Undirected Graph Reachability
- In LPAR 2008, Doha, Katar, ©Springer-Verlag
- Formalisation in Coq
Browse the formalisation:
Summary of Main Results, JAGs and Reachability, General Index.Download the formalisation sources:
reach1.1.zip (17 June 2008)
These files can be checked in Coq 8.1 with the tactic language extension SSReflect 1.1. A distribution of SSReflect 1.1 along with installation instructions can be obtained from the Mathematical Components Project.
- Pure Pointer Programs with Iteration
- With Martin Hofmann.
- In Computer Science Logic (CSL08), Bertinoro, Italy
- LNCS 5213, 2008, ©Springer-Verlag
- Stratified Bounded Affine Logic for Logarithmic Space
- In Logic in Computer Science (LICS07), Wroclaw, Poland, ©IEEE
- Draft long version, comments welcome!
- Slides: LICS07 (July 2007)
- Space-efficient Computation by Interaction – A Type System for Logarithmic Space
- In Computer Science Logic (CSL06), Szeged, Hungary
- LNCS 4207, 2006, ©Springer-Verlag
- Slides: CSL06 (September 2006)
- Modelling Generic Judgements
- In International Workshop on Logical Frameworks and Meta-Languages: Theory and Practice (LFMTP06), Seattle, USA, 2006, ENTCS 174(5), 2007
- Slides: LFMTP06 (August 2006)
- Names and Binding in Type Theory
- PhD Thesis, The University of Edinburgh, 2006
- Slides: ICMS07 (May 2007)
- A Dependent Type Theory with Names and Binding
- With Ian Stark.
- In Computer Science Logic (CSL04), Karpacz, Poland
- LNCS, 3210, pages 235–249, 2004
- Slides: CSL04 (September 2004), Logic and Semantics Club at LFCS (August 2004)
- Verifying Temporal Properties using Explicit Approximants: Completeness for Context-free Processes. (Older version with outline proofs)
- With Alex Simpson.
- In Proceedings of Foundations of Software Science and Computation Structures (FOSSACS02), Grenoble, France
- LNCS, 2303, pages 372–386, 2002, ©Springer-Verlag
- Slides: FoSSaCS02 (April 2002), Logic and Semantics Club at LFCS (February 2002)
- Formal Verification of Processes
- MSc thesis, The University of Edinburgh, 2001
Software
Events
- PPDP 2021: Principles and Practice of Declarative Programming (PC member)
- PPDP 2020: Principles and Practice of Declarative Programming (PC member)
- LFMTP 2020: Logical Frameworks and Meta-Languages: Theory and Practice (PC member)
- WPTE 2020: Rewriting Techniques for Program Transformations and Evaluation (PC member)
- Martin Hofmann Memorial Meeting, 13 July 2019, (co-organiser)
- WPTE 2019: Rewriting Techniques for Program Transformations and Evaluation (PC member)
- LOLA 2019: Syntax and Semantics of Low-Level Languages (PC member)
- APLAS 2018: Asian Symposium on Programming Languages and Systems (contributed talk)
- GaLoP 2018: Games for Logic and Programming Languages (invited speaker)
- LCC 2018: Logic and Computational Complexity (PC member)
- PPDP 2017: Principles and Practice of Declarative Programming (PC member)
- Shonan school on "Semantics of Effects, Resources, and Applications"
- APLAS 2016: Asian Symposium on Programming Languages and Systems (PC member)
- LOLA 2015: Syntax and Semantics of Low-Level Languages (PC co-chair)
- MFPS 2015: Mathematical Foundations of Programming Semantics XXXI (PC member)
- GaLoP 2015: Games for Logic and Programming Languages (PC member)
- TYPES 2015: Types for Proofs and Programs (PC member)
- FOSSACS 2015: Foundations of Software Science and Computation Structures (PC member)
- DICE 2014: Developments in Implicit Computational Complexity (PC chair)
- APLAS 2013: Asian Symposium on Programming Languages and Systems (PC member)
- FOPARA 2013: Foundational and Practical Aspects of Resource Analysis (PC member)
- LOLA 2012: Syntax and Semantics of Low Level Languages (PC member)
- LCC 2012: Logic and Computational Complexity (PC member)
- DICE 2012: Developments in Implicit Computational Complexity (PC member)
- MSFP 2012: Mathematically Structured Functional Programming (PC member)
- SOFSEM 2012: International Conference on Current Trends in Theory and Practice of Computer Science (PC member)
- LOLA 2010: Syntax and Semantics of Low Level Languages (PC member)
Teaching
I taught the following courses at Ludwig-Maximilians-Universität München.
- WS21/22: Seminar und Praktikum Wissenschaftliches Arbeiten und Lehren
- SS21: Seminar Software Security
- SS20: Seminar Software Security
- WS18/19: Praktikum Compilerbau
- WS18/19: Vorlesung Grundlagen der Analysis
- SS18: Vorlesung Typsysteme
- SS18: Seminar Algorithmen und Datenstrukturen
- WS17/18: Praktikum Compilerbau
- WS17/18: Übungen zu Grundlagen der Analysis
- SS17: Übungen zu Cryptography
- WS16/17: Softwareentwicklungspraktikum Nebenfach (with Stephan Barth und Steffen Jost)
- WS16/17: Statische Programmanalyse (with Steffen Jost)
- SS16: Vorlesung und Übung: Formale Spezifikation und Verifikation
- WS15/16: Softwareentwicklungspraktikum Nebenfach (with Stephan Barth)
- WS15/16: Übungen zu Komplexitätstheorie
- SS15: Übungen zu Formale Spezifikation und Verifikation
- WS14/15: Praktikum Compilerbau
- SS14: Übungen zu Formale Spezifikation und Verifikation
- WS13/14: Softwareentwicklungspraktikum (with Steffen Jost)
- SS13: Praktikum Compilerbau (with Andreas Abel)
- SS12: Vorlesung Protokollsicherheit (with Vivek Nigam)
- SS12: Übungen zu Formale Sprachen und Komplexität
- WS11/12: Praktikum Compilerbau (with Andreas Abel)
- WS11/12: Übungen zu Automatentheorie
- SS11: Vorlesung Typsysteme (with Andreas Abel)
- SS11: Übungen zu Formale Sprachen und Komplexität
- WS10/11: Einführung in die Informatik: Programmierung und Softwareentwicklung
- SS10: Semantik von Programmiersprachen (with Andreas Abel)
- WS09/10: Praktikum Compilerbau (with Robert Grabowski)
- WS09/10: Übungen zu Spezifikation und Verifikation
- WS08/09: Softwareentwicklungspraktikum (with Martin Lange)