Additive manufacturing completely changes the way objects can be produced. On the one hand, it simplifies the manufacturing process itself, allowing everyone - including the general public - to physically realize a virtual model using a 3D printer. On the other hand, it affords for unprecedented possibilities in terms of shape complexity, both at the macro and micro scales: objects can be filled with multi-material structures that vary in size, orientation and shape to give specific properties to the final parts. Unfortunately, describing shapes at this level of customization, scale and complexity is beyond the reach of current software. The challenge lies in how to specify shapes than can be easily manipulated, optimized for properties, as well as visualized during manipulation and prepared efficiently for the manufacturing process. A key technical choice is that of shape representation. Boundary representations (e.g. triangle meshes) are very effective to represent surfaces. However, additive manufacturing blurs the frontier between surfaces and volumes. « Implicits », a mathematical definition which computes whether a point is solid or empty, provide an efficient scalable representation. Such approaches are referred to as procedural and can be used to represent both gradient of material and microstructures. This project seek to explore novel implicit representations in order to provide a unified approach for the modeling and slicing of both macro geometry, microstructures and gradient of material. Additionally, this research aims at a complete, tight integration of both standard boundary representations and novel implicit volume representations, allowing the best choice of representation for different parts of a design. In particular I will consider how to relate features of implicit volumes to features on existing boundary meshes, as well as how to constrain implicit volumes within meshes that can be interactively edited.

This project aims to propose a declarative language dedicated to cryptanalytic problems in symmetric key cryptography using constraint programming (CP) to simplify the representation of attacks, to improve existing attacks and to build new cryptographic primitives that withstand these attacks. We also want to compare the different tools that can be used to solve these problems: SAT and MILP where the constraints are homogeneous and CP where the heterogeneous constraints can allow a more complex treatment. One of the challenges of this project will be to define global constraints dedicated to the case of symmetric cryptography. Concerning constraint programming, this project will define new dedicated global constraints, will improve the underlying filtering and solution search algorithms and will propose dedicated explanations generated automatically.

The fruitful application of logical methods in several areas of computer science, epistemology and artificial intelligence has resulted in an explosion of new logics. These logics are more expressive than classical logic, allowing finer distinctions and a direct representation of notions that do not find a natural place in classical logic. Logics are used to express different modes of truth (modal logics) and other types of reasoning including hypothetical and plausible reasoning (conditional logics), reasoning about knowledge (epistemic logics), and separation and sharing of resources (bunched implications logics). In addition to formalizing reasoning in this way, logics are also used to model various systems and to prove properties about them leading to applications in checking correctness and safe behaviour. In this project we consider those logics that are variants and generalizations of modal logics (inclusive of all the logics listed above) and characterized by variants of Kripke semantics; they find applications specifically in the areas of formal verification, epistemology and knowledge representation. Our investigation will focus on the proof-theory of these logics. Proof-theory provides a constructive approach to investigating fundamental meta-logical and computational properties of a logic through the design and the study of calculi (formal proof systems) with suitable properties (analyticity). Analytic calculi are also the base for developing practical reasoning tools such as theorem provers and proof assistants. In the literature of the last 30 years, several formal proof systems, generalizing the original sequent calculi by Gentzen, have been proposed to provide analytic calculi for modal and related logics; among them hypersequent calculi, labelled calculi and display calculi. The proof systems we study here fall into two categories: internal calculi, in which every basic object of the calculus can be read as a formula of the language of the logic, and external calculi where the basic objects are formulas of a more expressive language which partially encode the semantics (meaning) of the logic. The success of this investigation is varied: for some important classes of logics, no internal calculi are known, for others no terminating or optimal external calculi are known. The internal and external calculi reflect the two different ways of presenting a logic: syntactically and semantically. Both presentations are useful: they exhibit distinct properties and reveal different facets of the logic. The relationships between internal and external calculi are largely unexplored and their investigation is our main objective. We intend to systematically study the relationships between internal and external calculi with the aim of transferring the advantages from one type of calculi into the other. We think that such a study will shed light on the relationship between provability in syntactic and semantic-based calculi, enable the transfer of proof-theoretic properties between different calculi and lead to the discovery of internal calculi for logics that do not yet enjoy them. These new internal calculi will be helpful for the solution of several important theoretical problems including interpolation and conservativity. Indeed, the question of decidability is also still open for many logics and a main obstacle is the lack of an analytic internal calculus. The TICAMORE project will clarify the relationship between the two fundamental and historically distinct approaches, thus promoting the unification and cross-fertilization of new ideas between practitioners in the two communities, leading to new insights into the proof-theory of modal and related logics. Finally the project will contribute to the development of new automated reasoning tools to be applied in knowledge representation and in the formal verification of system properties.

All software systems execute within an environment or context. Reasoning about the correct behavior of such systems is a ternary relation linking requirements, system and context models. Formal methods are concerned with providing tool (automated) support for the synthesis and analysis of such models. These methods have quite successfully focused on binary relationships: validation of a formal model against an informal one, verification of one formal model against another formal model, generation of code from a design, and generation of tests from requirements. The contexts of systems in these cases are treated as second-class concepts: in general, the modeling is implicit and usually distributed between the requirements and system models. This project is concerned with the explicit modeling of contexts as first-class concepts. Usually, "explicit" means clearly expressed or readily observable whilst "implicit" means implied or expressed indirectly. However, it should be noted that there is some inconsistency, within computer science and software engineering communities, regarding the precise meaning of these adjectives. The requirements engineering community use the terms to distinguish between declarative (descriptive) and operational (prescriptive) requirements where they acknowledge the need for “a formal method for generating explicit, declarative, type-level requirements from operational, instance-level scenarios in which such requirements are implicit”. A consequence of our research is a formal treatment of the adjectives implicit and explicit when engineering software. Nowadays, several research projects and approaches aim at formalizing mathematical theories applicable in the formal development of systems. These theories are helpful for building complex formalizations, expressing and reusing proof of properties. Usually, these theories are defined within contexts, imported and and/or instantiated. They usually represent the implicit semantics of the systems, by types, logics, algebras, etc. based approaches. To our knowledge, no work adequately addresses the formal and explicit description of domains expressing the semantics of the universe in which the developed systems run. For example, the context dependent properties (like weight which depends on gravity) are not expressed in the formal theory in which the formal developments are conducted. This domain information is usually expressed in an explicit semantics. Several relevant properties are checked by the formal methods. These properties are defined on the implicit semantics associated to the formal technique being used: type checking, proofs theory, logic based reasoning, rewriting, refinement, model checking, trace analysis, simulation, etc. When considering these properties in their context with the associated explicit semantics, these properties may be no longer respected. As a very simple example, take two formally developed systems that are composed to exchange currency data represented by a float. This system is no longer consistent if one system refers to Euros and the other to dollars. This is due to the absence of explicit semantics expression in the proof context of the system defining this composition. Therefore, the development activities need to be revisited according to the possibility to handle not only the implicit semantics, but also the explicit one. Without a more formal software engineering development approach, based on separation of implicit and explicit, the composition of software components in common contexts risks compromising correct operation of the resulting system. This is a significant problem if we wish to develop dynamic systems of heterogeneous components that are reliable (self-healing) in unreliable contexts. Thus, this project is about separation of intrinsic and extrinsic concerns by building explicit formal models of contextual semantics using proof based techniques and illustrated on two application domains.

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.