Curriculum Vitae

This is the professional curriculum vitae of Prof. Gerald Lüttgen. Information on his former and current teaching activities and on his paper and invited presentations can be found elsewhere.

Education

• May 1998: Doctoral Degree in Natural Sciences (Dr. rer. nat.), Department of Mathematics and Computer Science, University of Passau, Germany. Dissertation: Pre-emptive Modeling of Concurrent and Distributed Systems. Advisors: Prof. Bernhard Steffen and Prof. Rance Cleaveland.
• July 1994: Advanced Degree in Computer Science (Diplom-Informatiker), Department of Computer Science, RWTH Aachen University, Germany. Thesis: Kompositionelle Minimierung Endlicher Verteilter Systeme (Compositional Minimisation of Finite-state Distributed Systems). Advisor: Prof. Bernhard Steffen.

Positions

• April 2009 - present:
  • Full Professor, Faculty of Information Systems and Applied Computer Sciences, University of Bamberg, Germany
  • Head of the Software Technologies Research Group (Chair of Software Engineering and Programming Languages; Lehrstuhlinhaber)
  • Dean of the Faculty of Information Systems and Applied Computer Sciences (Dekan, between October 2013 and September 2015)
  • Member of the Standing PhD Committee (between October 2013 and September 2015)
  • "Modern Languages Teaching Centre" Liaison Officer (between April 2016 and September 2018)
  • "Fakultätentag Informatik" Liaison Officer (since October 2012)
  • Course Organiser of the BSc Software Systems Science degree programme (since April 2012)
  • Member of the Examination Board "Applied Computer Science & Software Systems Science" (since October 2011)
  • Member of the Fakultätsrat (Faculty Board, between October 2009 and September 2017)
  • Member of three Hiring Panels (Berufungskommissionen, between 2011 and 2014, Chair of one of them)
  • Instructor of the modules Applied Software Verification, Foundations of Software Analysis, Foundations of Software Engineering and Principles of Compiler Construction, amongst others
  • Supervisor of Post Docs, PhD students, BSc/MSc students and teaching/research assistants
• October 2008 - March 2009:
  • Reader, Department of Computer Science, University of York, UK
  • Member of the High Integrity Systems Engineering research group (between May 2006 and March 2009) and the Programming Languages and Systems research group (bewtween January 2003 and March 2009)
  • Director of the LSCITS EngD Centre (between April 2008 and March 2009); Co-PI of the UK Research and Training Initiative in Large Scale Complex IT Systems (LSCITS)
  • Instructor of the postgraduate-level module Reactive Systems Design (Spring 2007-2009)
  • Supervisor of Post Docs, PhD students and BSc/MSc students
• January 2003 - September 2008:
  • Senior Lecturer, Department of Computer Science, University of York, UK
  • Member of the High Integrity Systems Engineering research group (between May 2006 and March 2009) and the Programming Languages and Systems research group (between January 2003 and March 2009)
  • Lead Developer of the LSCITS Engineering Doctorate (EngD) Programme (since February 2007) and Director of the LSCITS EngD Centre (between April 2008 and March 2009); Co-PI of the UK Research and Training Initiative in Large Scale Complex IT Systems (LSCITS) (between February 2007 and March 2009)
  • MSc Software Engineering (MScSWE) Course Organiser between January 2005 and August 2007; MScSWE Staff Representative between October 2003 and December 2004; Member of the Masters' Teaching Committee between October 2003 and August 2007
  • Staff Handbook Editor between July 2003 and August 2006; Member of the Departmental Information Committee between August 2003 and August 2005
  • Graduate Studies Publicity Coordinator and Member of the Departmental Graduate Studies Committee between January 2004 and August 2005
  • Instructor of the undergraduate-level module Protocol Design and Validation (Spring 2004, Autumn 2005 & Summer 2007) and the postgraduate-level module Reactive Systems Design (Spring 2007-2009)
  • Co-instructor of the postgraduate-level modules Requirements Engineering (Autumn 2003-2006) and Java and Biocomputing (Spring 2005 & 2006)
  • Supervisor of Post Docs, PhD students and BSc/MSc students
• September 2000 - December 2002:
  • Senior Lecturer. Department of Computer Science, University of Sheffield, UK
  • Member of the Verification and Testing Group and of the Centre for Mobile Communications Research
  • Director of Undergraduate Admissions (between September 2001 and December 2002); Undergraduate Admissions Tutor (between September 2000 and August 2001)
  • Instructor of the undergraduate-level modules Principles of Computer Networks and Software Engineering Practice
  • Instructor of postgraduate-level modules in advanced research topics, including Semantic Foundations of Engineering Design Languages and Automated Design Validation
  • Supervisor of PhD students and BSc/MSc students
• January 2000 - May 2000:
  • Adjunct Assistant Professor, Department of Computer Science, College of William and Mary, Virginia, USA
  • Instructor of an advanced graduate-level module on Principles of Program Analysis and Verification
• July 1998 - August 2000:
  • Staff Scientist, Institute for Computer Applications in Science and Engineering (ICASE), NASA Langley Research Center, Virginia, USA
  • Leader of ICASE's research efforts into Formal Methods
  • Principal Investigator in the field of Formal Methods for the specification, design, and verification of fault-tolerant, real-time, embedded, and safety-critical systems
  • Instructor of a short course on Introduction to Model Checking
