Curriculum Vitae

This is the professional curriculum vitae of Dr. Gerald Luettgen. 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, Aachen University of Technology, Germany. Thesis: Kompositionelle Minimierung Endlicher Verteilter Systeme (Compositional Minimisation of Finite-state Distributed Systems). Advisor: Prof. Bernhard Steffen.

Positions

• January 2003 - present:
  • Senior Lecturer, Department of Computer Science, University of York, UK
  • Member of the High Integrity Systems Engineering research group (since May 2006) and the Programming Languages and Systems research group (since January 2003)
  • MSc Software Engineering (MScSWE) Course Organiser since January 2005; MScSWE Staff Representative between October 2003 and December 2004; Member of the Masters' Teaching Committee since October 2003
  • Staff Handbook Editor since August 2003; 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
  • Teaching the undergraduate-level module Protocol Design and Validation
  • Co-teaching the postgraduate-level modules Requirements Engineering and Java and Biocomputing
  • Supervising Post Docs, PhD students and 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
  • Taught the undergraduate-level modules Principles of Computer Networks and Software Engineering Practice
  • Taught postgraduate-level modules in advanced research topics, including Semantic Foundations of Engineering Design Languages and Automated Design Validation
  • Supervised PhD students and MSc students
• January 2000 - May 2000:
  • Adjunct Assistant Professor, Department of Computer Science, College of William and Mary, Virginia, USA
  • Taught 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
  • Led ICASE's research efforts into Formal Methods
  • Conducted research in the field of Formal Methods for the specification, design, and verification of fault-tolerant, real-time, embedded, and safety-critical systems
  • Taught a short course on Introduction to Model Checking
• April 1996 - June 1998:
  • Staff Scientist, Department of Mathematics and Computer Science, University of Passau, D
  • Conducted research into specification formalisms for concurrent and distributed systems
  • Taught a graduate-level module on Specification Languages, focusing on SDL and Statecharts
  • Organised and conducted weekly practicals for modules in System Architectures and Programming, Software Engineering and Implementation of Databases; prepared and marked student assignments and exams
  • Supervised MSc projects
• April 1995 - March 1996:
  • Visiting Scholar, Department of Computer Science, North Carolina State University, USA
  • Conducted research into process calculi with priority and real-time
• August 1994 - March 1995:
  • Staff Scientist, Department of Mathematics and Computer Science, University of Passau, D
  • Performed research in the field of analysis and verification of concurrent and distributed systems
  • Organised and conducted weekly practicals for an undergraduate module; prepared and graded student assignments and exams
  • Supervised seminar work of MSc students
  • Organised and supervised system administration tasks
• August 1993 - July 1994:
  • Research Assistant, Department of Mathematics and Computer Science, University of Passau, D
  • Developed state-space generation techniques aimed at avoiding the state-space explosion problem
  • Prepared lecture notes for a module on Principles of Program Analysis and Verification
• October 1990 - July 1993:
  • Teaching Assistant, Institute for Geometry and Practical Mathematics, Aachen University of Technology, D
  • Conducted weekly practicals for modules in Numerical Mathematics
  • Trained graduate students in Applied Numerical Mathematics
  • Marked student assignments and exams

Grants & Awards

• Luettgen, 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.

  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.

• Luettgen, 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 Luettgen, 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.

• Luettgen, 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 Luettgen, 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.

  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 Luettgen, 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".

• Luettgen, 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

• 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), 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), 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.

Reviewing

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

• EPSRC (Engineering and Physical Sciences Research Council) - UK Science Foundation (August 2002)

  In addition: Member of the EPSRC Software Panel in April & July 2002.

• NWO - Dutch Science Foundation (October 2005)

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

• AMS Mathematical Reviews (March 2007)
• Annals of Software Engineering (July 1998)
• The Computer Journal (October 2001)
• Computer Languages (November 1999)
• ACM Computing Surveys (November 2001)
• BCS Formal Aspects of Computing (December 2006)
• Formal Methods in System Design (December 2005)
• Information and Computation (February 2007)
• Information and Software Technology (July 2002)
• Information Processing Letters (October 2002)
• 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 Logic and Algebraic Programming (March 2006)
• Science of Computer Programming (December 1997)
• Software Testing, Verification & Reliability (May 2004)
• Software Tools for Technology Transfer (July 2000)
• Theoretical Computer Science (July 2006)
• ACM Transactions on Programming Languages and Systems (December 2005)
• IEEE Transactions on Software Engineering (August 2006)

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

• Intl. Conf. on Application of Concurrency to System Design (ACSD) (February 2004)
• Intl. AMAST Workshop on Real-Time and Probabilistic Systems (ARTS) (January 1999)
• 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) (April 2006)
• 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 2003)
• Intl. Conf. on Automata, Languages and Programming (ICALP) (March 2006)
• Italian Conf. on Theoretical Computer Science (ICTCS) (June 2003)
• Intl. Parallel and Distributed Processing Symposium (IPDPS) (November 2000)
• Intl. Conf. on Logic in Computer Science (LICS) (February 1995)
• Intl. Symposium on Mathematical Foundations of Computer Science (MFCS) (May 2000)
• Annual Symposium on Principles of Programming Languages (POPL) (September 2005)
• Intl. Workshop on Model-Driven High-Level Programming of Embedded Systems (SLA++P) (December 2006)
• 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) (December 1996)
• Intl. Conf. on Theory and Practice of Software Development (TAPSOFT) (November 1994)
• Intl. Worskshop on Weighted Automata: Theory and Applications (WATA) (February 2003)

Conference & Workshop Organisation

• 12th European Joint Conferences on Theory and Practice of Software (ETAPS), York, UK, March 2009. This is the primary European forum for academic and industrial researchers working on topics relating to Software Science. ETAPS, established in 1998, is a confederation of five main annual conferences, accompanied by about twenty satellite workshops and other events.
• 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.

Current Collaborators

• Department of Computer Science, University of Augsburg, Germany. Contact: Prof. Walter Vogler.
• Informatics Theory Group, University of Bamberg, Germany. Contact: Prof. Michael Mendler.
• Department of Computer Science, University of California at Riverside, USA. Contact: Prof. Gianfranco Ciardo.
• Department of Computer Science, University of Maryland and Fraunhofer USA Center for Experimental Software Engineering, Maryland, USA. Contact: Prof. Rance Cleaveland.
• National Institute of Aerospace, Virginia, USA. Contact: Dr. Radu Siminiceanu.
• Formal Methods Group, NASA Langley Research Center, Virginia, USA. Contact: Ricky Butler.

Consultancies

• Institute for Computer Applications in Science and Engineering (ICASE), NASA Langley Research Center, Virginia, USA, 2001-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 and Recent Post Docs & PhD Students

• Dr. Diyaa Addein-Atiya (part-time; October 2004 until March 2005)
• Dr. Néstor Cataño (September 2004 until December 2006)
• Jonathan Ezekiel (since October 2003)
• Dr. Andrew Galloway (since January 2007)
• Jan Tobias Mühlberg (since October 2005)
• Barry Norton (April 2002 until March 2003)

External Examining

• Vitus Lam, 2005. Department of Computer Science, University of Bath, UK. Degree award pending.
• Andrew Ray, 2003. School of Information Technology & Electrical Engineering, University of Queensland, Australia. Degree award pending.
• Radu Siminiceanu, 2003. Department of Computer Science, College of William and Mary, Virginia, USA. Awarded a PhD in 2004. Staff Scientist at the National Institute of Aerospace, Virginia, USA.