• Automated Formal Proofs for Program Verification (cancelled)
• Let the CI spot the holes in tested code with the Descartes tool
• Re-engineering Software Variability into Software Product Lines
• Model your modeling workbench, and generate code and documentation from your models

In this tutorial, we focus on the use automated formal proofs for program verification. In particular, we introduce the B method, which is used in industry to specify and build, by stepwise refinements, software that requires high integrity and that is correct by design. The tutorial is a day-long tutorial and is structured in 3 parts:

1. Introduction to Atelier B, a tool that supports the B method, and which is developed by the ClearSy company.
   The B method is a method of software development based on B, a tool-supported formal method based on an abstract machine notation, used in the development of computer software. It was originally developed by Jean-Raymond Abrial in France and the UK. B is related to the Z notation (also originated by Abrial) and supports development of programming language code from specifications. B has been used in major safety-critical system applications in Europe (such as the Paris Métro Line 14). It has robust, commercially available tool support for specification, design, proof and code generation.
2. Proof search in presence of theories using deduction modulo theory. Application to the B set theory along the lines of the BWare project.
   Reasoning within theories, whether decidable or not, has become a crucial point in automated theorem proving. A theory, commonly formulated as a collection of axioms, is often necessary to specify, in a concise and understandable way, the properties of objects manipulated in software proofs, such as lists or arrays. Each theory has its own features and specificities, but a small number of them appear recurrently, among which arithmetic and set theory. Leaving the axioms and definitions of the theory at the same level as the hypotheses is not a reasonable option: first, it induces a combinatorial explosion in the search space and second, axioms do not bear any specific meaning that an automated theorem prover can take advantage of. To avoid these drawbacks, we replace axioms by rewrite rules, along the lines of deduction modulo theory, a framework combining first order proof systems with a congruence generated by rewrite rules on terms and propositions.
   In this part of the tutorial, we will see how to define an encoding of the set theory of the B method using deduction modulo theory, i.e. using a rewrite system rather than a set of axioms. We will also introduce several automated deduction tools able to deal with deduction modulo theory, whose some of them have been developed in the framework of the BWare project. Among these tools, we will present Zenon Modulo, a tableau-based theorem prover, iProver Modulo, an instantiation-based theorem prover, and Zipperposition, a superposition-based theorem prover.
3. Checking of automated formal proofs using Dedukti, a universal proof checker.
   After decades of constant work, automated theorem provers have reached a high level of efficiency and now discharge more proof obligations than ever. At the end, many of program verification tools use their corresponding automated theorem provers as oracles. The main concern here is the level of confidence users give to them. These programs are generally large software, consisting of dozens of thousands of lines of code, and using some elaborate heuristics, with some ad hoc proof traces at best, and with a simple "yes or no" binary answer at worst.
   A solution, stated by Barendregt and Barendsen and pursued by Miller among others, relies on the concept of proof certificates. Automated theorem provers should be seen as proof-certificate generators. The final "yes or no" answer is therefore left to an external proof checker.
   In this part of the tutorial, we introduce Dedukti, a proof checker based on the lambda-Pi-calculus modulo. The calculus used by Dedukti is versatile enough to encode any formalism on which an automated theorem prover is based. In particular, we propose two encodings of proofs coming from Zenon Modulo and iProver Modulo. These encodings are quite natural as the considered automated theorem provers and Dedukti rely on deduction modulo theory.

This tutorial has never been presented before.

The ClearSy company was founded on January 1st, 2001 by a group of engineers that had industrialized the formal modeling tool referred to as Atelier B, used in the rail transport industry to create safety software.
Clearsy was created on the basis of two principal objectives:

• To develop formal type methods and tools
• To develop software and systems that justify the use of formal methods

Today, ClearSy employs approximately a hundred engineers, consultants and experts in the regions of Aix en Provence, Paris, Lyon and Strasbourg. ClearSy engineers are skilled in various engineering fields (systems, mechanics, electronics, software, operational safety). They have IT tools and an electronic laboratory to create prototypes and conduct trials. Collaborations with laboratories and industrial partnerships ensure the production of the various system components (sensors and interfaces).

