The Software Engineering Laboratory of Innopolis University has several open positions for PhD students and postdocs in areas of program verification, software architecture, concurrency and other advanced software engineering topics.
Innopolis, based in Kazan, Russia, is a new, well-funded university founded on the international model and aiming to reach quickly the highest international ranks. The Software Engineering Laboratory is headed by Prof. Bertrand Meyer from ETH Zurich, a leading expert in software engineering and recipient of many awards, and Prof. Manuel Mazzara, formerly of the University of Newcastle and Politecnico di Milano. Scholarships and benefits are on a par with the most attractive international offerings. Numerous opportunities are available for collaboration and exchanges with ETH and other universities including MIPT (Phystech) in Moscow. We are accepting applications from enthusiastic students with a master's or equivalent, an excellent academic record,
The working of the Language Laboratory is English.
Please send a CV, grade transcript, motivation letter and any other document (PDF or plain text only, plain attachments without zip etc.) to Manuel Mazzara (firstname.lastname@example.org)
The thesis topics proposed below all follow the same general theme: building a development environment that allows programmers to verify their software as they go. For more background look up Tony Hoare’s “Verified Software Grand Challenge”, my talks about “Verification As a Matter Of Course” (VAMOC), and the web page of my group at ETH Zurich, the Chair of Software Engineering. The base technology is as a rule Eiffel, EiffelStudio and the EVE environment, although we of course use many other tools as well, such as the Z3/Boogie tool stack developed at Microsoft Research.
A PhD is not an industry project: good PhD students adapt the original topic, and it changes anyway as the research develops. So the descriptions below should be taken as starting points. Still, they give a good idea of the kind of research we perform in the lab. I am always open to other suggestions as long as they fit in the general spirit of our work.
The topics are all related to previous work by our group at ETH (and ITMO), so you can understand them better by looking up the corresponding publications and other documentation available on the Web.
Handling numbers in a verification environment
When they appear in programs, numbers and numeric variables -- both integers and floating point -- pretend to be the same as mathematical numbers, but they are not: computers impose strict representational constraints. The purpose of this PhD is to support exact verification of numerical properties of programs. There is a substantial amount of work in the area, but no practical programming environment in which one can verify numerical properties fully and automatically. Time to change that situation.
A verified graphical library
With the EVE environment and particular the AutoProof system (see the thesis and articles by Nadia Polikarpova), we have demonstrated the possibility of producing a fully verified library in the area of data structures (EiffelBase 2). The approach is very promising, but the application domain is limited. This PhD project attacks an important and difficult application area, graphics, and verify a graphical library. The project will start by attempting to verify the EiffelVision 2 library but most likely it will have to adapt the library along the way, to make it suitable for formal proof. The result, if successful, will be groundbreaking, demonstrating the possibility of fully verifying ambitious, state-of-the-art specialized application software.
Verified application libraries
Application areas other than graphics could also benefit from a similar approach. Contact me if you have an idea for an application-specific library that you would want to verify fully.
Better automatic testing (and fixing)
The AutoTest automatic testing environment is a major advance in testing, providing push-button testing without manual writing of test cases and test oracles. New insights are needed to make it a more generally usable tool; for example it requires better testing strategies, taking advantage of contracts, and needs to handle external software elements on which little is known. There is room for a brilliant PhD thesis (or two) in this area.
Note that the complementary tool for fixing programs, AutoFix, is also ripe for more research.
The Alias Calculus, described in papers from the last 5 years, is an exciting approach to solving many core verification problems including framing, verification of programs with pointers, and deadlock analysis. There is room here for at least one brilliant PhD thesis, and probably two: one more theoretically-oriented and the other devoted to producing an outstanding implementaiton.
Integrating requirements in a seamless fashion
This is the least verification-oriented of all the topics listed here. Requirements today are done very poorly, with multiple documents each presenting a different view, and usually a wrong one. There is no simple way to connect the requirements with the reality of the software (“traceability”). The purpose of this project, based on my “multirequirements” paper (google it), is to bring about a radical change to requirements by integrating them fully in the development process and the development environment, with graphical as well as textual and formal tools.
Other topics covered in the research pages of the Chair of Software Engineering are also a fertile ground for new PhD theses. Note in particular the work on distributed software development and smart configuration management, the work on object-oriented persistence, and the TrucStudio system for course development.