Chair of Software and Security at Schaffhausen Institute of Technology

Prof. Bertrand Meyer

Prof. Bertrand Meyer

Head of the Chair of Software and Security
at Schaffhausen Institute of Technology

Professor of Software Engineering (emeritus) at ETH Zurich: Chair of Software Engineering. Chief Technology Officer, Eiffel Software.

CV: Électricité de France 1974-1983; Univ. of California Santa Barbara 1983-1985; Eiffel Software, Santa Barbara since 1985 (president until 2001, then CTO); ETH Zurich since Oct. 2001 (department chair 2004-2006).

Modern software systems are extremely complex constructions. Some of them are more complex than any engineering system (jet plane, space station, airport...) ever built by humankind.

In fact their level of complexity is more comparable to that of human systems such as a large city, but with a major difference: in a human system, many things can go wrong without shutting down the system; for example, in any city at any given time, there are traffic jams, accidents, closed streets, burglaries and so on, which cause disruption but not shutdown. In a software system, everything has to be right (changing a single bit in the object code of Windows, out of billions, may render the OS inoperative). Conversely, it is possible to make major changes which are not immediately detected; intruders take advantage of this property.

Fortunately, techniques of software analysis, which treat a software system as an artifact worthy of large- scale extensive study (with both logical techniques and big-data/machine learning techniques) have made tremendous progress in recent years.

The Software Analysis Factory is a general platform combining many different techniques to dissect software systems, small, large or very large, and explore their properties.

A SAF user feeds a software system (source form and object form) into the SAF and also presents a number of questions ("is a buffer overflow possible?"); the SAF produces responses in the form of an analysis. The key is the extremely high quality of such analyses, which must be sound (give correct answers) and precise (give the best answers), as well as fast. This quality, relying on advanced techniques (abstract interpretation, model checking, static analysis) is the first unique feature of the SAF.

The term "query" will denote a type of analysis (a type of questions, such as buffer overflow).

The second key distinctive characteristic of the SAF is its parameterizability. The above simplified API is the user API. The second API, giving the SAF its "universal" nature, is the technology API.

Since software analysis is fundamentally dependent on the input format (e.g. programming language), this API provides a way to make the SAF able to handle such a format. The term "handle" will denote such an adaptation (the Python handle, the .NET handle etc.).

Student Projects

Type-based deadlock prevention in SCOOP

Concurrent programming introduces new challenges for developers due to race conditions, deadlocks, starvation and priority inversion. Structured concurrent object-oriented programming (SCOOP) is data-race-free, but does not guarantee deadlock freedom. The goal of this project is to provide a sound solution to the problem using static analysis and replacing exact modelling of object structure at run-time with an approximation based on type information. The project includes development of the rules that guarantee deadlock freedom, their implementation and assessment on an existing code base, a (preferably, mechanically checked) formal proof of the technique.

Supervisor: Alexander Kogtenkov

Verification of programming languages specifications

Some programming languages are specified by text documents describing their syntax and semantics. The goal of the project is to develop a model of the programming language specification, to define the requirements that this model should satisfy, and to apply them to real-world specifications. Examples of the requirements include "all terminal symbols should be defined and used", "definitions should not be circular", "dynamic semantics should cover all cases described by static semantics", etc. Warning: most contemporary language specifications are huge, therefore, converting them to a format usable for formal verification might be time-consuming, so, please, apply to this project only if you are confident that you would be able to cover at least one currently used programming language specification.

Supervisor: Alexander Kogtenkov, Bertrand Meyer

Design by contract in dynamic context

The method of "Design by Contract" is well-studied and understood for static relations in OOP languages. In particular, it defines how to compute preconditions and postconditions for methods in descendant classes. But what if a method is used to initialize a closure variable (aka function pointer, delegate, agent, etc.) and this closure needs to have a non-trivial precondition or postcondition? The goal of the project is to develop a model for such reattachment, to specify evaluation and responsibility rules for assertions in these conditions, to provide a prototype implementation, and to prove soundness of the model.

Supervisor: Alexander Kogtenkov

Client-side selection of repeatedly-inherited methods

Multiple inheritance of implementation in an object-oriented programming language has an issue with repeated inheritance when the same parent method can have more than one implementation in a particular descendant (so-called "diamond problem"). In order to support dynamic dispatch to an intended method, one of the implementations needs to be selected. This can be done at the supplier side (e.g., using "select" adaptation clause in Eiffel), but fixes the selection once and for all. An alternative is to do the selection at the client side. Provided that the replicated methods can come in groups rather than alone, the selection should be parent-class-based instead of method-based. At least 2 projects are possible here. The common goal of either project is to develop a mechanism to select the required parent at the client side. Then, the specific goal of one project is to formally describe the semantics of the mechanism, and to prove that it has certain properties (e.g., preserves object identity, preserves parent semantics, is type-safe, etc.). The specific goal of another project is to develop an efficient implementation of the mechanism, and to prove that this implementation satisfies the expected behavior.

Supervisor: Alexander Kogtenkov

Safe covariance of argument types

Argument type covariance is essential to support the approach of "Design by Contract" in object-oriented programming languages. However, its combination with polymorphism and dynamic dispatch is known to be type-unsafe. One solution to this problem is to disable one of the variability dimensions in every particular case. This is achieved by introducing type annotations that restrict type compatibility. The goal of the project is to formalize the rules of the corresponding type system, and to prove its soundness.

Supervisor: Alexander Kogtenkov

Verified object-oriented programming language compiler

Top-level universities have developed mechanically verified compilers for subsets of C (CompCert) and ML (CakeML). The goal of the project is to bring an object-oriented language to the scene of formally verified compilers. Given that this is an ambitious target with potentially several PhD theses for a non-trivial OO language, for a master's thesis, a very limited subset of an object-oriented language would be considered, using C or ML as a backend to rely on one of the existing verified frameworks.

Supervisor: Alexander Kogtenkov

Formal verification of string constraints for Eiffel programs

Formal verification is essential to improve software quality and provide a high level of assurance of software correctness. To formally verify Eiffel programs, the semantics of the programs is formally specified in mathematical formalisms (i.e., logical formulas), which can be fed into mechanical verification tools (e.g., SMT solvers) to perform rigorous analysis on the specifications. This project aims to provide the support for formal analysis of string constraints for string-manipulation programs, i.e., Eiffel program: A set of mapping rules should be proposed to translate Eiffel strings into Boogie strings that are verifiable by SMT solvers. An automatic translation should be implemented to facilitate the translation. Verification of string constraints (e.g., word equations, length constraints, and regular membership queries) for Eiffel programs should be performed based on the proposed translation-based approach.

Supervisor: Li Huang

Research Activity

The role of formalism in system requirements.

Jean-Michel Bruel, Sophie Ebersold, Florian Galinier, Manuel Mazarra, Alexander Naumchev, Bertrand Meyer.

ACM Computing Surveys, 2021 (accepted for publication).

Mechanically-checked soundness of type-based null safety.

Alexander Kogtenkov.

CPP 2021 Lightning Talks (POPL 2021), 2021–01–18.