Olivier Hermant is a professor at CRI, the computer science laboratory of Mines ParisTech and an close collaborator to the Deducteam Inria project-team. Within the formal method community, his theoretical research interests spread from proof theory to type theory and rewriting. In the practical side, he is involved in the development of Dedukti, a universal proof-checker that is able to check proofs from various proof assistants, together with its companion tools. He also has studied various automated theorem proving techniques (resolution, tableaux).

Guillaume Burel is an assistant professor at the ENSIIE. He is a member of the Methodes team of the Samovar lab (UMR 5157 CNRS Télécom SudParis). He is also visiting scientist in the Inria project-team Deducteam. He is interested in automated deduction, reasoning mechanization, proof theory and logic in general. In particular, he is interested in the combination of theories through deduction modulo theory.

David Delahaye is a professor at the Science Faculty of the University of Montpellier. He is a member of the MaREL team of the LIRMM laboratory. His research topics are essentially the following:

• Dependability, Modeling of Critical (Embedded) Systems
• Formal Methods, Interactive and Automated Theorem Proving
• Type Theory, Proof Assistants, Proof Languages
• Formalization of Mathematics
• Interactions between Deduction and Computer Algebra

Bring your laptop, your favorite Java project (with JUnit tests) and find out how much of the covered code is actually specified by the test suite!

In this tutorial, we introduce the intriguing concept of pseudo-tested method, i.e., methods that are covered by the test suite, yet no test case fails when the method body is removed. We show that such methods can be found in mature, well-tested projects and we discuss some possible root causes. Attendants have the opportunity to experiment hands-on with our tool, called Descartes tool, which automatically detects pseudo-tested methods in Java projects.

The tutorial is structured in three parts:

• 1. Introduce the concept of pseudo-tested methods. We position these methods in the context of test adequacy assessment and contrast them with code coverage and mutation testing. We illustrate the concept with examples found in large, well tested open source projects developed by the Apache foundation, Google, Amazon and Spotify.
• 2. Let the attendants discover the presence of pseudo-tested methods in their own Java projects using our Descartes tool. This tool automatically transforms all the methods that are covered by one test case at least into empty methods. The following code shows an example of a method and the potential transformations that Descartes could create:

//Original method
public static long factorial(int n) {
    if(n==0) return 0;
    long result = 1;
    for(int i = 2; i <= n; i++)
        result *= i;
    return result;
}

//Variant 1
public static long factorial(int n) {
    return 0;
}

//Variant 2
public static long factorial(int n) {
    return 1;
}

Then the test suite is run on each transformed method, leveraging the mature and efficient transformation and test execution engine of PITest. Attendants will learn how to configure the tool for their projects and interpret the results.
• 3. We demonstrate the usage of Descartes tool in a Continuous Integration (CI) environment. We show how it can be integrated within Jenkins and Maven to monitor the evolution of a test suite. This last part is also a mix of presentation and hands-on with specific examples taken from XWiki, a well-tested, active Java-based CMS: 1, 2, 3, 4.

This tutorial has never been presented before. Yet, some parts about the presentation of pseudo-tested methods, test adequacy and Descartes have been addressed in previous talks given by the instructors:

• Advanced testing in action on a Java project: Vincent Massol gave a version of this talk at FOSDEM'84 in front of approx. 100 Java developers and another version at Devoxx'18 in front of approx. 800 Java developers. In these talks, Vincent covers aspects related to test quality, test generation and continuous integration. The video for the talk at FOSDEM'18 is publicly available. A chapter of the LesCastCodeurs podcast also included a discussion about Descartes and mutation testing.
• Mutate and Test your Tests: Talk given by Benoit Baudry at EclipseCon Europe 2017 in front of approx. 60 Java developers and testers. This talk was practically oriented, based on concrete examples that illustrate the concepts of pseudo-tested methods and the relation with test suites. The slides and video for this talk are publicly available. They illustrate the type of content that serves as a basis for the tutorial proposed here.

