No description available.

Dynamically Typed Assembly Language (D-TAL) is not only a lightweight and effective solution to the gap generated by the drop in security produced by the translation of high-level language instructions to low-level language instructions, but it considerably eases up the burden generated by the level of complexity required to implement typed assembly languages statically. Although there are tradeoffs between the static and dynamic approaches, focusing on a dynamic approach leads to simpler, easier to reason about, and more feasible ways to understand deployment of types over monomorphically-typed or untyped intermediate languages. On this occasion, DISM, a simple but powerful and mature untyped assembly language, is extended by the addition of type annotations (on memory and registers) to produce an instance of D-TAL. Strong-DISM, the resulting language, statically, lends itself to simpler analysis about type access and security as the correlation between datatypes and instructions with their respective memory and registers becomes simpler to observe; while dynamically, it disallows operations and further eliminates conditions that from high level languages could be used to violate/circumvent security.

Ce travail se situe dans le cadre du projet ANR VBD ECOREB qui œuvre avec le projet national PN RECYBETON à la levée des verrous technologiques propres à l’utilisation des granulats recyclés en vue de la formulation des bétons de structure.Pour cette étude six bétons de granulats recyclés correspondant à deux classes de résistance C25/30 et C35/40 et à une classe de consistance S4 sont élaborés. Ces formulations, définies dans le cadre du PN RECYBETON, sont conçues à partir de deux formulations de référence en substituant partiellement ou complètement les granulats naturels par des matériaux issus du recyclage des bétons. Un programme expérimental a été réalisé pour déterminer les propriétés du béton à l’état frais et à l’état durci. Les résultats des essais mécaniques montrent que pour la même classe de résistance à la compression, l’incorporation des granulats recyclés dans le béton induit une diminution de la résistance à la traction et du module d'élasticité .aussi bien qu’une augmentation de la déformation au pic et de la déformation ultime. Sous compression cyclique du type charge-décharge, l’endommagement au pic de contrainte augmente lorsque le taux de substitution est important alors que la vitesse d’endommagement devient plus faible. La campagne d’essais du fluage menée sur des poutres chargées en flexion trois points indique que la cinétique du fluage est influencée par la présence des granulats recyclés et elle est d’autant plus accélérée que le taux de remplacement est important.Les résultats expérimentaux de cette étude ainsi qu’un nombre important des résultats rapportés dans les références bibliographiques ont permis d’évaluer la validité des relations analytiques développées pour prédire les propriétés mécaniques du béton des granulats naturels en vue de leur utilisation pour le béton des granulats recyclés. On montre que ces expressions nécessitent la connaissance de la résistance moyenne à la compression, fcm aussi bien qu’un coefficient qui tient compte de l’effet des granulats recyclés. La comparaison entre les courbes contrainte-déformation obtenues dans le cadre de cette thèse et certains modèles montre, qu’avec les modifications proposées, ils décrivent d’une manière satisfaisante le comportement jusqu’à la rupture. / This work is part of the ANR VBD ECOREB which aims with the project PN RECYBETON to remove the technological locks for the use of recycled aggregates for the formulation of structural concretes.For this study, six concretes of recycled aggregates corresponding to two classes of compressive strength C25 / 30 and C35 / 40 and S4 class of workability are developed. These mixtures, defined in the framework of the PN RECYBETON, are derived from two reference formulations by substituting partially or completely the natural aggregates with materials resulting from the recycling of concretes. An experimental program was carried out to determine the properties of concrete in fresh state and hardened state. The results of mechanical tests show that for the same class of compressive strength, the incorporation of recycled aggregates into the concrete induces a decrease in the tensile strength and the elastic modulus as well as an increase in the peak and ultimate strains. Under loading-unloading compression, the damage at the peak stress increases when the substitution rate is high while the damage rate becomes lower The creep tests carried out on beams loaded under three-point bending indicate that creep kinetics are influenced by the presence of recycled aggregates and is accelerated as the replacement rate is important.The experimental results of the present study together with an extensive number of results reported in the literature have allowed evaluating the current relationships used for predicting mechanical properties of recycled concrete aggregates (RAC). The validity of many analytical expressions of the stress-strain relationship has been also studied and the effect of replacement ratio was taken into account. It was pointed out that design codes relationships dedicated to assess the mechanical properties and the stress-strain compressive curve of natural aggregates concretes (NAC) are not adequate to predict the behavior of recycled aggregates concrete (RAC). It is established that these properties are related to fcm and to a parameter, which takes into account the effect of the recycled aggregates. The comparison between the stress-strain curves obtained in this thesis and some models shows that, with the proposed modifications, these models satisfactorily describe the behavior up to failure.

