As software spreads all over our everyday life and grows in complexity, it becomes more and more crucial to ensure a certain level of quality when producing it. “Software Verification” is the field studying the formal ways to prove the correctness of a program.
Nowadays, software verification through formal methods is a very active topic, both at a practical level in software industries and at a theoretical level in academic research. Strongly rooted in mathematics and formal methods, it also relies on computational power and on clever programming to put into practice and scale-up various verification tools. In recent years, formal methods have been used to prove the correctness of software in many prominent projects worldwide: the METEOR transportation system, the Airbus A340 and A380 aircrafts and device drivers in the Microsoft Windows operating system to cite a few.
The Master European Studies in Software Verification (ESSV) correspond to a 2-years study programme hold by Université de Bordeaux 1 and ENSEIRB-MATMECA (Bordeaux, France) and with the help of Université Libre de Bruxelles (Brussels, Belgium) and Technische Universität München (Munich, Germany) and Twente Universiteit (Twente, Netherland).
An ideal candidate for this Master needs to have an academic degree at bachelor level in computer science or mathematics. A good proficiency in English is required to follow the courses.
The ESSV trains experts in formal methods for software verification to become software and/or system safety engineers in industrial companies (domains: Software Industry, Aerospace, Transports, Electronics, Communications, …) or to start a Ph.D. in various research laboratories all over the World.
The Master is composed of 3 semesters of highly specialized academic courses (held in English), and a final internship semester (spent within a company or a research laboratory) leading to the Master thesis. Students are requested to have a mobility across Europe on the second semester. We already have several universities ready to welcome the students with an appropriate study programme, but we will probably try to enlarge the offer on the long term.
The successful completion of the study programme (i.e. validating each semester) is awarded Master’s degree in Computer Science by Bordeaux 1 University or ENSEIRB-MATMECA.
Basically, the two years are split into four semesters of 30 ECTS each. Students are encouraged to pick more than 30 ECTS for each semester, but 30 is the lowest limit to reach.
The Master starts with a Basis semester where we focus on grounding students’ knowledge, strengthen their formal and practical skills and give them a full proficiency in English. Then Advanced I (second semester) and Advanced II (third semester) focus on specialised topics in software verification and formal methods. Last semester is intended to write their Master Thesis which is defended by the end of the semester.
Table 1. (see below) shows the mobility scheme.
|Internship (4-6 months)|
All topics are taught through all the proposed mobility scheme, but one should select his mobility depending on his acquaintance with the proposed courses and the location of the universities. Knowing that, the last semester can be achieved anywhere in the World and will let you explore some more.
Université Bordeaux 1/ENSEIRB-MATMECA
This semester follows the « Master d’informatique, Algorithmique et Méthodes Formelles » from Bordeaux 1 University and in collaboration with ENSEIRB-MATMECA.
The courses are the following:
Extended Automata in Applications by Anca Muscholl (6 ECTS, original syllabus).
The course presents some fundamental results and techniques from automata theory, with widespread applications in the analysis of programs and of semi-structured data. Some of the topics covered are:
- tree automata (ranked and unranked trees);
- weighted and probabilistic automata;
- pushdown automata;
- data automata and logics;
System Modelling and Formal Design by Alain Griffault (6 ECTS, original syllabus).
Systems and software design can be made much more reliable through the use of formal methods. This course is a pragmatic approach of formal design through a wide spectrum of case studies that will be modelled in AltaRica and verified by model-checking.
Logic by Géraud Sénizergues, Pierre Castéran (6 ECTS, original syllabus).
Foundation of logic and its use in software specification, verification and program synthesis:
- Foundation of logic: Propositional logic, predicate calculus, higher-order logic, modal logic, notion of model and of validity, inference rules and notion of proof.
- Logic and Computers: Proof as a computational object, correlation between proofs and programs, formula and automata.
- Computer assisted proofs: Correct program synthesis from proofs, proof of programs.
C and Java Programming by Emmanuel Fleury (6 ECTS, original syllabus).
This course teach basics on procedural (C language) and object-oriented programming (Java language). For both programming languages, the students are asked to create from scratch a full application and to handle their code in a proper manner. More than only programming skills, this course is also concerned about code correction, efficiency and style.
Scientific Communication in Computer Science by Emmanuel Fleury (6 ECTS, original syllabus).
The students are given an introduction to research activities (paper reading and writing, writing referee for an article, presenting a paper). Moreover, they are requested to attend to seminars given by invited or local lecturers and to produce a written report on some of the talks.
Université Libre de Bruxelles
Formal Verification of Computer Systems by Thierry Massart, Jean-François Raskin (5 ECTS, original syllabus).
This course gives an introduction to existing techniques and tools to specify and formally verify distributed systems. More precisely, it encompases the study of Kripke Structures and Labeled Transition Systems, Temporal logics, omega-automata, mu-calculus, Model Checking, Symbolic and efficient Model-Checking, Specification Languages and Formal Description Techniques, Testing, Program Verification by Invariant Technique. The aim of this course is to give an overview of the most important techniques underlying computer aided verification.
Embedded Systems Design by Gilles Geraerts (5 ECTS, original syllabus).
This course considers embedded system design and aims to get students familiar with theoretical and practical solutions which allow to deal with embedded systems’ constraints. The focus will be set on the importance of the ‘model-based design’ concept in which we deal with formal models of systems to ensure that system’s specifications are holding.
Graphs and Networks by Gwenaël Joret and Martine Labbé (5 ECTS, original syllabus).
This course introduces to various graph algorithms used to solve problems over networks. This include spanning-trees algorithms, connectivity, k-colorability of a graph, Kuratowski theorem, planar graphs, …
Advanced Computability and Approximation Algorithms by Jean-François Raskin, Samuel Fiorini (5 ECTS, original syllabus).
This course goes further in the study of complexity classes by studying space complexities, classes of problems that can be solved efficiently with randomized algorithms, classes of optimization problems that can be approximated in polynomial time. The aim of this course is to give to the students the right theoretical tools to start a research activity in subjects where algorithmic complexity plays an important role.
Seminars on Critical Systems Design by Véronique Bruyère (5 ECTS).
The students are requested to attend to seminars given by invited or local lecturers and to produce a written report on some of the talks.
Finally, depending on the availability of the courses, the students will be proposed to attend one of these courses:
Concurrent System Verification by Bernard Boigelot, Pascal Gribomont, Pierre Wolper (6 ECTS, original syllabus).
This course has two parts.First one is dedicated to concurrent system verification algorithms based on state-space exploration. It covers usual state-space exploration techniques, usual optimizations and its use for formal verification on temporal logic formula through model-checking. The former problem is dealt with automata over infinite words to which a crash course is given. Symbolic verification or analysis of infinite state-space are also explored.
The second part of this course introduce the invariants method and inductive assertions. We study techniques allowing to automatically derive invariants and techniques to validate them. We will more specifically focus on tools which can partly automate the verification process, and on cases where most of the variables of the system to be verified are boolean.
Multicore Programming by Tom Van Cutsem (6 ECTS, original syllabus).
Processors are no longer growing faster. Instead, they are growing ever more parallel. Hardware architects are no longer using the additional transistors afforded by Moore’s Law to make sequential processors faster, but instead to put more processing cores on a single chip, leading to so-called chip multiprocessors, or simply multicore processors. Unfortunately, this creates a problem for us, programmers. Before the turn of the century, you could simply wait another year and your program would run faster on next-generation processors. This free lunch is now officially over: you’ll have to learn how to successfully write concurrent and parallel programs if you want your programs’ performance to continue to scale with the hardware capacity.
The course will primarily involve programming in Java, Erlang and Clojure. All of these programming languages feature direct support for concurrent programming. If you question the usefulness of non-mainstream functional languages like Erlang and Clojure, I am not alone in thinking that the ideas embedded in these languages are important going forward. Here is a preliminary list of topics to be discussed:
- Multicore Processors: what and why?
- Parallelism: laws, scalability (speedup and efficiency)
- Hardware primer: architectures, caches, cache coherence
- Parallelism vs. Concurrency
- Parallelism: DAG model, fork/join, the Java Fork/Join framework
- Concurrency: shared-memory multithreading (in Java): locks, race conditions, deadlock
- Concurrency: message-passing models: channels (Occam-pi) and actors
- Actors in practice: an introduction to Erlang
- Google’s MapReduce abstraction: parallel programming for data centers
- Practical functional programming: an introduction to Clojure
- Software-transactional memory
Technische Universität München
Logic by Tobias Nipkow (8 ECTS, original syllabus).
In the context of propositional and predicate logic the following basic notions are covered:
- Syntax and semantics
- Proof system and proof search
- Soundness and completeness
Possible further topics (non exhaustive):
- Proof systems
- Automated theorem proving
- Decision procedures
- Data base theory
- Higher-order logic
- Set theory
- Constructive logic
- Fuzzy logic.
Model-Checking I by Andrey Rybalchenko (8 ECTS, original syllabus).
Model checking is a technique used for automatically verifying whether hardware or software systems meet a given specification. Model checking has made enormous progress during the last 20 years and is nowadays used in large-scale industrial applications.
This course teaches the fundamentals of model checking, mostly for systems with finite state spaces. The course starts with the basics behind temporal logics (LTL, CTL), used for specifying correctness properties. Hardware or software systems of interest are modelled as Kripke structures, and it will be shown how such structures can be efficiently extracted, e.g., from the source code of a program. The course incorporates basic verification algorithms as well as various optimizations (“On-the-fly” model checking, partial-order reduction, binary decision diagrams, abstraction/refinement, bounded model checking) and gives a vivid picture of the current state-of-the-art. The techniques taught in the course are illustrated by software tools (Spin, SMV, Blast, CBMC), and participants have opportunity of getting hands-on experience with these.
Virtual Machine by Helmut Seidl (5 ECTS, original syllabus).
While trying to produce code for a programming language like Prolog, one quickly realizes that one would like to use certain instructions during the translation which are not already available on concrete machines. On the other hand, instruction sets of modern computers are changing so quickly that it doesn’t seem useful for the compiler to depend on some arbitrarily chosen instructions. Such a dependance would mean that in a few years one would feel obliged to rewrite the compiler anew. With the implementation of the first Pascal compilers, one already arrived at the idea of first generating code for a slightly idealized machine, each of whose instructions then only need to be implemented on different target machines. Translation of modern programming languages like Prolog, Haskell or Java are also based on this principle. On one hand this facilitates portability of the compiler. On the other hand this also simplifies the translation itself since one can choose a suitable instruction set according to the programming language to be translated. In particular, we consider:
- Translation of C;
- Translation of a functional language;
- Translation of Prolog;
- Translation of a concurrent dialect of C.
Algorithmic Game Theory by Felix Brandt (5 ECTS, original syllabus).
Algorithmic game theory is a young research area at the intersection of theoretical computer science, mathematics, and economics that deals with the optimal strategic behavior in interactive situations. Particular attention will be paid to algorithmic aspects of game-theoretic solution concepts such as Nash equilibrium and the design of mechanisms such as auctions.
Depending of the variable availability of this course, the student may choose another course on this list.
In this course we look at methods for analyzing security using techniques from the domain of programming languages and compilers, for example, abstract interpretation and type systems. Topics of the lecture are among others:
- Buffer overflows and their prevention using abstract interpretation
- Security concepts in Java: Sandbox principle, class loading, bytecode verification, stack inspection, privilege management
- Typed assembly languages
- Security protocols and their modeling
- Information flow analysis
Advanced Logic by A. Rensink (5 ECTS, original syllabus).
In logic many aspects of computer science are treated in a theoretical way. Examples are the relationship between syntax and semantics, computability, and concepts of programming languages. In a more direct sense, logic is applied in, e.g., logic programming, but also in programming by contract and other types of formal verification.
In this course we study the formal syntax and semantics of proposition and predicate logic. Several proof systems (semantic tableaux, Hilbert and Gentzen style systems, resolution) and their equivalence are presented, and soundness and completeness are discussed. We then continue by studying connections to other logic-related programming and specification paradigms: logic programming, Hoare-style (contractual) program verification, specification in Z, and temporal logic.
System Validation by M. Huisman (5 ECTS, original syllabus).
The complexity of software and hardware systems is rapidly increasing and so is their vulnerability with respect to errors. The course System Validation is focused on validation techniques and methods to assess the correctness and dependability of information- and communication technology (ICT) systems. The following tools and techniques will be discussed: the JML run-time checker, the static checker ESC/Java and the model checkers NuSMV and Java PathFinder.
The JML run-time checker and ESC/Java are used for the validation of the functional properties of Java programs. This varies from simple checks (e.g. whether arguments to a method are within a certain range) to functioal correctness, i.e. whether a program fragment actually implements the desired computation. In the course we will closely look at the verification of program invariants: properties that have to be valid during the complete execution of the program. The run-time checker only checks some sample execution, whereas ESC/Java properties proves for all possible executions.
The model checker NuSMV is used for the verification of high level designs and protocols, whereas Java PathFinder is used for the verification of Java software. These model checkers are used to check temporal properties, e.g. whether certain program steps are executed in the correct order, whether a certain program state is always reached.
In addition, several guest lecturers will be invited, to illustrate how system development can go wrong, and how validation can be used to improve the quality of system development.
This course is a hands-on course: in several practical assignments, the students will learn how to use the tools and techniques. After the course they will know when and how to use these validation tools. The acquired skills will be assessed in a written examination.
After the course, the student will be able to:
- describe the essential characteristics of the main formal techniques, and to describe in what situation what kind of tool is most appropriate
- write JML specifications
- predict what will happen when the JML run-time assertion checker is applied to an annotated code fragment
- complete and correct specifications, so that they are accepted without warnings by the ESC/Java checker
- apply abstraction techniques to write specifications that are not implementation-specific
- translate plain text requirements to temporal logic formulae, which can be checked efficiently and explain the meaning of temporal logic formulae
- interpret the meaning of counterexamples produced by the model checkers NuSMV and JPF
- write SMV specfications and verifiy them using NuSMV
- verify Java programs with JPF
Testing Techniques by M.I.A. Stoelinga (5 ECTS, original syllabus).
Testing is an important part of almost any software development project. Systematic and effective tests are crucial in the quality control of software products. However, the testing phase is often underestimated in the software life cycle. This course treats a number of techniques, methods and tools to test software in a systematic, structured and effective way. We will discuss both existing techniques and new development in the world of software testing. The techniques presented during the course focus on the testing of embedded systems and communication protocols.
Topics to be treated are: types, aspects and phases in software testing, test automation, test tools, test case design, test coverage, test generation from (formal) specification. Some courses will be given by invited software testers from industry.
The course presents a variety of frameworks for test case generation. After passing this course, the student is able to:
explain, apply, compare, the techniques within these frameworks.
- reason about the mathematical properties of these techniques and
- extend these with new features and adapt them to new testing contexts.
Advanced Programming Concepts by P.M. van den Broek (10 ECTS, original syllabus).
This course focuses on the role of composition and compositionality of programming concepts in the functional, logical and aspect-oriented paradigms. The first part of the course (4 weeks) gives an introduction to these paradigms and ends in a practical assignment.
In the second part (4 weeks), composition-related problems are presented, with a strong focus on aspect-oriented programming concepts. This part also has the goal to bring the students in touch with some of the state-of-the-art research.
The third part (8 weeks), is more interactive, and involves weekly (practical) work and presentations by the students. The aim of this part is to get a deep understanding of language design, with a focus on aspect-oriented composition. Through an incremental and iterative design of an AOP language, including implementing this in a given AOP interpreter framework, the language design space of AOP languages is explored in detail: investigating the different alternatives for expressing certain concepts in a programming language, showing concrete examples from actual AOP languages, and assessing their merits and deficiencies, in particular with respect to compositionality. The students will on a weekly basis explore part of the design space and present their results.
The students deliver the final language design and its design decisions in essay. After completing this course successfully, the student can independently:
- write algorithms in several programming paradigms
- explain the characteristics of prevalent programming paradigms
- identify software composition problems and construct solutions
- describe the metamodel for AOP languages introduced in this course
- contribute to the design of aspect-oriented programming languages, using acquired knowledge about:
- the AOP language design space;
- the trade-offs and design descisions that have to be made when designing an AOP language
Advanced Requirements Engineering by M. Daneva (5 ECTS, original syllabus).
In this course, the student performs a small research project on a topic related to requirements engineering within the research interests of the Information Systems group. Each student in the course will perform a different project. The student can choose from a number of topics, such as:
- Goal-oriented requirements engineering
- Quality attributes and soft goals
- Cost-benefit evaluation and preferences
- User-centered requirements engineering
- Systems engineering
- Analyzing ill-structured problems
- Requirements priorization
- Requirements engineering in Agile software development
- Service-oriented requirements
A final list of topics will be announced when the course begins.
The research project can either be a literature study, an empirical study, or a design project. In each case, the end product is an article that satisfies standards for scientific publications. The student has progress meetings with a staff member of the Information Systems group, but the student should be able to manage the project by him/herself. Students with good results for Design Science Methodology (7 or higher) are encouraged to take this course. Examination is by means of the scientific paper, which is reviewed by two independent researcher.
Université Bordeaux 1 / ENSEIRB-MATMECA
This semester follows the « Master d’informatique, Algorithmique et Méthodes Formelles » from Bordeaux 1 University and in collaboration with ENSEIRB-MATMECA.
Advanced Modelisation Techniques by Frédéric Herbreteau, Marc Zeitoun (6 ECTS, original syllabus).
Browse important specification and modelisation formalisms and well-known tools to verify complex systems such as distributed, real-time or other kind of systems.
- Synchronous systems: High level language (Esterel, Lustre, …), constraints automata. Tools used during this part of the course will include, for example, SMV.
- Concurrent systems: LTS, synchronization product, Petri nets, sequence diagrams, I/O automata, process algebra.
- Dense and Infinite Systems: Timed automata, hybrid automata. Tools: Uppaal, Hytech, FAST.
Software Verification by Jérôme Leroux, Grégoire Sutre, Aymeric Vincent (6 ECTS, original syllabus).
This course presents some techniques, algorithms and data-structures used in software verification. Typically:
- Model-Checking: Bounded model-checking, ROBDD data-structure, symbolic model-checking, post/pre computation, SAT solvers.
- Static Analysis: Data-flow Analysis, Abstract Interpretation (complete lattice, Galois connection, fixpoints theory), widening and narrowing.
- Verification by Abstraction: Predicate abstraction, Interpolation and CEGAR techniques (Clarke, McMillan), SMT solvers.
Games and Fix-points for Controller Synthesis by Anne Dicky, Hugo Gimbert, Anca Muscholl (6 ECTS, original syllabus).
The controller synthesis problem aims at computing a controller of a system which guarantees the system to behave correctly. When behavioral properties of the targeted system are expressed using temporal logics, the computation of a correct or optimal controller reduces to the computation of a winning or optimal strategy in a two-player zero-sum game. This course presents the
interplay between controller synthesis, fix-points computation and game theory.
- Controller synthesis;
- Games on finite graphs;
- Temporal logics for the specification (LTL, CTL);
- Fix-points and modal mu-calculus;
- Stochastic Games.
Foundation of Program Proving by Pierre Castéran and Emmanuel Fleury (3 ECTS, original syllabus).
The course will browse among:
- Proof techniques: induction, co-induction;
- Operational semantics of programs: Floyd-Hoare calculus, Lamport weakest preconditions, well-founded theory of termination;
- Proof of sequential programs: axiomatisation of datastructures (proved using induction), program annotation (precondition, postcondition, loop invariants, loop variants), proof obligations (using weakest preconditions and proved using induction);
- Tools: Coq (proofs by induction), Why (proofs of programs).
Modern Type-Oriented Constructs in Programming Languages by Philippe Narbel (3 ECTS).
Types are one of the means for obtaining some safety in programs. Even when restricted to domains where decidability is prefered, like in multi-purpose programming languages, type theory can be applied in many effective ways. Type inference, polymorphisms, genericity, class and module types, etc., are some of the sophisticated elements which now offer some automatic validation in everyday programming. Some languages have included and developed these notions from their beginning (e.g. Haskell, OCaml, Scala), and also some mainstream languages are now extended through them (e.g. Java, C#, and even C++). This course introduces and illustrates these modern type-oriented programming constructions, their theoretical foundations and their usefulness in programs.
Dependable Computing (RAMS) by Jean-Luc Chabot, Cyrille Folleau and Patrice Capircio (6 ECTS).
Mandatory for ENSEIRB-MATMECA students and to be taken in replacement of one of the previous courses.
Safety engineering, reliability, availability, maintainability. Here is the plan of the course:
- 1st part: safety engineering aims at maintaining the dependability of systems during their whole life cycle at the lowest cost. Methodologies include RAMS, threats analysis, modeling of failures: failures modes, effect analysis, fault tree analysis, failure prevention and contention.
- 2nd part: safety engineering applied to the safety of computing units in planes. This particular domain require a high level of safety that serves as a motivation. Safety analysis and failure contention is then studied.
The Research Project and the Seminars are mandatory for all students:
Research Project organized by Emmanuel Fleury (6 ECTS, original syllabus).
Seminars (0 ECTS).
The students are requested to attend to seminars given by invited or local lecturers.
The Master Thesis can be done within a research laboratory or in a company anywhere in the World. The evaluation of the student’s work is performed through a Master Thesis report and a defence that takes place at the end of the semester.
Services to the Students
The Master ESSV administratives will provide students with help for most administrative concerns (insurances, visa, unversity fees, housing, and so on).