The European Studies in Software Verification (ESSV) is a 2 years study program leading to a Master diploma in Computer Science (Master Informatique, spécialité Algorithmes & Méthodes formelles, Université de Bordeaux). The focus of this Master program is formal methods applied to software verification and analysis. This Master degree gives you the opportunity to work either in the software industry as project leader or in a computer science laboratory as researcher. Courses are mainly taken in Bordeaux University (Talence, France). They will be given in French during the first year and in English during the second year. The spring semesters of both years can be done abroad in a partner University (see International Mobility for more information).
‘Formal Methods‘ and ‘Software Verification‘ open to a quite wide-spectrum of activities and topics which can be both extremely theoretical or applied to practical industrial cases. As a non-exhaustive list of topics, here are some examples: software quality (code and process audit), compiler design (with static-analysis and abstract interpretation), protocol verification (model-checking and theorem provers), computer security (proofs of non-interference, data leakage, …), development of critical systems (aerospace, transportation, banks, …), …
The strong impact of Formal Methods on system design has been acknowledged in the recent years. In 2007, Edmund Clarke, Allen Emerson and Joseph Sifakis received the Turing award “for their original and continuing research in a quality assurance process known as Model Checking. Their innovations transformed this approach from a theoretical technique to a highly effective verification technology that enables computer hardware and software engineers to find errors efficiently in complex system designs. This transformation has resulted in increased assurance that the systems perform as intended by the designers.” Then, in 2013, Leslie Lamport received the Turing award “for fundamental contributions to the theory and practice of distributed and concurrent systems […] He devised important algorithms and developed formal modeling and verification protocols that improve the quality of real distributed systems. These contributions have resulted in improved correctness, performance, and reliability of computer systems.” And in 2014, Gérard Berry received the CNRS Gold Medal (France’s most prestigious scientific distinction) for his contributions “from the formal processing of programming languages to the computer-assisted design of integrated circuits and parallel real-time programming […] Berry’s achievements have led to major advances in information technology, finding myriad applications in the daily lives of computer users the world over.”
Formal Methods propose a rigorous approach to software design. They are now fully integrated in design processes of many companies. Since the latest version of the recommendation regarding software in airborne systems and equipments (DO-178C), they can be used in the certification process of aircrafts. They have been successfully applied to many industrial projects. For instance, the tool Astrée has been used to prove the absence of run-time errors in the primary flight control software of the Airbus A340. Many critical systems, particulary automatic transportation systems, have been developed using the B-Method. Microsoft has developed the SLAM project to improve the quality of its software and Amazon.com uses Lamport’s TLA+ to specify and check distributed algorithms.
The University and the City of Bordeaux
With 65000 students, the city of Bordeaux displays a strong educational network covering every field of study, with two universities, several engineering schools and other higher education institutions.
Situated at the south of Bordeaux, besides teaching and research buildings, the campus hosts all the necessary students’ facilities, including libraries, halls of residence, university restaurants, sports grounds, tennis courts, a swimming pool, a medical centre and social services. All these equipments can be used by students. They will have access as well to study rooms and computer facilities.
The University and the City of Bordeaux offer a wide range of opportunities for foreign student to take language courses. Students can chose between intensive summer university classes or evening courses, adapted to every level and conducted by qualified teachers.
The lecturers of the ESSV program are mainly researchers belonging to the Formal Methods team of the “Laboratoire Bordelais de Recherche en Informatique” (LaBRI). LaBRI is the Computer Science research department at the University of Bordeaux and one of the most renowned in France for research on Formal Methods.