Functional communication training (FCT) is an effective procedure to teach a functional communication response (FCR) and decrease problem behavior. However, there are limitations to FCT. These limitations include excessive manding (e.g., requesting items at a high rate) and manding at inappropriate times (e.g., requesting attention when caregiver is driving). Multiple schedules using static signals (e.g., colored cards) have been used to decrease these limitations while maintaining appropriate levels of the FCRs and low levels of problem behavior. Moreover, dynamic signals have been used to maintain low levels of problem behavior and appropriate levels of alternative responses outside of a multiple schedule format. Presently, no research has examined the comparison of static and dynamic signals to address the limitations of FCT. Therefore, the purpose of the current study is to compare the effects of static and dynamic signals (i.e., Time Timer®) during multiple schedules consisting of reinforcement and extinction components following FCT. Key words: functional communication training, multiple schedules, static signals, Time Timers®

The use of underwater systems has grown significantly, and they can be used both for military and civilian purposes. Many of their parts are replaceable. An underwater vehicle can be equipped with different devices depending on the taskit should carry out. This can make the vehicle unbalanced, which means that the demand for balancing systems will increase in line with the increasing use of underwater systems. The goal of the thesis is to deliver a method for balancing based on parameters estimated both in static and dynamic operation. The parameters define a nonlinear physical model that can describe the underwater vehicle in different environments and conditions. The main idea in the proposed method for parameter estimation based on static operation data is to solve equilibrium equations when the on-board control system is used to maintain two different orientations. The balancing can then be done by solving an optimisation problem that gives information about where additional weights or float material should be installed. The static parameter estimation has been evaluated successfully in simulations together with three ways of solving the balancing problem. The dynamic parameter estimation has also been evaluated in simulations. In this case, the estimated parameters seem to have the same sign as the true ones but it seems difficult to obtain accurate estimates of some of the parameters. However, the total dynamic model was good except the prediction of the vertical movements. In particular, the model could explain the rotations of the vehicle well. The reason for the worse performance for the vertical movements might be some difficulties when generating suitable excitation signals. The work done by Feras Faez Elias in connection to this master thesis made a contribution to a patent application that Saab AB has filed where Feras Faez Elias was one of the inventors.

Using contracts such as method preconditions, postconditions, and class invariants in code is an approach to preventing bugs in object-oriented programs. In the .NET Framework, this is possible due to the framework of Code Contracts, which includes Clousot, a tool for static program analysis based on abstract interpretation. Although string is a fundamental type in .NET programs, Clousot does not have a usable support for analysis of string values. In this thesis, we explore the specifics of string manipulation in the C# language and in the .NET Framework, and show how they can be covered by static analysis. Our approach is to use the methods of the String class and a subset of regular expressions to specify string properties in code, and to use abstract interpretation with non-relational abstract domains to reason about those properties. We chose a small number of already published abstract domains for strings, which vary in their complexity and ability to represent different properties. We adapted those domains to our setting, including definitions of abstract semantics for the supported string methods. We implemented the abstract domains in Clousot in a way that cooperates with numerical analysis and allows adding more string abstract domains in the future. Powered by TCPDF (www.tcpdf.org)