Oscar Luis Vera Pérez: PhD Student at Inria Rennes, France since 2017 and member of the DiverSE research group. He has been involved as a lecturer in the course of Software Validation and Verification for master students at the University of Rennes. He received his B.S in Computer Science in 2007 and a M.S degree in Mathematics in 2012 at the University of Havana Cuba where he also taught the subjects of Programming and Compiling. His current research interests are related to software testing, mutation testing and search-based software engineering.

Vincent Massol: CTO of XWiki SAS and an active committer of the XWiki open source project. Before being paid to work on open source he spent over 10 years working nights and week ends having fun on various open source projects (committer on Apache Maven, creator of Apache Cactus and Codehaus Cargo to name a few). Vincent also co-authored 3 books: JUnit in Action, Maven: A Developer's Notebook and Better Builds with Maven. He is a regular speaker at IT and Java conferences and also a member of LesCastCodeurs podcast, a French podcast focusing on news in the Java world at large.

Benoit Baudry: Professor in software technology at the KTH Royal Institute of Technology (Stockholm, Sweden). Until August 2017 he was a research scientist at INRIA, France, where he led the DiverSE research group since 2013. His research interests are in the area of automatic software testing, software diversity and DevOps. He has been teaching software testing and automatic software engineering at Universities and companies since 2004. He regularly gives talks in academic and industry conferences.

Software Product Lines (SPLs) represent one of the most exciting paradigm shift in software development in the two last decades. Multiple approaches have been proposed addressing the different activities of variability design and manipulation, reusable assets implementation, or product derivation.

However, adopting an SPL approach and managing variability is still a major challenge and represents a risk for a company. First, compared to single-system development, SPL variability management implies a methodology that highly impacts the life cycle of the products as well as the processes and roles inside the company. Second, adopting an SPL from the beginning, called proactive SPL adoption, is subject to two main assumptions: 1) these companies must have, in advance, a complete understanding of the variability to anticipate all possible variations; 2) these companies should start from scratch to specify the variability and implement the reusable assets. Thus, instead of adopting an SPL, many companies usually start from a set of existing systems that must undergo a well-defined re-engineering process. Many approaches to conduct such re-engineering processes have been proposed and documented in research literature.

In this tutorial, after introducing SPLs and their concepts, we introduce the re-engineering processes for SPL adoption and a summary of the research literature. Attendees will have the possibility to experiment hands-on with SPL open source tools and also on our tools for SPL re-engineering such as FAMILIAR and BUT4Reuse.

The tutorial is structured as follows:

1. Come, let's play with Software Product Lines. We will use two intuitive examples: a generator of LaTeX paper variants (VaryLaTeX) and a programming game-rich variability system (Robocode). These two examples will be an opportunity to present the general process of SPL engineering: (1) feature modeling (2) variability implementation (3) product derivation. We will use open source tools with exercises we used when training graduate students and PhD candidates (see http://teaching.variability.io/)
   1. Part 1: Course
      1. Domain analysis and feature model specification including feature identification, hierarchical organisation of features, constraints, and hot research topics).
      2. Domain Implementation including main existing paradigms (annotative, compositional) in different technologies (e.g, Java, JavaScript).
      3. Product Derivation for automating the synthesis of variants.
   2. Part 2: Hands-on experiments
      1. FAMILIAR (https://familiar-project.github.io) for elaborating and reasoning about feature models.
      2. Analysis of SPL implementation of open source projects.
2. SPL re-engineering. Now the audience is convinced by the benefits of an SPL approach, we introduce the general re-engineering process including the different activities related to: (1) feature identification and location (2) constraint mining (3) reusable asset extraction (4) variability model synthesis.
   1. Part 1: Course
      1. Extractive SPL adoption activities including feature Identification and location, constraints mining, reusable assets and feature model extraction.
      2. Machine learning based techniques for automatically extracting constraints.
   2. Part 2: Hands-on experiments
      1. Extracting SPL from existing variants using the BUT4Reuse platform. We will use the examples and the benchmarks provided by the BUT4Reuse platform (https://github.com/but4reuse/but4reuse/wiki/Examples).
      2. Mining constraints with statistical, supervised machine learning (https://varyvary.github.io/): we will use an end-to-end example with VaryLaTeX for learning paper variants that meet constraints.

Tutorials about variability and software product lines were presented at SPLC'12, MODELS'12, and ECSA'13. The re-engineering aspect was not a core focus of these tutorials. We will reuse and customize FAMILIAR material (see https://teaching.variability.io) for the tutorial.

VaryLaTeX has been presented at VaMoS'18 and as part of courses for introducing SPLs. It is an easy-to-understand example, especially for scholars. Other material (based on machine learning and SPL) has partly been presented as part of papers' presentations. Again we will adapt the material to precisely focus on automated re-engineering scenarios.

BUT4Reuse has been presented at ICSE'2017. It offers many tutorials and illustrative examples including adapters for software models, source code and images https://github.com/but4reuse/but4reuse/wiki/Tutorials.

Tewfik Ziadi is Associate professor at Sorbonne Université and a researcher at Laboratoire d'Informatique de Paris 6 (LIP6). He received his Ph.D. from the University of Rennes 1 in 2005 and his habilitation (HDR) in 2016 from UPMC. His main research area of interest is related to SPLs with different contributions published at ASE, SPLC or IST journal. He is a co-developer of the BUT4Reuse platform for Bottom-Up technologies for Reuse. He is the scientific coordinator of the ITEA REVaMP² project.

Mathieu Acher is Associate Professor at University of Rennes 1 /Inria, France. His research focuses on reverse engineering, modeling, and learning variability of software intensive systems with different contributions published at ASE, ESEC/FSE, SPLC, MODELS, IJCAI, or ESEM journal. He is the main developer of FAMILIAR for which he has designed and implemented novel automated operations for feature models. He is currently leading a research project on machine learning and variability: https://varyvary.github.io/.

Modeling workbenches and the use of models for code and documentation generation are core elements of Model-Driven Engineering. This tutorial will guide participants through a step-by-step scenario which leads to the creation of a modeling tool for a Lego Mindstorms Robot. This tool will allow users to define the choreography of a robot: moving forward, rotating, grabbing or releasing objects and allow the users to generate the code to be executed on the robots as well as the documentation of the choreography.

From the specification of a dedicated metamodel to the creation of custom graphical editors, including properties views and advanced edition tools, the participants will see during this hands-on tutorial, the main stages of a Sirius-based modeling tool's inception.

In a second part, the code targeting the Lego Mindstorms platform will be generated from the models to control the robot and execute the choreography.

The last point of the tutorial will target the generation of documentation from your models, based on the properties of the instances of your metamodel concepts and diagrams.

Have a look at our introducing presentation of this tutorial.

Parts of this tutorial have been given at SiriusCon, but it has been reviewed and extended and feedbacks from participants have been taken into account.

Jacob Geisel is an Eclipse Modeling Consultant at Obeo working with and on Eclipse Sirius, Acceleo, Xtext and other EMF-based technologies and is contributor to the open-source community. He is responsible for the interactions with the academic partners at Obeo. In 2015, he obtained his Ph.D. in computer science in the field of process modeling and domain specific languages targeting systems with high security requirements. During his Ph.D. thesis, Jacob has been a teaching assistant and, in the context of European and French collaborative projects, has organized workshops and tutorials on pattern, process and properties modeling and modeling workbenches. He continues to be a speaker at international conferences and modeling events, such as EclipseCon, SiriusCon or Capella Days and gives lectures at universities and tutorials on modeling techniques, DSLs and software quality.