• April 1996 - June 1998:
  • Staff Scientist, Department of Mathematics and Computer Science, University of Passau, D
  • Investigator of specification formalisms for concurrent and distributed systems
  • Instructor of a graduate-level module on Specification Languages, focusing on SDL and Statecharts
  • Organisor and instructor of weekly practicals for modules in System Architectures and Programming, Software Engineering and Implementation of Databases; prepared and marked student assignments and exams
  • Supervisor of MSc projects
• April 1995 - March 1996:
  • Visiting Scholar, Department of Computer Science, North Carolina State University, USA
  • Investigator of process calculi with priority and real-time
  • Host: Prof. Rance Cleaveland
• August 1994 - March 1995:
  • Staff Scientist, Department of Mathematics and Computer Science, University of Passau, D
  • Investogator in the field of analysis and verification of concurrent and distributed systems
  • Organisor and instructor of weekly practicals for an undergraduate module; prepared and graded student assignments and exams
  • Supervisor of MSc students in research seminars
  • Organisor and supervisor of system administration tasks
• August 1993 - July 1994:
  • Research Assistant, Department of Mathematics and Computer Science, University of Passau, D
  • Investigator of state-space generation techniques aimed at avoiding the state-space explosion problem
  • Preparator of lecture notes for a module on Principles of Program Analysis and Verification
• October 1990 - July 1993:
  • Teaching Assistant, Institute for Geometry and Practical Mathematics, RWTH Aachen University, D
  • Instructor of weekly practicals for modules in Numerical Mathematics
  • Instructor of graduate-level lab work in Applied Numerical Mathematics
  • Marker of student assignments and exams

Grants & Awards

• Lüttgen, G. and Deubzer, M., 2017-2018. Optimiertes Buffering für zeitgesteuerte automobile Software (Optimized Buffering of Time-Triggered Automotoive Software) - OBZAS. Bayerische Forschungsstiftung (grant no.: AZ-1257-16), EUR 41,400. Abstract (in German).

  Das Einhalten harter Echtzeitanforderungen ist für sicherheitskritische eingebettete Multicore-Systeme unverzichtbar. Zeitgesteuerte Echtzeitsysteme bieten hierbei ein absolut zeitlich vorhersagbares Verhalten, jedoch zu Lasten einer effizienten Ressourcennutzung. Ziel dieses Projekts ist die Entwicklung und Implementierung neuartiger Algorithmen und Heuristiken, welche die Kommunikation zwischen Prozessorkernen mittels optimierter Buffering-Mechanismen minimieren und auf industrieller Automobilsoftware evaluiert werden sollen.

• Lüttgen, G. and Vogler, W., 2016-2019. Foundations of Heterogeneous Specifications Using State Machines and Temporal Logic. Research grant (Sachbeihilfe). DFG (grant no.: LU 1748/3-2), EUR 283,012. Abstract / Case for Support.

  his project shall significantly enhance the foundations and practical utility of concurrency-theoretic specification formalisms, and in particular interface theories, that enrich state machine notations with logic connectives, thus promising more concise specifications. Prior work in this project has seen the development of the MIA (Modal Interface Automata) interface theory that combines de Alfaro and Henzinger's Interface Automata with Larsen et al.'s Modal Transition Systems. In contrast to related work, MIA is nondeterministic, properly handles conjunction and internal behaviour, and allows for fully compositional interface refinement, all while preserving an optimistic view of component compatibility. The project so far has also added temporal-logic operators for expressing safety properties within interfaces, thereby yielding a truly heterogeneous specification theory. The follow-up project proposed here shall further enrich MIA's heterogeneity and practicality along three dimensions. Firstly, the MIA framework shall be elaborated so as to be able to reason also about liveness and fairness properties, and equipped with an according and more sophisticated notion of interface refinement. Secondly, MIA's communication mechanism shall be extended to handle value- passing and complemented by a mechanism for shared-variable communication; both are necessary to adequately capture features of modern parallel programming languages. Thirdly, MIA shall be cast into a behavioural type theory, thereby making it not only useful for the model-based design but also for the programming of complex concurrent systems. The outcome of this project shall be novel and expressive interface and behavioural type theories as well as accompanying prototypic tools centered around Google's parallel programming language Go, together with demonstrators and evaluations on the basis of case studies.

• Lüttgen, G., 2014-2017. Learning Data Structure Behaviour from Executions of Pointer Programs. Sachbeihilfe, Deutsche Forschungsgemeinschaft (DFG, LU 1748/4-1), EUR 325,003. Abstract / Case for Support.

  This project concerns the development of techniques to automatically and reliably learn the data structure behaviour in a pointer program by analysing traces of its execution. For example, when considering a program that employs a linked list to implement a queue, we would like to learn the shape of the data structure (singly linked list), its behaviour (only operations consistent with a queue are permitted) and any relevant additional information (such as whether the list uses a header node). This information may be used to further automate formal verification, understand legacy code and aid in reverse engineering. Existing approaches in these domains are limited in that they either ignore pointers, can handle only simple dynamic data structures automatically, or require user assistance when dealing with complex data structures.

  Recently, we have successfully prototyped machine learning and pattern matching algorithms to automatically identify the behaviour of a limited set of dynamic data structures in C programs, and written a proof-of-concept implementation. We now seek to develop this idea further by providing substantial theoretical and practical advancements to enable the identification of a greater number of more complex data structures, as will be required for the analysis of real-world software from the domains of OS software (e.g., device drivers), application software (e.g., open-source user applications) and obfuscated / legacy software (e.g., malware / early versions of Unix tools). We also wish to enable the analysis for object code, thereby removing the reliance on a specific source language and providing the possibility to perform an analysis when the source code is unavailable or when object code is preferable.

  The outcome of this research project will be novel techniques, algorithms and tools that reliably identify data structures - in terms of shape, operational behaviour and coding style - within complex pointer programs. These can be interfaced to existing methods for program verification that currently require much user assistance, and will offer greatly needed support to engineers maintaining legacy systems or performing reverse engineering.