Cette thèse propose un nouveau cadre pour la composition de domaines abstraits. L'idée principale en est l'organisation d'une sémantique abstraite suivant la distinction usuelle entre expressions et instructions, en cours dans la plupart des langages impératifs. La définition d'une sémantique abstraite peut alors se diviser entre abstractions de valeurs et abstractions d'états (ou domaine abstrait). Les abstractions de valeurs représentent les valeurs possibles d'une expression en un point donné, et assurent l'interprétation de la sémantique des expressions. Les abstractions d'états représentent les états machines qui peuvent se produire lors de l'exécution d'un programme, et permettent d'interpréter la sémantique des instructions. De ce choix de conception découle naturellement un élégant système de communication entre abstractions. Lors de l'interprétation d'une instruction, les abstractions d'états peuvent échanger des informations au moyen d'abstractions de valeurs, qui expriment des propriétés à propos des expressions. Les valeurs forment donc une interface de communication entre états abstraits, mais sont également des éléments canoniques de l'interprétation abstraite. Ils peuvent donc eux-même être combinés par les moyens existants de composition d'abstractions, permettant encore davantage d'interactions entre les composants des sémantiques abstraites. Cette thèse explore les possibilités offertes par cette nouvelle architecture des sémantiques abstraites. Nous décrivons en particulier des stratégies efficaces pour le calcul d'abstractions de valeurs précises à partir des propriétés inférées par les domaines, et nous illustrons les différentes possibilités d'interactions que ce système offre. L'architecture que nous proposons inclue également une collaboration directe des abstractions pour l'émission des alarmes qui signalent les erreurs possibles du programme analysé. Nous proposons également un mécanisme permettant d'interagir avec les composants d'une combinaison générique de types OCaml. Nous utilisons des GADT pour encoder la structure interne d'une combinaison, et construisons automatiquement les fonctions d'injection et de projection entre le produit et ses composants. Cette fonctionnalité permet d'établir une communication directe entre les différentes abstractions d'un interpréteur abstrait. Enfin, une dernière contribution de cette thèse est l'extension automatique de domaines abstraits à l'aide de prédicats logiques qui évitent les pertes d'information aux points de jonction. De fait, lorsque plusieurs chemins d'exécution se rejoignent, un domaine abstrait doit représenter les comportements possibles de chacun des chemins, ce qui engendre souvent des pertes de précision. Pour remédier à cette limitation, nous proposons de propager un ensemble d'états abstraits, munis chacun d'un prédicat qui indique sous quelle condition l'état est valable. Contrairement à d'autres approches, notre analyse ne maintient pas une stricte partition des états abstraits, car les prédicats utilisés ne sont pas mutuellement exclusifs. Cette particularité rend possible des optimisations cruciales pour le passage à l'échelle de cette technique, confirmée par nos résultats expérimentaux sur un programme industriel généré. L'ensemble du système de composition des abstractions proposé dans cette thèse a été mis en œuvre dans EVA, la nouvelle version de l'interpréteur abstrait de Frama-C. EVA a été spécifiquement conçu pour faciliter l'introduction de nouvelles abstractions et permettre des interactions riches entre ces abstractions. Grâce à son architecture modulaire et extensible, cinq nouveaux domaines abstraits ont pu être introduit dans l'analyseur en moins d'un an, améliorant ainsi tant ses capacités que sa précision. / This thesis proposes a new framework for the combination of multiple domains in the abstract interpretation theory. Its core concept is the structuring of the abstract semantics by following the usual distinction between expressions and statements. This can be achieved by a convenient architecture where abstractions are separated in two layers: value abstractions, in charge of the expression semantics, and state abstractions —or abstract domains—, in charge of the statement semantics. This design leads naturally to an elegant communication system where the abstract domains, when interpreting a statement, interact and exchange information through value abstractions, that express properties about expressions. While the values form the communication interface between domains, they are also standard elements of the abstract interpretation framework. The communication system is thus embedded in the abstract semantics, and the usual tools of abstract interpretation apply naturally to value abstractions. For instance, different kinds of value abstractions can be composed through the existing methods of combination of abstractions, enabling even further interaction between the components of the abstract semantics. This thesis explores the possibilities offered by this framework. We discuss efficient strategies to compute precise value abstractions from the information inferred by abstract domains, and illustrate the means of communication between different state abstractions. Our architecture also features a direct collaboration for the emission of alarms that report the possible errors of a program. We also proposes a mechanism to enable interacting with the components of a modular combination of OCaml types. We use GADT to encode the inner shape of a combination, and automatically build injection and projection functions between a product of datatypes and its components. This allows direct communications between the abstractions of an abstract interpreter. Finally, a last contribution of this thesis is the automatic extension of abstract domains to track sets of disjunctive abstract states, each one being qualified with a predicate for which the state holds. This enhances the precision of an abstract semantics at join points, when several possible paths of a program execution meet. At these points, predicates preserve the information usually lost by the merge of abstract states. Unlike other approaches, the analysis does not maintain a strict partition of the abstract states, as the predicates we use are not mutually exclusive. This design enables some optimizations that are crucial for scalability, as confirmed by our experimental results on an industrial, generated program. The general system of abstractions combination has been implemented within EVA, the new version of the abstract interpreter provided by the Frama-C platform. Thus, Eva enjoys a modular and extensible architecture designed to facilitate the introduction of new abstractions and to enable rich interactions between them. Thanks to this work, five new domains from the literature have been implemented in less than a year, enhancing the scope and the precision of the analyzer.

