Chair of Software and Security at SIT

Prof. Bertrand Meyer
Prof. Bertrand Meyer

Head of the Chair of Software and Security at the 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).

What is the Software Analysis Theory?

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 that 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 question, 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.)

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.

1
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 modeling of object structure at run-time with an approximation based on type information. The project includes the 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

2
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

3
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 the soundness of the model.

Supervisor: Alexander Kogtenkov

4
Client-side selection of repeatedly-inherited methods

Multiple inheritances of implementation in an object-oriented programming language have 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 the "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

5
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

6
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 Ph.D. 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

7
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

Here you can find the most recent mentions and news about the Chair.

Interested in research with Prof. Bertrand Meyer?

Apply now for your PhD or postdoc research.