Software systems govern nearly every aspect of today’s world and have the potential to cause enormous damage if they malfunction. The complexity of modern software often surpasses that of any engineering system ever built before. The Chair of Software Engineering is dedicated to producing tools that enable programmers to create programs that are guaranteed to function properly, where the guarantee is a mathematical proof and is automatically checked using computerized tools, providing the highest possible level of trust.

The most visible result of our multi-year research is the AutoProof system, which proves the correctness of contract-equipped Eiffel programs (see Bertrand Meyer, Object-Oriented Software Construction, Prentice Hall on Design by Contract). AutoProof relies on a technology stack including the Boogie proof system and the Z3 SMT solver. It can be used freely on the web at http://autoproof.sit.org, which includes numerous examples, documentation and tutorials.

Suggestion: try the “bank account” example at the given URL. See that it doesn’t verify. Fix the first bug (it’s easy, just a typo). Even after this correction, the program still does not verify. Can you see why? It’s actually not trivial (although in fact a simple property). Hint if you get stuck: check if the preconditions cover everything they should. Once you fix it, you will have a program that has been mathematically proved correct through a computerized proof.

We are working to refine and extend this technology to make it applicable on a large scale. Topics include special language constructs, handling large programs, handling concurrency, and handling high-level functionals (agents, delegates).

Aside from this core goal, our Chair pursues research in various areas of software engineering, including:

• Requirements engineering, a key discipline, about which we published a milestone Handbook in 2022 (see publication list).
• The role of AI and AI-based assistants (e.g. ChatGPT, GPT 4…) in producing and maintaining high-quality software.
• Software engineering for new computing paradigms such as quantum computing.
• Concurrent and distributed programming.
• Language design, with the continued development of the Eiffel language and its international (ISO) standard.
• Agile methods, software processes, tools to support software project management.
• Educational technology, particularly the development of feedback systems.

We collaborate with several of the most advanced programming methodology and software engineering research groups worldwide, primarily through the IFIP WG2.3 (Programming Methodology) working group. Our recent milestone Handbook on Requirements Engineering (published in 2022, see the publication list below) is a testament to our commitment to advancing the field of software engineering.

The Chair of Software Engineering offers a wide range of student projects on the topics described above, including  program proofs, tests, concurrency, requirements engineering, AI for software engineering, and automated support for education. If you are interested in pursuing a student project, please contact Prof. Meyer or any of the other members of the chair.