Les liaisons hybrides métal/composite sont fréquemment sollicitées en matage. Dans le système de transmission d’un hélicoptère, ces liaisons peuvent subir plus de 〖10〗^9 cycles de chargement en fatigue. Il convient de maîtriser les effets du matage sur le comportement des matériaux, afin que ce mode de sollicitation ne conduise pas à la ruine de pièces tournantes hybrides.L’objectif de cette thèse est de s’intéresser au comportement en matage des matériaux composites stratifiés, d’abord en statique, afin d’identifier les principaux phénomènes d’endommagement, puis en fatigue. En statique, des modèles d’endommagement de complexité croissante sont proposés, puis leur réponse est analysée en détails. La fatigue est abordée principalement sous un angle expérimental. La question de l’existence éventuelle d’une limite de fatigue est discutée, et les liens étroits entre les mécanismes d’endommagement en statique et en fatigue sont mis en évidence / Hybrid metal/composite connections are frequently subjected to bearing (localised compression) loads. In a helicopter, such connections can endure as many as 〖10〗^9 fatigue cycles. It has to be ensured that the effects of bearing loads are understood in order to prevent in-service failure of hybrid rotating components. The aim of this thesis is to study the bearing behaviour of composite laminates, first under a monotonic loading, in order to identify the main damage modes, and then in fatigue. Static damage models of increasing complexity are elaborated and thoroughly analyzed. Fatigue is mainly dealt with from an experimental point of view. The possible existence of a fatigue limit is debated, and the existence of a strong connection between fatigue and static damage is emphasised.

