There is a growing need in the semantic web (SW) community for technologies that give humans easy access to the machine-oriented Web of data. Because it maps data to text, Natural Language Generation (NLG) provides a natural mean for presenting this data in an organized, coherent and accessible way. Conversely, the representation languages used by the semantic web (e.g., OWL ontologies and RDF data) are a natural starting ground for NLG systems. The aim of the Web-NLG project is to exploit this synergy between NLG and the Semantic Web and to further the development of robust and portable, high quality NLG systems capable of producing natural sounding text from SW data (e.g., Knowledge Bases, Linked Data). The project will build on an ongoing collaboration between LORIA (Nancy, France), the KRDB group at (Bolzano, Italy) and Stanford Research International (Palo Alto, USA), bringing together high level academic partners with internationally recognised expertise in both NLG (LORIA) and knowledge processing (KRDB, SRI).

The Spectre vulnerability has recently been reported, which affects most modern processors. The idea is that attackers can extract information about the private data using a timing attack. It is an example of side channel attacks, where secure information flows through side channels unintentionally. How to systematically mitigate such attacks is an important and yet challenging research problem. We propose to automatically synthesize mitigation of side channel attacks (e.g., timing or cache) using formal verification techniques. The idea is to reduce this problem to the parameter synthesis problem of a given formalism (for instance, variants of the well-known formalism of parametric timed automata). Given a program/system with design parameters which can be tuned to mitigate side channel attacks, our approach will automatically generate provably *secure* valuations of these parameters. We will use a 3-phase research plan: 1. define formally the problem of timing information leakage; 2. propose optimized parametric model checking algorithms for information leakage checking; 3. propose optimizations and methods translating real-worlds systems and programs into our formalisms to achieve practical scalability. We plan to deliver a fully automated toolkit which can be automatically applied to real-world systems including, those in the DARPA challenge. This project will benefit from the synergy of 5 scientists in 4 partner labs, with a complementary expertise in security, formal methods and program analysis.

Natural Language Generation (NLG) produces text from data, text or meaning representations. With the boom of AI and deep learning technology, the field of NLG has been growing at exponential speed. While NLG has many potential applications (summarization, data verbalisation, text simplification, robo-journalism, story telling, etc.), key research questions are still outstanding such as how to handle the lack of training data and how to allow for NLG into the many natural languages. Using state-of-the-art neural technologies (BERT language modelling, Encoder-Decoder architectures, multi-task and transfer learning), XNLG will (i) investigate techniques to compensate for the lack of training data and (ii) develop models for multi-lingual, multi-source generation i.e., generation into multiple languages and from either meaning representations (MR2T), text (T2T) or data (D2T). We will in particular investigate whether a single meaning representation (MR) can be used as input for generation into multiple languages and how it compares with generation from language dependent MRs; how well the models we’ll propose for MR2T generation extend to D2T and T2T generation; and whether MRs provide a better basis for MR2T generation than the powerful continuous representations currently created for sentences by neural models such as BERT and ELMO.

The development of complex (software-based) systems requires multi-view system modelling involving different scientific disciplines and skills. For instance, in the case of autonomous systems, modelling behaviours and interactions of different systems may require control theory concepts such as differential equations, communication protocols, resource allocation, access control rules, etc. State-based formal methods have proved their efficiency in supporting the development of such systems. One of these successful methods is Event-B and its RODIN IDE at the heart of the EBRP project proposal. Nowadays, Event-B and RODIN offer a - modelling language with formal semantics based on set theory and first order logic allowing to design state-based models and express system properties, namely safety; - built-in refinement operation for modelling decomposition/composition mechanisms, defining a stepwise development from an abstract model to a concrete one; - proof system to discharge proof obligations generated from models. Although Event-B and its RODIN platform offer capabilities to handle complex system models related to different engineering domain areas, it may require to model concepts that are not explicitly supported by core Event-B (e.g. real numbers, classes, communication protocols, process calculi, other logics, resource allocation, access control). Their formal definition requires starting from the core Event-B concepts (set theory, predicate logic, basic integer arithmetic). In Event-B, this modelling chain is cumbersome and reuse of obtained models can be difficult. The scientific challenge of EBRP is to address the Event-B development of complex systems allowing system models to define and borrow concepts from domain theories as first class citizens and to support formal reasoning on these objects. To achieve this objective, EBRP pushes the idea of defining a framework for extending Event-B and RODIN with domain theories (and explicit import/export mechanisms) formalising the various domain concepts. In addition, the soundness of this extension will be established. This extension framework shall allow developers to define/instantiate/import/ export/extend theories through the introduction of generic data types with associated operators, axioms and theorems. Moreover, this framework shall not be an adhoc one specifically designed for particular theories, but it will be generic. Finally, it will offer the capability for checking the correct use of these theories; in particular, it will address the soundness of mixing several theories together and the correctness of the obtained proofs. EBRP is organised around 4 technical tasks dealing with the definition of domain theories, their use in formal models, their use in (automated) proofs and a validation of the approach through complex case studies of various themes (continuous/discrete). The consortium of EBRP is made of experts of the Event-B method in France and in Europe. The inventor of the B and Event-B methods, Jean-Raymond Abrial, has accepted to join the EBRP project.

Marine environments undergo rapid changes under the influence of various pressures (human footprint, climate change) and the monitoring of their ecosystem status becomes critical. Such a monitoring requires gathering data, to process them and to extract indicators summarizing the status of the environment that is otherwise too highly dimensional to be grasped by a human being. In recent years, the massive availability of data combined with powerful machine learning algorithms and the associated hardware led to significant advances in domains that were not even dreamed about in the last few years (image classification, automatic translation, text to speech, action selection, ...). Marine ecosystems, where progress has been made in collecting large amounts of data, could also benefit from these AI advances. However, the data in environmental sciences are often sparse either in time, space or relative to the measured variables, and imbalanced which constitute challenges for AI algorithms. This leads to the two directions followed in the SMART-BIODIV proposal: 1) harnessing the power of machine learning algorithms to complete and process sparse and imbalanced data that we often encounter in environmental sciences and 2) designing indicators to qualify the ecological status of the considered environments. Even if the data are scattered, there are several heterogeneous databases that constitute as many points of view that can be combined to build a coherent and complete state of the ecosystem. We will study the potential of interpolation algorithms in time and space as well as predictive models based on co-occurrences. We will also exploit the large image databases collected by the partners on marine plankton and make them available to the challenge participants. More prospectively, we will study the feasibility of including symbolic data, such as food webs, to constrain the evolution of the state of the ecosystem and inject this knowledge of the interdependencies between the dimensions of the state to improve its estimation. These data, grouped, merged and completed, will then serve as a basis for the calculation of taxonomic and trait-based indicators, which will be designed on the basis of our expertise in freshwater bioindication. To reach the challenge’s objectives, our consortium gathers complementary expertises in deep learning, computer vision, oceanography, plankton imaging, and freshwater bioindication. In addition, our experts in AI (GeorgiaTech, CentraleSupelec) and biodiversity (LOV, LIEC) have a strong record of fruitful interdisciplinary collaborations (co-supervised PhD, co-authored articles).