Current Ph.D. students
- Huang Li: Combining Tests and Proofs
- Ilya Baimetov: Feedback Systems for CS/SE education
- Others (in progress)
We are hiring! We are looking in particular for PhD students interested in formal methods, with both a very strong programming experience and a keen mathematical inclination. If you hold a master’s degree in CS or a related field we encourage you to apply. Applications to postdoc positions are also welcome.
Software systems govern nearlyevery 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.
Recent publications (2022 - March 2023)
Bertrand Meyer, Alisa Arkadova and Alexander Kogtenkov, The Concept of Class Invariant in Object-Oriented Programming, 2023, to appear.
Bertrand Meyer (Editor): The French School of Programming, Springer, 2023, to appear.
Bertrand Meyer: Right and Wrong: Ten Choices in Language Design, to appear in The French School of Programming (see above), 2023.
Li Huang, Sophie Ebersold, Alexander Kogtenkov, Yinling Liu and Bertrand Meyer: Lessons from Formally Verified Deployed Software Systems, submitted for publication, January 2023.
Bertrand Meyer: Handbook of Requirements and Business Analysis, Springer, 2022.
Jean-Michel Bruel, Sophie Ebersold, Florian Galinier, Manuel Mazzara, Bertrand Meyer and Alexandr Naumchev: The Role of Formalism in System Requirements, in ACM Computing Surveys, vol. 54, no. 5, pages 1-36, 2022.
Li Huang and Bertrand Meyer : A Failed Proof Can Yield a Useful Test, submitted for publication, 2022.
Li Huang, Bertrand Meyer and Manuel Oriol: Improving Counterexample Quality from Failed Program Verification, in ISWF (International Workshop on Software Faults), part of ISSRE-2022, October 2022.
Li Huang, Bertrand Meyer and others: Test Generation from Failed Proofs, filed as US Patent 17/818,348, 8 August 2022.
Maria Naumcheva, Sophie Ebersold, Alexandr Naumchev, Jean-Michel Bruel, Bertrand Meyer and Florian Galinier: Object-Oriented Requirements: a Unified Framework for Specifications, Scenarios and Tests, submitted for publication, 2022.
Alfredo Capozucca, Jean-Michel Bruel, Manuel Mazzara and Bertrand Meyer (editors): Special Issue on New Paradigms of Software Production and Deployment, Springer Nature Computer Science, vol. 3, no. 2, 2022.
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.
We welcome all inquiries, which can be directed to any member of the chair, including Prof. Meyer at email@example.com. We make every effort to respond promptly to all messages, but in the event that we miss a message, please do not hesitate to remind us. We are always happy to hear from you and are committed to providing the best possible support and guidance to those interested in software engineering.