• Lüttgen, G. and Vogler, W., 2014-2016. Foundations of Heterogeneous Specifications Using State Machines and Temporal Logic. Research grant (Sachbeihilfe). DFG (grant no.: LU 1748/3-1), EUR 161,045. Abstract / Case for Support.

  This project shall significantly enhance the theoretical foundations and practical utility of the growing number of formalisms for specifying reactive systems that enrich state machine notations with logic connectives, thus promising more concise specifications. Examples are the Interface Theories of de Alfaro/Henzinger and Caillaud et al., which consider logic conjunction, and the Contractual State Machines of Paige et al., which incorporate temporal logic. However, the semantics of the latter is not yet defined mathematically, while the former theories are insensitive to deadlock and thus unsuitable for reasoning about the concurrency inherent in reactive systems.

  The project shall, firstly, fix these shortcomings by applying techniques used by the applicants in recent studies of process algebras enriched with logics. This requires capturing the input/output behaviour and the parallel compositions of Interface Theories and Contractual State Machines, while maintaining desired algebraic properties, including full-abstraction, of their refinement preorders which relate specifications and implementations. Secondly, Interface Theories shall be extended by temporal-logic operators, so as to be able to constrain system behaviour by safety properties. Thirdly, tool support in terms of a refinement checker and a simulator for Interface Theories and Contractual State Machines shall be provided, and evaluated via case studies.

• Lüttgen, G. and Ciardo, G., 2013-2014. Improving Symbolic Software Verification via Machine Learning. Internationalization of the High-Tech-Initiative. BaCaTeC (grant no.: 5 [2012-2]), EUR 4,000. Abstract / Case for Support.

  Given society's dependence on digital systems, the ability to assess their correctness is essential. However, the high complexity of software systems can overwhelm even the best verification algorithms, such as our symbolic, decision-diagram-based Saturation algorithm. To keep decision diagram sizes small and thus Saturation effective, heuristics for finding good orderings of system variables and events are required.

  This project studies the influence of system characteristics on such ordering parameters, via benchmarking software models taken from the literature and industry. It also explores how machine learning can help determine 'good' orderings for a given verification problem by analysing runs on smaller instances of the same problem. This should greatly improve the applicability of Saturation and outperform related techniques that do not take the characteristics of the studied software system into account.

• Lüttgen, G. and Paige, R., 2013-2014. Advanced Heap Analysis and Verification. Initiation of International Collaboration. DFG (grant no.: LU 1748/2-1), EUR 7,130. Abstract / Case for Support.

  The formal verification of software is key to guaranteeing their safe operation and a grand challenge in Computer Science. A main difficulty concerns reasoning about pointers and dynamic data structures stored in the computer's heap, which are indispensable in today's software but make it hard to debug. Several techniques have been proposed to address aspects of pointer programs, heap analysis and heap verification, together with prototypic tool support. However, their practical impact is currently low since they do not interoperate, and since each technique targets only specific pointer structures and does not scale beyond small programs.

  This proposal is intended to bootstrap a collaboration between internationally recognized researchers of the Universities of Bamberg, Germany, and York, U.K, which will address these shortcomings. Two bilateral workshops will give the researchers a platform to exchange their expertise and identify synergies between their approaches to heap analysis and verification. In particular, requirements for a domain-specific language for representing and reasoning about pointer programs and heap structures shall be identified, so as to enhance interoperability of approaches and tools. The workshops will incubate new ideas and, together with mutual short visits, will lead to the submission of a large-scale joint DFG/EPSRC proposal by February 2013.