L’utilisation du parallélisme des architectures actuelles dans le domaine du calcul hautes performances, oblige à recourir à différents langages parallèles. Ainsi, l’utilisation conjointe de MPI pour le parallélisme gros grain, à mémoire distribuée et OpenMP pour du parallélisme de thread, fait partie des pratiques de développement d’applications pour supercalculateurs. Des erreurs, liées à l’utilisation conjointe de ces langages de parallélisme, sont actuellement difficiles à détecter et cela limite l’écriture de codes, permettant des interactions plus poussées entre ces niveaux de parallélisme. Des outils ont été proposés afin de palier ce problème. Cependant, ces outils sont généralement focalisés sur un type de modèle et permettent une vérification dite statique (à la compilation) ou dynamique (à l’exécution). Pourtant une combinaison statique/- dynamique donnerait des informations plus pertinentes. En effet, le compilateur est en mesure de donner des informations relatives au comportement général du code, indépendamment du jeu d’entrée. C’est par exemple le cas des problèmes liés aux communications collectives du modèle MPI. Cette thèse a pour objectif de développer des analyses statiques/dynamiques permettant la vérification d’une application parallèle mélangeant plusieurs modèles de programmation, afin de diriger les développeurs vers un code parallèle multi-modèles correct et performant. La vérification se fait en deux étapes. Premièrement, de potentielles erreurs sont détectées lors de la phase de compilation. Ensuite, un test au runtime est ajouté pour savoir si le problème va réellement se produire. Grâce à ces analyses combinées, nous renvoyons des messages précis aux utilisateurs et évitons les situations de blocage. / Supercomputing plays an important role in several innovative fields, speeding up prototyping or validating scientific theories. However, supercomputers are evolving rapidly with now millions of processing units, posing the questions of their programmability. Despite the emergence of more widespread and functional parallel programming models, developing correct and effective parallel applications still remains a complex task. Although debugging solutions have emerged to address this issue, they often come with restrictions. However programming model evolutions stress the requirement for a convenient validation tool able to handle hybrid applications. Indeed as current scientific applications mainly rely on the Message Passing Interface (MPI) parallel programming model, new hardwares designed for Exascale with higher node-level parallelism clearly advocate for an MPI+X solutions with X a thread-based model such as OpenMP. But integrating two different programming models inside the same application can be error-prone leading to complex bugs - mostly detected unfortunately at runtime. In an MPI+X program not only the correctness of MPI should be ensured but also its interactions with the multi-threaded model, for example identical MPI collective operations cannot be performed by multiple nonsynchronized threads. This thesis aims at developing a combination of static and dynamic analysis to enable an early verification of hybrid HPC applications. The first pass statically verifies the thread level required by an MPI+OpenMP application and outlines execution paths leading to potential deadlocks. Thanks to this analysis, the code is selectively instrumented, displaying an error and synchronously interrupting all processes if the actual scheduling leads to a deadlock situation.

Doctor of Philosophy / Department of Computing and Information Sciences / David A. Schmidt / We are interested in modular static analysis to analyze softwares automatically. We focus on programs with data structures, and in particular, programs with pointers. The final goal is to find errors in a program (problems of dereferencing, aliasing, etc) or to prove that a program is correct (regarding those problems) in an automatic way. Isthiaq, Pym, O'Hearn and Reynolds have recently developed separation logics, which are Hoare logics with assertions and predicates language that allow to prove the correctness of programs that manipulate pointers. The semantics of the logic's triples ({P}C{P'}) is defined by predicate transformers in the style of weakest preconditions. We expressed and proved the correctness of those weakest preconditions (wlp) and strongest postconditions (sp), in particular in the case of while-loops. The advance from the existing work is that wlp and sp are defined for any formula, while previously existing rules had syntactic restrictions. We added fixpoints to the logic as well as a postponed substitution which then allow to express recursive formula. We expressed wlp and sp in the extended logic and proved their correctness. The postponed substitution is directly useful to express recursive formula. For example, [equations removed, still appears in abstract] describes the set of memory where x points to a list of integers. Next, the goal was to use separation logic with fixpoints as an interface language for pointer analysis. That is, translating the domains of those analyses into formula of the logic (and conversely) and to prove their correctness. One might also use the translations to prove the correctness of the pointer analysis itself. We illustrate this approach with a simple pointers-partitioning analysis. We translate the logic formula into an abstract language we designed which allows us to describe the type of values registered in the memory (nil, integer, booleans, pointers to pairs of some types, etc.) as well as the aliasing and non-aliasing relations between variables and locations in the memory. The main contribution is the definition of the abstract language and its semantics in a concrete domain which is the same as the one for the semantics of formula. In particular, the semantics of the auxiliary variables, which is usually a question of implementation, is explicit in our language and its semantics. The abstract language is a partially reduced product of several subdomains and can be parametrised with existing numerical domains. We created a subdomain which is a tabular data structure to cope with the imprecision from not having sets of graphs. We expressed and proved the translations of formula into this abstract language.