• Lüttgen, G. and McDermid, J., 2008-2015. EngD in Large-Scale Complex IT Systems. EPSRC (grant no.: EP/F501374/1), GBP 4,099,287. Abstract / EPSRC Summary.

  The proposed EngD will be the major training activity of the LSCITS Initiative, whose research component is already funded by EPSRC. This Initiative was prompted by various reports by the Royal Academy of Engineering and others, which established an industrial need for specialist education in LSCITS. The specific EngD themes are those that were indentified by the Initiative as the `LSCITS Stack' that also guides the Initiative reserach programme, and spans from Mathematical Foundations, via Predicatable Software Systems, High-integrity Software Engineering and Socio-technical Systems Engineering, to Compexity in Organisations.

• Lüttgen, G. and Paige, R., 2007-2010. Refinement Patterns for Contractual Statecharts. EPSRC (grant no.: EP/E034853/1), GBP 398,273. Abstract / Case for Support / EPSRC Summary.

  Increasingly, aerospace systems such as airplane engines have a substantial computer software component. Building such software is challenging, because the software must interact with mechanical devices , like sensors on an airplane wing, and with computer hardware. Moreover, this software must be reliable, robust, and above all, safe, i.e., it must be certified as acceptably safe for use. In building such software, engineers typically rely on ad-hoc design methods for control systems. These methods usually start with an abstract description of a proposed solution, expressed in several different styles: operational (describing steps to be taken) and declarative (describing properties that the software should possess). These descriptions are then step-by-step refined into executable programs. The aim of this project is to put this ad-hoc design method on to a formal footing, via the introduction of a new concept called a refinement pattern. A refinement pattern effectively captures the step-by-step refinements that engineers carry out in practice. We will provide formal, mathematical foundations for refinement patterns and for reasoning about refinements. We also intend to support this method by developing novel and specialised tools, including a specialised model checker, that integrate with the widely used Matlab/Stateflow design tool. This will help engineers produce more reliable, more robust aerospace systems by building on their established practices.

• Lüttgen, G. and Ciardo, G., 2004-2007. New-Generation Symbolic Model Checkers for Verifying Asynchronous Systems. EPSRC (grant no.: GR/S86211/01), GBP 184,746. Abstract / Case for Support / EPSRC Summary.

  This proposal is devoted to the development, implementation, and assessment of new-generation symbolic model checkers for verifying event-based asynchronous systems, such as distributed embedded software. It involves a research collaboration of the PI with the US co-author, for whose activities the US National Science Foundation has recently awarded funding. The project's principal aim is to overcome the severe time- and memory-deficiencies of current BDD-based model-checking techniques when verifying asynchronous systems. This will be achieved by employing MDDs and Kronecker-based data structures for storing state spaces and system transitions, respectively, which will permit one to systematically exploit the event locality that is inherent in asynchronous systems in such a way that model checking only requires local manipulations of these data structures. Key project goals include the devising of parallelisations of model-checking algorithms based on these ideas, their formal proof of correctness, and their implementation in the form of C++ packages that will also be made web-accessible for remote execution. The performance of the developed model checkers will be assessed by extensive benchmarking and by comparison to existing state-of-the-art model checkers, and our algorithms' practicality will be tested by applying them to a realistic case study involving the formal analysis of human-computer-interaction aspects in aircraft cockpits.

• Lüttgen, G. and White, D., 2004. Integrating Databases into the Synchronous Paradigm for Reactive-systems Programming. Nuffield Foundation (Undergraduate Research Bursary, grant no.: URB/01528/G), GBP 1,450. Abstract / Case for Support / Final Report.

  This project shall develop a way for accessing databases within synchronous languages, which are popular for programming embedded control systems in tools such as SCADE. The devised technology shall be prototyped in SCADE and used to program a model warehouse shelving system built with Lego Mindstorms' robotics kit.

• Ciardo, G. and Lüttgen, G., 2002-2005. Automated Verification of Asynchronous Software Systems. US National Science Foundation (grant no.: CCR-0219745), USD 360,000. Abstract / Case for Support.

  The proposed research is devoted to the development and implementation of novel sequential and parallel algorithms for the verification of asynchronous software systems, such as communication protocols and distributed or embedded software. Existing automated techniques to verification via state-space exploration, in particular symbolic model checking based on Binary Decision Diagrams (BDDs), focus on verifying synchronous hardware and software. Although symbolic model checking may in principle be applied to debugging asynchronous software systems, this poses new challenges which are not or only insufficiently addressed in the literature. Most importantly, the inherent complexity of asynchronous software makes state-space exploration a time-bound problem, in addition to a memory-bound problem. The proposed work addresses these two fundamental limitations by developing algorithms that employ Multi-valued Decision Diagrams (MDDs) and Boolean Kronecker operators to encode sets of states and transitions, respectively, in contrast to BDDs traditionally used for both purposes. This paves the way for exploiting the property of event locality that is inherent in asynchronous software and, thereby, for greatly improving the efficiency of sequential algorithms and enabling their efficient parallelization. The project will focus on the following lines of inquiry:

  (1) The investigation of design choices for sequential MDD-based state-space generation algorithms exploiting event locality, and the development of sequential model checkers on top of these algorithms.

  (2) Shared-memory and distributed-memory parallelizations of the above algorithms and of the according model checkers.

  (3) The conduct of case studies involving access protocols in distributed B-tree algorithms and avionics systems to assess the utility of the work.

  This research will greatly enhance the applicability of state-space exploration techniques, especially symbolic model checking, to the verification of asynchronous software systems. The implementation of the derived algorithms in form of C++ packages will allow an easy integration and comparison with other existing verification and validation tools, as well as with industrial design tools. The packages will be made web-accessible for remote execution at the College of William and Mary, in order to gather run-time statistics that will enable to fine-tune its performance with increasing experience. Last, but not least, this project is an excellent opportunity for exposing graduate and undergraduate students to advanced software engineering technologies, as it combines the important topics of parallel and distributed algorithms and state-of-the-art verification and debugging techniques, whose industrial relevance is on the rise.

• Lüttgen, G. and Hermanns, H., 2002. Dependability Modelling and Analysis using Statecharts. British Council (UK-Netherlands Partnership Programme in Science; grant no.: PPS719), travel grant, EUR 1,888. Case for Support / Final Report.
• Mendler, M. (author) and Lüttgen, G. (PI), 2000-2003. Type Analysis for Component-based Real-time Programming. EPSRC (grant no.: GR/M99637), GBP 134,241. Abstract / Case for Support / Final Report / EPSRC Summary.

  The research involves developing a theory of real-time process types for the static validation of signal processing and control applications. It will combine the standard methods of type checking, model-checking and timing analysis within one coherent analysis framework. The type-theory and its semantics will be based on a novel notion of clocked transition systems. Using semantic abstractions, several specialised type-checking algorithms for this type system will be developed corresponding to traditional type checking, model checking, and timing analysis. Semantic coherence will be ensured by systematically maintaining and solving abstraction constraints. The semantic foundation of clocked transition systems and the concept of abstraction and constraints in type theory builds on substantial recent research carried out by the investigator. The algorithms will be integrated into an existing programming tool, provided by the collaborators, and a case study to demonstrate the usefulness and efficiency of the algorithms will be undertaken. We expect that by extending the conventional type-checking paradigm as proposed the project will open up and explore a new route for transferring formal methods technology into software industry. The methods will support practical programming tools in the targeted domain to meet the high demands on correctness, real-time performance, and numeric precision.

• Cleaveland, R. and Lüttgen, G., 2000-2003. Heterogeneous Specification Formalisms for Reactive Systems. US National Science Foundation (grant no.: CCR-9988489), USD 325,000. Abstract / Case for Support.

  This project will investigate heterogeneous, mathematically rigorous modeling and analysis techniques for embedded software. The growing popularity of embedded computer controllers in devices ranging from airplanes to pacemakers to electric shavers points to the importance of cost-effective methods supporting the software they run. Traditional specification formalisms have emphasized homogeneous approaches in which all modeling and analysis occur within one framework, such as Statecharts or temporal logic; however, heterogeneous methodologies supporting multi-paradigm specifications have strong practical motivations, and informal design notations such as UML already provide superficial support for them. To enable heterogeneous systems specifications to be analyzed in a mathematically rigorous manner, thereby providing designers with feedback in advance of implementation, the project will pursue these lines of inquiry: the development of a uniform theory of operational and logic-based system specifications; the study of mechanisms for composing component models given in disparate formalisms; the implementation of automated tool support for verifying the correctness of heterogeneous specifications; and the investigation of case studies involving avionics systems and communication protocols. This research will enhance greatly the capabilities of formal system modeling and analysis by providing a rigorous basis for diverse embedded-software specification and verification technologies to "interoperate".

• Lüttgen, G., 1995-1996. Modeling and Verification of Distributed Systems under Consideration of Priority and Real-time Aspects. German Academic Exchange Service (DAAD, Doktorandenstipendium HSP II/ AUFE; PKZ: D/95/09026), approx. DM 38,000. Case for Support / Final Report.

  Thema meiner Dissertation ist die Erweiterung der Ergebnisse meiner Diplomarbeit Kompositionelle Minimierung endlicher verteilter Systeme auf Systeme mit Prioritäten, stochastischem Verhalten und Realzeitaspekten. Neben prinzipiellen methodischen Fragen ist hier die Auseinandersetzung mit den verschiedenen diesbezüglichen Modellerweiterungen notwendig. Das spezielle Anwendungsprofil, insbesondere der Wunsch nach Einfachheit und Interaktionstransparenz erfordert Kenntnisse, die nicht allein über die einschlägige Literatur gewonnen werden können. Herr Prof. Cleaveland ist einer der führenden Experten auf den relevanten Gebieten. Seine Arbeitsgruppe bietet daher eine ideale Arbeitsumgebung, um 1) den aktuellen Forschungsstand gezielt zu sondieren, 2) die Variationsmöglichkeiten der Erweiterungen zu erfassen und 3) ein konkretes Szenario zur Realisierung meines Vorhabens zu entwickeln. Die Ergebnisse dieser drei Schritte sollen in einem Bericht zusammengefasst werden, der zu einem Kernstück meiner Dissertation werden soll.

Program Committees

• 25th Intl. Conf. on Engineering of Complex Computer Systems (ICECCS 2020), Singapore, October 2020.
• 24th Intl. Conf. on Engineering of Complex Computer Systems (ICECCS 2019), Hong Kong, China, November 2019.
• GI Jahrestagung Informatik (INFORMATIK 2019). Track Sicherheit, Zuverlässigkeit, Korrektheit, Kassel, Germany, September 2019.
• 30th Intl. Conf. on Concurrency Theory (CONCUR 2019), Amsterdam, The Netherlands, August 2019.
• 3rd Intl. Workshop on Verification of Objects at Runtime Execution (VORTEX 2019), London, UK, July 2019.
• 19th Intl. Conf. on Application of Concurrency to System Design (ACSD 2019), Aachen, Germany, June 2019.
• 23rd Intl. Conf. on Engineering of Complex Computer Systems (ICECCS 2018), Melbourne, Australia, December 2018.
• 18th Intl. Conf. on Application of Concurrency to System Design (ACSD 2018), Bratislava, Slovakia, June 2018.
• 22nd Intl. Conf. on Engineering of Complex Computer Systems (ICECCS 2017), Fukuoka, Japan, November 2017.
• 13th Intl. Conf. on integrated Formal Methods (iFM 2017), Torino, Italy, September 2017.
• 21st Intl. Conf. on Engineering of Complex Computer Systems (ICECCS 2016), Dubai, United Arab Emirates, November 2016.
• 9. GI-Arbeitstagung Programmiersprachen (ATPS 2016), Vienna, Austria, February 2016. (Workshop organized by the German Informatics Society)
• 20th IEEE Intl. Conf. on Engineering of Complex Computer Systems (ICECCS 2015), Gold Coast, Australia, December 2015.
• 14th Intl. Workshop on Automated Verification of Critical Systems (AVoCS 2014), Enschede, The Netherlands, September 2014.
• 19th IEEE Intl. Conf. on Engineering of Complex Computer Systems (ICECCS 2014), Tianjin, China, August 2014.
• 14th Intl. Conf. on Application of Concurrency to System Design (ACSD 2014), Tunis, Tunisia, June 2014.
• 16th Brazilian Symp. on Formal Methods (SBMF 2013), Brasilia, Brazil, September 2013.
• 13th Intl. Workshop on Automated Verification of Critical Systems (AVoCS 2013), Guildford, Surrey, UK, September 2013.
• 11th IEEE Intl. Conf. on Industrial Informatics (INDIN 2013), track on Ensuring Safety in Industrial Critical Systems (ESICS), Bochum, Germany, July 2013.
• 18th IEEE Intl. Conf. on Engineering of Complex Computer Systems (ICECCS 2013), Singapore, July 2013.
• 13th Intl. Conf. on Application of Concurrency to System Design (ACSD 2013), Barcelona, Spain, July 2013.
• 5th Intl. Conf. on Subject-Oriented Business Process Management (S-BPM 2013), Deggendorf, Germany, March 2013.
• 8th Doctoral Workshop on Mathematical and Engineering Methods in Computer Science (MEMICS 2012), Znojmo, Czech Republic, October 2012.
• 15th Brazilian Symp. on Formal Methods (SBMF 2012), Natal-RN, Brazil, September 2012.
• 12th Intl. Workshop on Automated Verification of Critical Systems (AVoCS 2012) (co-chair), Bamberg, Germany, September 2012.
• 11th Intl. Workshop on Parallel and Distributed Methods in verifiCation (PDMC 2012), London, UK, September 2012.
• 17th IEEE Intl. Conf. on Engineering of Complex Computer Systems (ICECCS 2012), Paris, France, July 2012.
• 2nd Intl. Workshop on Petri Nets Compositions (CompoNet 2012), Hamburg, Germany, June 2012.
• 26th IEEE/ACM Intl. Conf. on Automated Software Engineering (ASE 2011, Tool Track), Lawrence, Kansas, USA, November 2011.
• 14th Brazilian Symp. on Formal Methods (SBMF 2011), Sao Paulo, Brazil, September 2011.
• 11th Intl. Workshop on Automated Verification of Critical Systems (AVoCS 2011), Newcastle upon Tyne, UK, September 2011.
• 22nd Intl. Conf. on Concurrency Theory (CONCUR 2011), Aachen, Germany, September 2011.
• 10th Intl. Workshop on Parallel and Distributed Methods in verifiCation (PDMC 2011), Snowbird, Utah, USA, July 2011.
• 16th IEEE Intl. Conf. on Engineering of Complex Computer Systems (ICECCS 2011), Las Vegas, Nevada, USA, April 2011.
• 37th Intl. Conf. on Current Trends in Theory and Practice of Computer Science (SOFSEM 2011), Novy Smokovec, Slovakia, January 2011.
• 13th Brazilian Symp. on Formal Methods (SBMF 2010), Natal, Rio Grande do Norte, Brazil, November 2010.
• 10th Intl. Workshop on Automated Verification of Critical Systems (AVoCS 2010), Düsseldorf, Germany, September 2010.
• 15th IEEE Intl. Conf. on Engineering of Complex Computer Systems (ICECCS 2010), Oxford, UK, March 2010.
• 8th Intl. Workshop on Parallel and Distributed Methods in verifiCation (PDMC 2009), Eindhoven, The Netherlands, November 2009.
• 9th Intl. Workshop on Automated Verification of Critical Systems (AVoCS 2009), Gregynog, Wales, September 2009.
• 7th Intl. Workshop on Parallel and Distributed Methods in verifiCation (PDMC 2008) (co-chair), Budapest, Hungary, March 2008.
• 3rd Intl. Workshop on Systems Software Verification (SSV 2008), Sydney, Australia, February 2008.
• 6th Intl. Workshop on Parallel and Distributed Methods in verifiCation (PDMC 2007), Berlin, Germany, July 2007.
• 3rd Intl. Workshop on Methods and Tools for Coordinating Concurrent, Distributed and Mobile Systems (MTCoord 2007), Paphos, Cyprus, June 2007.
• Intl. Workshop on Model-Driven High-Level Programming of Embedded Systems (SLA++P 2007), Praga, Portugal, March 2007.
• 4th Intl. Conf. on Formal Modelling and Analysis of Timed Systems (FORMATS 2006), Paris, France, September 2006.
• 17th Intl. Conf. on Concurrency Theory (CONCUR 2006), Bonn, Germany, August 2006.
• 2nd Intl. Workshop on Methods and Tools for Coordinating Concurrent, Distributed and Mobile Systems (MTCoord 2006), Bologna, Italy, June 2006.
• 2nd Intl. Workshop on Semantic Foundations of Engineering Design Languages (SFEDL 2004) (co-chair), Barcelona, Spain, April 2004.
• 3rd Intl. Workshop on Models for Time Critical Systems (MTCS 2002), Brno, Slovakia, August 2002.
• 1st Intl. Workshop on Semantic Foundations of Engineering Design Languages (SFEDL 2002) (co-chair), Grenoble, France, April 2002.
• 2nd Intl. Workshop on Models for Time Critical Systems (MTCS 2001), Aalborg, Denmark, August 2001.
• 5th NASA Langley Formal Methods Workshop (Lfm2000), Williamsburg, Virginia, USA, June 2000.

Editorial Boards & Committees

• Fakultätentag Informatik e.V. (Association of Computer Science Departments at German Universities) - Member of the Board of Directors (January 2018 - current)
• Information and Computation, an international journal published by Elsevier - Member of the Editorial Board (April 2017 - current)
• European Joint Conferences on Theory and Practice of Software (ETAPS) - Member of the Steering Committee (April 2007 - current); Member of the Executive Committee (April 2011 - current); Treasurer (April 2011 - current); Vorstand ETAPS e.V. (April 2011 - current)
• Fachgruppe Concurrency Theory der Gesellschaft für Informatik e.V. (Concurrency Theory Section, German Computer Science Society) - Member of the Steering Committee (April 2013 - March 2019)

Consultancies

• Deutscher Akademischer Austauschdienst (DAAD, German Academic Exchange Service), Germany. Member of committees for evaluating Trans National Education project, which are partially funded by the German state, 2009, 2012 & 2017.
• Duale Hochschule Baden-Württemberg (Baden-Wuerttemberg Cooperative State University), Germany. External Examiner for degree courses in computing/informatics, in accordance with the regulations and procedures of the Open University Validation Service, 2010-2012.
• Institute for Computer Applications in Science and Engineering (ICASE), NASA Langley Research Center, Virginia, USA, 2001-2002.

Reviewing

Reviewer for the following grant organisations (date of last review):

• DAAD (Deutscher Akademischer Austausch Dienst) - German Academic Exchange Service (April 2017)
• DFG (Deutsche Forschungs Gemeinschaft) - German Research Foundation (March 2013)
• EPSRC (Engineering and Physical Sciences Research Council) - UK Science Foundation (March 2013). In addition: Member of the EPSRC Software Panel (April & July 2002).
• ERC - European Research Council (April 2010)
• ISF - Israel Science Foundation (May 2009)
• NWO - Dutch Science Foundation (April 2008)
• NRF - National Research Foundation, South Africa (June 2008)

Reviewer for the following journals (date of last review):

• AMS Mathematical Reviews (September 2017)
• Annals of Software Engineering (July 1998)
• Automated Software Engineering (October 2008)
• The Computer Journal (October 2001)
• Computer Languages (November 1999)
• ACM Computing Surveys (November 2001)
• BCS Formal Aspects of Computing (September 2015)
• Formal Methods in System Design (January 2015)
• Fundamenta Informaticae (January 2010)
• Information and Computation (August 2012)
• Information and Software Technology (July 2002)
• Information Processing Letters (May 2015)
• Journal of the Association for Computing Machinery (October 1997)
• Journal of Automata, Languages and Combinatorics (November 2005)
• Journal of Computer and System Sciences (May 2005)
• Journal of Computer Science and Technology (June 2008)
• Journal of Functional Programming (October 2012)
• Journal of Logic and Algebraic Programming (May 2005)
• Journal of Logic and Computation (April 2008)
• Mathematical Structures in Computer Science (January 2014)
• Science of Computer Programming (August 2015)
• Software: Practice & Experience (February 2010)
• Software Testing, Verification & Reliability (September 2010)
• Software Tools for Technology Transfer (July 2000)
• Theoretical Computer Science (May 2013)
• ACM Transactions on Embedded Computing Systems (June 2014)
• ACM Transactions on Programming Languages and Systems (December 2005)
• IEEE Transactions on Software Engineering (November 2009)

Reviewer for the following international conferences and workshops (date of last review):

• Intl. Conf. on Application of Concurrency to System Design (ACSD) (March 2013)
• Intl. AMAST Workshop on Real-Time and Probabilistic Systems (ARTS) (January 1999)
• IEEE/ACM Intl. Conf. on Automated Software Engineering (ASE) (July 2011)
• GI-Arbeitstagung Programmiersprachen (ATPS) (January 2016)
• Intl. Workshop on Automated Verification of Critical Systems (AVoCS) (July 2013)
• Intl. Workshop on the Construction and Analysis of Safe, Secure and Interoperable Smart Devices (CASSIS) (July 2004)
• Intl. Conf. on Computer Aided Verification (CAV) (February 2007)
• Intl. Conf. on Concurrency Theory (CONCUR) (June 2019)
• Intl. Workshop on Expressiveness in Concurrency Theory (EXPRESS) (July 2003)
• Intl. Conf. on Formal Methods (FM) (June 2006)
• Intl. Conf. on Formal Modelling and Analysis of Timed Systems (FORMATS) (May 2006)
• Intl. Conf. on Formal Description Techniques for Distributed Systems and Communication Protocols, and Protocol Specification, Testing and Verification (FORTE/PSTV) (June 2000)
• Intl. Conf. on Foundations of Software Science and Computation Structures (FOSSACS) (November 2013)
• Intl. Conf. on Fundamentals of Software Engineering (FSEN) (November 2008)
• Intl. Conf. on Automata, Languages and Programming (ICALP) (March 2006)
• IEEE Intl. Conf. on Engineering of Complex Computer Systems (ICECCS) (August 2017)
• Italian Conf. on Theoretical Computer Science (ICTCS) (June 2003)
• Intl. Conf. on integrated Formal Methods (iFM) (May 2017)
• IEEE Intl. Conf. on Industrial Informatics (INDIN) (April 2013)
• Intl. Parallel and Distributed Processing Symposium (IPDPS) (November 2000)
• Intl. Conf. on Logic in Computer Science (LICS) (February 1995)
• Doctoral Workshop on Mathematical and Engineering Methods in Computer Science (MEMICS 2012) (August 2012)
• Intl. Symposium on Mathematical Foundations of Computer Science (MFCS) (May 2000)
• Intl. Workshop on Parallel and Distributed Methods in verifiCation (PDMC) (July 2012)
• Annual Symposium on Principles of Programming Languages (POPL) (September 2005)
• Brazilian Symposium on Formal Methods (SBMF) (July 2013)
• Intl. Conf. on Subject-Oriented Business Process Management (S-BPM ONE) (October 2012)
• Intl. Workshop on Model-Driven High-Level Programming of Embedded Systems (SLA++P) (December 2006)
• Intl. Conf. on Current Trends in Theory and Practice of Computer Science (SOFSEM) (October 2010)
• Intl. Workshop on Systems Software Verification (SSV) (November 2007)
• Intl. Symposium on Theoretical Aspects of Computer Science (STACS) (October 1994)
• Intl. Workshop on Tools and Algorithms for the Construction and Analysis of Systems (TACAS) (November 2007)
• Intl. Conf. on Theory and Practice of Software Development (TAPSOFT) (November 1994)
• Intl. Workshop on Algebraic Development Techniques (WADT) (November 2012)
• Intl. Workshop on Weighted Automata: Theory and Applications (WATA) (February 2003)

Conference & Workshop Organisation

• 7th IT-Forum Oberfranken, Bamberg, Germany, March 2017.
• 12th Intl. Workshop on Automated Verification of Critical Systems (AVoCS 2012), Bamberg, Germany, September 2012.
• German Chapter CONCUR (D-CON 2010), Bamberg, Germany, March 2010.
• 12th European Joint Conferences on Theory and Practice of Software (ETAPS 2009) (Organising Committee Chair), York, UK, March 2009.
• 7th Intl. Workshop on Parallel and Distributed Methods in verifiCation (PDMC 2008), Budapest, Hungary, March 2008. Satellite workshop to ETAPS 2008.
• UK Model Checking Days 2005, York, UK, September 2005.
• 2nd Intl. Workshop on Semantic Foundations of Engineering Design Languages (SFEDL 2004), Barcelona, Spain, April 2004. Satellite workshop to ETAPS 2004.
• 1st Intl. Workshop on Semantic Foundations of Engineering Design Languages (SFEDL 2002), Grenoble, France, April 2002. Satellite workshop to ETAPS 2002.

Prizes

• Finalist of the GI Dissertationspreis 1998 (Dissertation Award of the German Society for Computer Science, Gesellschaft für Informatik); only nominee from the University of Passau, Germany.

Current & Former Post Docs & PhD Students

• Dr. Diyaa Addein-Atiya (part-time; October 2004 until March 2005)
• Jan Boockmann (from April 2018)
• Dr. Néstor Cataño (September 2004 until December 2006)
• Dr. Milan Ceska (April 2011 until July 2011)
• Alexander Ditter (September 2009 until March 2012)
• Dr. Jonathan Ezekiel (October 2003 until October 2007)
• Dr. Sascha Fendrich (from September 2013 until July 2017)
• Dr. Andrew Galloway (January 2007 until March 2009)
• Johannes Gareis (from April 2017)
• Dr. Lishan Harbird (October 2007 until March 2009)
• Dr. Alexander Heußner (October 2012 until September 2017)
• Alexander Kraas (from July 2015)
• Dr. Jan Tobias Mühlberg (October 2005 until January 2011)
• Tarek Nashashbi (May 2009 until October 2009)
• Barry Norton (April 2002 until March 2003)
• Dr. Stefan Rieger (September 2011 until August 2012)
• Thomas Rupprecht (June 2014 until August 2017)
• Andreas Sailer (from November 2012)
• Dr. Stephan Scheele (since October 2018)
• Dr. Heiko Schmidt (April 2009 until September 2009)
• Ons Seddiki (March 2015 until October 2018)
• Dr. David White (since October 2009 until September 2016)
• Dr. Hashem Yazbek (May 2017 until October 2017)
• Dr. Eugene Yip (August 2015 until September 2016, and again since September 2017)

External Examining of Academic Theses

• Nils Berg, 2019, Dr. rer. nat. Electrical Engineering and Computer Science, TU Berlin, Germany.
• Jussi Lahtinen, 2016, PhD. Department of Computer Science, Aalto University, Finland.
• Chris Chilton, 2013, PhD. Department of Computer Science, University of Oxford, UK.
• Antti Siirtola, 2010, PhD. Department of Information Processing Science, University of Oulu, Finland.
• Li Hsien Yoong, 2010, PhD. Department of Electrical and Computer Engineering, University of Auckland, New Zealand.
• Heiko Schmidt, 2009, Dr. rer. nat. Technische Fakultät, Christian-Albrechts-Universität zu Kiel, Germany.
• Joachim Baran, 2008, PhD. School of Computer Science, University of Manchester, UK.
• Andy Gimblett, 2008, MPhil. Department of Computer Science, University of Wales, Swansea, UK.
• Vitus Lam, 2005, PhD. Department of Computer Science, University of Bath, UK.
• Andrew Ray, 2003, PhD. School of Information Technology & Electrical Engineering, University of Queensland, Australia.
• Radu Siminiceanu, 2003, PhD. Department of Computer Science, College of William and Mary, Virginia, USA. Now a Staff Scientist at the National Institute of Aerospace, Virginia, USA.