Certains environnements ont besoin de plusieurs compilateurs, par exemple un pour le système d'exploitation, supportant la norme C/C++ complète, et l'autre pour les applications, qui supporte éventuellement un sous-ensemble de la norme, mais capable de fournir plus de performance. Le maintien de plusieurs compilateurs pour une plateforme cible représente un effort considérable. Il est donc plus facile d'implémenter et de maintenir un seul outil responsable des optimisations particulières au processeur ciblé. Il nous faut alors un moyen de relier ces compilateurs à l'optimiseur, de préférence, en gardant au passage certaines structures de données internes aux compilateurs qui, soit prendraient du temps, soit seraient impossible à reconstruire à partir du code assembleur par exemple. Dans cette thèse, nous introduisons Tirex, une représentation textuelle intermédiaire pour échanger des informations de bas niveau, déjà dépendantes de la cible, entre les compilateurs, les optimiseurs et les autres outils de la chaîne de compilation. Notre représentation contient un flot d'instructions du processeur cible, mais garde également la structure explicite du programme et supporte la forme SSA (Static Single Assignment). Elle est facilement extensible et très flexible, ce qui permet de transmettre toute donnée jugée importante à l'optimiseur. Nous construisons Tirex par extension de MinIR, une représentation intermédiaire elle-même basée sur un encodage YAML des structures du compilateur. Nos extensions de Tirex comprennent: l'abaissement de la représentation au niveau du processeur cible, la conservation du flot de données du programme, ainsi que l'ajout d'informations sur les structures de boucles et les dépendances de données. Nous montrons que Tirex est polyvalent et peut être utilisé dans une variété d'applications différentes, comme par exemple un environnement d'exécution virtuel (VEE),et fournit une base forte pour un environnement d'analyse du programme. Dans le cadre d'un VEE, nous présentons un interprèteur de la forme SSA et un compilateur just-in-time (JIT). Nous montrons comment l'interprétation d'une représentation au niveau du processeur cible élimine la plupart des problèmes liés à l'exécution en mode mixte. Nous explorons également les questions liées à l'interprétation efficace d'une représentation de programme sous la forme SSA. / Some environments require several compilers, for instance one for the operating system, supporting the full C/C++ norm, and one for the applications, potentially supporting less but able to derive more performance. Maintaining different compilers for a target requires considerable effort, thus it is easier to implement and maintain target-dependent optimizations in a single, external tool. This requires a way of connecting these compilers with the target-dependent optimizer, preferably passing along some internal compiler data structures that would be time-consuming, difficult or even impossible to reconstruct from assembly language for instance. In this thesis we introduce Tirex, a Textual Intermediate Representation for EXchanging target-level information between compilers, optimizers an different tools in the compilation toolchain. Our intermediate representation contains an instruction stream of the target processor, but still keeps the explicit program structure and supports the SSA form(Static Single Assignment). It is easily extensible and highly flexible, which allows any data to be passed for the purpose of the optimizer. We build Tirex by extending the existing Minimalist Intermediate Representation (MinIR), itself expressed as a YAML textual encoding of compiler structures. Our extensions in Tirex include: lowering the representation to a target level, conserving the program data stream, adding loop scoped information and data dependencies. Tirex is currently produced by the Open64 and the LLVM compilers, with a GCC producer under work. It is consumed by the Linear Assembly Optimizer (LAO), a specialized, target-specific, code optimizer. We show that Tirex is versatile and can be used in a variety of different applications, such as a virtual execution environment (VEE), and provides strong basis for a program analysis framework. As part of the VEE, we present an interpreter for a Static Single Assignment (SSA) form and a just-in-time (JIT) compiler. We show how interpreting a target-level representation eliminates most of the complexities of mixed-mode execution. We also explore the issues related to efficiently interpreting a SSA form program representation.

O emergente Paradigma Orientado a Notificações (PON) está materializado em um Framework desenvolvido na linguagem de programação C++. Este foi projetado para fornecer uma Application Programming Interface (API) e estruturas de alto nível que facilitasse o desenvolvimento de software segundo sua orientação. Entretanto, isto induz a uma sobrecarga de processamento computacional em cada aplicação PON. Ainda, uma embrionária interface amigável denominada Wizard foi concebida para prover recursos de alto nível para o desenvolvimento de certas aplicações PON. Assim, este trabalho propõe uma nova materialização do Framework PON e a evolução de sua interface Wizard. Ao final, estes são validados por meio de comparações quantitativas e qualitativas em relação aos seus artefatos precedentes. A comparação quantitativa diz respeito a desempenho de instâncias de Framework, enquanto que a qualitativa sobre facilidades de suas composições em relação ao conjunto interface e Framework PON. / The Emerging Notification Oriented Paradigm (NOP) is materialized in a Framework developed in the C++ language programming. The NOP Framework was designed to provide an Application Programming Interface (API) and high-level structures that would facilitate the development of software according to their orientation. However, this implies to a computational processing overhead of each NOP application. Still, an embryonic friendly Interface called Wizard was designed to provide high-level resource for the development of certain NOP applications. Thus, this work proposes a new version of materialization of NOP Framework and the evolution of its Wizard Interface. At the end, these are validated by quantitative and qualitative comparisons, in a relation to its previous artifacts. The quantitative comparisons are referent of the performance to the Framework instances, whereas the qualitative comparisons are about the facilities of yours compositions.

O emergente Paradigma Orientado a Notificações (PON) está materializado em um Framework desenvolvido na linguagem de programação C++. Este foi projetado para fornecer uma Application Programming Interface (API) e estruturas de alto nível que facilitasse o desenvolvimento de software segundo sua orientação. Entretanto, isto induz a uma sobrecarga de processamento computacional em cada aplicação PON. Ainda, uma embrionária interface amigável denominada Wizard foi concebida para prover recursos de alto nível para o desenvolvimento de certas aplicações PON. Assim, este trabalho propõe uma nova materialização do Framework PON e a evolução de sua interface Wizard. Ao final, estes são validados por meio de comparações quantitativas e qualitativas em relação aos seus artefatos precedentes. A comparação quantitativa diz respeito a desempenho de instâncias de Framework, enquanto que a qualitativa sobre facilidades de suas composições em relação ao conjunto interface e Framework PON. / The Emerging Notification Oriented Paradigm (NOP) is materialized in a Framework developed in the C++ language programming. The NOP Framework was designed to provide an Application Programming Interface (API) and high-level structures that would facilitate the development of software according to their orientation. However, this implies to a computational processing overhead of each NOP application. Still, an embryonic friendly Interface called Wizard was designed to provide high-level resource for the development of certain NOP applications. Thus, this work proposes a new version of materialization of NOP Framework and the evolution of its Wizard Interface. At the end, these are validated by quantitative and qualitative comparisons, in a relation to its previous artifacts. The quantitative comparisons are referent of the performance to the Framework instances, whereas the qualitative comparisons are about the facilities of yours compositions.

Cette thèse s’intéresse à la sémantique dénotationnelle (en théorie desmodèles et en théorie des jeux) de quatre langages de programmation logique: - LP, le plus restrictif de tous, - DLP, une extension de LP aux disjonctions, - LPN, une extension de LP aux négations, et - DLPN, qui inclut les deux.Ce manuscrit apporte trois contributions principales:(1) Un cadre abstrait pour la sémantique de la programmation logique yest défini, et toutes les approches sémantiques que nous étudions par lasuite prennent place dans ce cadre.Nous définissons la notion générale d'espace de valeurs de vérité commeune structure algébrique spécifique, satisfaisant un certain ensembled'axiomes. Les booléens forment l'exemple canonique d'un tel espace,mais nous devons étudier des cas plus généraux si nous voulonsconsidérer la "négation par l'échec". Pour cela, nous définissons etétudions une famille infinie d'espaces, paramétrée par un ordinal.(2) Une sémantique des jeux pour LP a été définie en 1986, et son étudea été approfondie en 1998. Elle a ensuite été étendue au cas desprogrammes LPN en 2005.Ici nous développons en détails une sémantique pour les programmes DLP.Nous prouvons qu'elle est correcte et complète par rapport aux modèlesminimaux de Minker.(3) Nous définissons un opérateur sémantique qui, étant donnée une sémantique abstraite d'un langage non disjonctif, la transforme en une sémantique disjonctive associée.La correction de cette transformation découle du fait qu'elle conserveles équivalences de sémantiques.Nous en présentons ensuite quelques applications qui permettent, entre autres, d'obtenir la première sémantique des jeux pour DLPN. / In this thesis, we study denotational semantics (model-theoretic andgame-theoretic) of four logic programming languages:- LP which is the most restrictive one;- DLP which extends LP by allowing disjunctions;- LPN which extends LP by allowing negations; and- DLPN which allows both.The three main contributions of this dissertation can be summarized as follows:(1) An abstract framework for logic programming semantics is definedand all semantic approaches that we study are placed within this framework.We define the general notion of a truth value space as an appropriate algebraicstructure that satisfies a set of axioms.The booleans form the canonical example of such a space, but we need toconsider much more general ones when dealing with negation-as-failure. Forthis we define and study an infinite family of spaces, parametrized over anordinal number.(2) A game semantics for LP was defined in 1986 and further studied in 1998.Then in 2005 it was extended for the case of LPN programs.Here a game semantics for DLP programs is developed in full detail; we provethat it is sound and complete with respect to the standard, minimal modelssemantics of Minker.(3) We define a semantic operator which transforms any given abstractsemantics of a non-disjunctive language to a semantics of the"corresponding" disjunctive one. We exhibit the correctness of thistransformation by proving that it preserves equivalences of semantics,and we present some applications of it, obtaining new game semantics forDLPN, among others.

Submitted by Irene Nascimento (irene.kessia@ufpe.br) on 2016-10-17T18:29:55Z No. of bitstreams: 2 license_rdf: 1232 bytes, checksum: 66e71c371cc565284e70f40736c94386 (MD5) phd_efsb_FINAL_BIBLIOTECA.pdf: 7882904 bytes, checksum: df094c44eb4ce5be12596263047790ed (MD5) / Made available in DSpace on 2016-10-17T18:29:55Z (GMT). No. of bitstreams: 2 license_rdf: 1232 bytes, checksum: 66e71c371cc565284e70f40736c94386 (MD5) phd_efsb_FINAL_BIBLIOTECA.pdf: 7882904 bytes, checksum: df094c44eb4ce5be12596263047790ed (MD5) Previous issue date: 2016-08-29 / FACEPE / Context: In Software Engineering, technology transfer has been treated as a problem that concernsonly two agents (innovation and adoption agents) working together to fill the knowledge gap between them. In this scenario, the transfer is carried out in a “peer-to-peer” fashion, not changing the reality of individuals and organizations around them. This approach works well when one is just seeking the adoption of a technology by a“specific client”. However, it can not solve a common problem that is the adoption of new technologies by a large mass of potential new users. In a wider context like this, it no longer makes sense to focus on “peer-to-peer” transfer. A new way of looking at the problem is necessary. It makes more sense to approach it as diffusion of innovations, where there is an information spreading in a community, similar to that observed in epidemics. Objective: This thesis proposes a paradigm shift to show the adoption of programming languages can be formally addressed as an epidemic. This focus shift allows the dynamics of programming language adoption to be mathematically modelled as such, and besides finding models that explain the community’s behaviour when adopting programming languages, it allows some predictions to be made, helping both individuals who wish to adopt a new language that might seem to be a new industry standard, and language designers to understand in real time the adoption of a particular language by a community. Method: After a proof of concept with data from Sourceforge (2000 to 2009), data from GitHub (2009 to January 2016), a well-known open source software repository, and Stack Overflow (2008 to March 2016), a popular Q&A system for software developers, were obtained and preprocessed. Using cumulative biological growth functions, often used in epidemiological contexts, we obtained adjusted models to the data. Once with the adjusted models, we evaluated their predictive capabilities through repeated applications of hypothesis testing and statistical calculations in different versions of the models obtained after adjusting the functions to samples of different time frames from the repositories. Results: We show that programming language adoption can be formally considered an epidemiological phenomenon by adjusting a well-known mathematical function used to describe such phenomena. We also show that, using the models found, it is possible to forecast programming languages adoption. We also show that it is possible to have similar insights by observing user data, as well as data from the community itself, not using software developers as susceptible individuals. Limitations: The forecast of the adoption outcome (asymptote) needs to be taken with care because it varies depending on the sample size, which also influences the quality of forecasts in general. Unfortunately, we not always have control over the sample size, because it depends on the population under analysis. The forecast of programming language adoption is only valid for the analysed population; generalizations should be made with caution. Conclusion: Addressing programming languages adoption as an epidemiological phenomenon allows us to perform analyses not possible otherwise. We can have an overview of a population in real time regarding the use of a programming language, which allows us, as innovation agents, to adjust our technology if it is not achieving the desired “penetration”; as adoption agents, we may decide, ahead of our competitors, to adopt a seemingly promising technology that may ultimately become a standard. / Contexto: Em Engenharia de Software, transferência de tecnologia tem sido tratada como um problema pontual, um processo que diz respeito a dois agentes (os agentes de inovação e adoção) trabalhando juntos para preencher uma lacuna no conhecimento entre estes dois. Neste cenário, a transferência é realizada “ponto a ponto”, envolvendo e tendo efeito apenas nos indivíduos que participam do processo. Esta abordagem funciona bem quando se está buscando apenas a adoção da tecnologia por um “cliente” específico. No entanto, ela não consegue resolver um problema bastante comum que é a adoção de novas tecnologias por uma grande massa de potenciais novos usuários. Neste contexto mais amplo, não faz mais sentido focar em transferência ponto a ponto, faz-se necessária uma nova maneira de olhar para o problema. É mais interessante abordá-lo como difusão de inovações, onde existe um espalhamento da informação em uma comunidade, de maneira semelhante ao que se observa em epidemias. Objetivo: Esta tese de doutorado mostra que a adoção de linguagens de programação pode ser tratada formalmente como uma epidemia. Esta mudança conceitual na maneira de olhar para o fenômeno permite que a dinâmica da adoção de linguagens de programação seja modelada matematicamente como tal, e além de encontrar modelos que expliquem o comportamento da comunidade quando da adoção de uma linguagem de programação, permite que algumas previsões sejam realizadas, ajudando tanto indivíduos que desejem adotar uma nova linguagem que parece se apresentar como um novo padrão industrial, quanto ajudando projetistas de linguagens a entender em tempo real a adoção de uma determinada linguagem pela comunidade. Método: Após uma prova de conceito com dados do Sourceforge (2000 a 2009), dados do GitHub (2009 a janeiro de 2016) um repositório de projetos software de código aberto, e Stack Overflow (2008 a março de 2016) um popular sistema de perguntas e respostas para desenvolvedores de software, from obtidos e pré processados. Utilizando uma função de crescimento biológico cumulativo, frequentemente usada em contextos epidemiológicos, obtivemos modelos ajustados aos dados. Uma vez com os modelos ajustados, realizamos avaliações de sua precisão. Avaliamos suas capacidades de previsão através de repetidas aplicações de testes de hipóteses e cálculos de estatísticas em diferentes versões dos modelos, obtidas após ajustes das funções a amostras de diferentes tamanhos dos dados obtidos. Resultados: Mostramos que a adoção de linguagens de programação pode ser considerada formalmente um fenômeno epidemiológico através do ajuste de uma função matemática reconhecidamente útil para descrever tais fenômenos. Mostramos também que é possível, utilizando os modelos encontrados, realizar previsões da adoção de linguagens de programação em uma determinada comunidade. Ainda, mostramos que é possível obter conclusões semelhantes observando dados de usuários e dados da comunidade apenas, não usando desenvolvedores de software como indivíduos suscetíveis. Limitações: A previsão do limite superior da adoção (assíntota) não é confiável, variando muito dependendo do tamanho da amostra, que também influencia na qualidade das previsões em geral. Infelizmente, nem sempre teremos controle sob o tamanho da amostra, pois ela depende da população em análise. A adoção da linguagem de programação só é válida para a população em análise; generalizações devem ser realizadas com cautela. Conclusão: Abordar o fenômeno de adoção de linguagens de programação como um fenômeno epidemiológico nos permite realizar análises que não são possíveis de outro modo. Podemos ter uma visão geral de uma população em tempo real no que diz respeito ao uso de uma linguagem de programação, o que nos permite, com agentes de inovação, ajustar a tecnologia caso ela não esteja alcançando o alcance desejado; como agentes de adoção, podemos decidir por adotar uma tecnologia aparentemente promissora que pode vir a se tornar um padrão.

Orientador: Hans Kurt Edmund Liesenberg / Dissertação (mestrado) - Universidade Estadual de Campinas, Instituto de Computação / Made available in DSpace on 2018-08-05T04:28:35Z (GMT). No. of bitstreams: 1 NevesJunior_Carlos_M.pdf: 1230174 bytes, checksum: d583db28ad2a79922429fb1cc37e40ca (MD5) Previous issue date: 2005 / Resumo: O objetivo do presente trabalho é o desenvolvimento do Gerente de Distribuição do ambiente de execução Xchart. O ambiente Xchart, tal como definido na tecnologia de mesmo nome, a Tecnologia Xchart, é composto por um conjunto de ferramentas que apóiam o desenvolvimento de gerenciadores de diálogo de interfaces de usuário. A especificação destes gerenciadores de diálogo é modular e com semântica prevendo a execução concorrente de seus componentes, o que permitiria a distribuição de tais componentes por uma rede de computadores. Xchart também dá nome à linguagem visual empregada na especificação e captura do controle de diálogo destas interfaces, e o fato de Xchart ser uma variante de Statecharts permite que a linguagem seja utilizada em um domínio maior, o domínio de sistemas reativos distribuídos. O Gerente de Distribuição é o componente do sistema de execução de Xchart que fornece os recursos para a execução concorrente e distribuída destes sistemas reativos. O atual trabalho implementa este componente e o sistema de execução de Xchart com tecnologias disponíveis na plataforma Java 2 Platform, Enterprise Edition (J2EE). J2EE é uma especificação de plataforma para desenvolvimento de aplicações corporativas distribuídas que oferece uma série de recursos tais como serviço de nomes e diretório, sistema de entrega de mensagens e mecanismos para controle de concorrência como gerenciamento de transações atômicas. O emprego de J2EE no desenvolvimento do ambiente Xchart visa reduzir o esforço de implementação destas funcionalidades típicas de sistemas distribuídos, além de aproveitar outros benefícios da linguagem JavaTM como a independência de plataforma / Abstract: The aim of the current project is the development of the Distribution Manager of the Xchart runtime environment. The Xchart environment as defined by the Xchart technology is composed by a set of tools that supports the development of dialogue managers of user interfaces. The specification of these dialogue managers is modular and describes the concurrent execution of these components, which allows a potential distribution of these components over a computer network. Xchart is also the name of the visual language used to specify and capture the dialogue control of user interfaces, and since Xchart is a variant of Statecharts, it can be applied in a major domain: the domain of the distributed reactive systems. The Distribution Manager is the component of this Xchart runtime system that provides the resources for concurrent and distributed execution of these reactive systems. The current project implements this component and the Xchart runtime system using available technologies of the Java 2 Platform, Enterprise Edition (J2EE). J2EE is a specification of platform for development of distributed enterprise applications that offers a set of resources like naming and directory services, message service and a concurrency control mechanism based on atomic transaction management. Some of the benefits on using J2EE technology for the development of the Xchart environment are the reduction of the efforts typically required by the implementation of regular distributed systems algorithms and also the platform independence model provided by Java / Mestrado / Sistemas de Computação / Mestre em Ciência da Computação

[pt] Ambientes de Execução Gerenciada tornaram-se alvos populares para compiladores de linguagens de programação de alto nível. Eles provêem um sistema tipos de alto nível com segurança de memória garantida, assim como facilidades como coleta de lixo, acesso a serviços da plataforma subjacente (possivelmente através de uma sandbox), multithreading, e uma rica biblioteca de estruturas de dados e algorithmos, mas não possuem um modelo de desempenho claro, o que atrapalha as tentativas de otimização de qualquer linguagem que não tenha um mapeamento direto na semântica do ambiente de execução, especialmente se a linguagem é dinamicamente tipada. Nós afirmamos que é possível construir um compilador para uma linguagem dinâmica que tem como alvo um ambiente de execução gerenciada que rivaliza um compilador que tem como alvo linguagem de máquina na eficiência do código que ele gera. Essa tese apresenta um compilador com tal característica, descrevendo as otimizações necessárias para sua construção, e testes de desempenho que validam essas otimizações. Nossas otimizações não dependem de geração de código em tempo de execução, apenas em informação estaticamente disponível no código fonte. Nós usamos uma nova análise de inferência de tipos para aumentar a quantidade de informação disponível. / [en] Managed runtime environments have become popular targets for compilers of high-level programming languages. They provide a high-level type system with enforced runtime safety, as well as facilities such as garbage collection, possibility sandboxed access to services of the underlying platform, multithreadng, and a rich library of data structures and algorithms. But managed runtime environments lack a clear performance model, which hinders attempts ar optimizing the compilation of any language that does nor have a direct mapping to the runtime environments semantics. This is aggravated if the language is dynamically typed. We assert that it is possible to build a compiler for a dynamic language that targets a managed runtime environment so that it rivals a compiler that targets machine code directly in efficiency of the code it generates. This dissertation presents such a compiler, describing the optimizations that were needed to build it, and benchmarks that validate these optimizations. Our optimizations do not depend on runtime code generation, only on information that is statically available from the source program. We use a novel type inference analysis to increase the amount of information available.

No description available.

Une pression accrue s'exerce sur les compilateurs pour mettre en œuvre des transformations de programmes de plus en plus complexes délivrant le potentiel de performance des processeurs multicœurs et des accélérateurs hétérogènes. L'espace de recherche des optimisations de programmes possibles est gigantesque est manque de structure. La recherche de la meilleure transformation, qui inclut la prédiction des gains estimés de performance offerts par cette transformation, constitue le problème le plus difficiles pour les compilateurs optimisants modernes. Nous avons choisi de nous concentrer sur les transformations de boucles et sur leur automatisation, exprimées dans le modèle polyédrique. Les méthodes d'optimisation de programmes dans le modèle polyédrique se répartissent grossièrement en deux classes. La première repose sur l'optimisation linéaire d'une fonction de analytique de coût. La deuxième classe de méthodes met en œuvre une recherche itérative. La première approche est rapide, mais elle est facilement mise en défaut en ce qui concerne la découverte de la solution optimale. L'approche itérative est plus précise, mais le temps de compilation peut devenir prohibitif. Cette thèse contribue une approche nouvelle de la recherche itérative de transformations de programmes dans le modèle polyédrique. La nouvelle méthode proposée possède la précision et la capacité effective à extraire des transformations profitables des méthodes itératives, tout en en minimisant les faiblesses. Notre approche repose sur l'évaluation systématique d'une fonction de coût et de prédiction de performances non-linéaire. Par ailleurs, la parallélisation automatique dans le modèle polyédrique est actuellement dominée par des outils de compilation source-à-source. Nous avons choisi au contraire d'implémenter nos techniques dans la plateforme GCC, en opérant sur une représentation de code de bas niveau, à trois adresses. Nous montrons que le niveau d'abstraction de la représentation intermédiaire choisie engendre des difficultés de passage à l'échelle, et nous montrons comment les surmonter. À l'inverse, nous montrons qu'une représentation intermédiaire de bas niveau ouvre de nouveaux degrés de liberté, bénéficiant à notre stratégie itérative de recherche de transformations, et à la compilation polyédrique de manière générale. / In order to take the performance advantages of the current multicore and heterogeneous architectures the compilers are required to perform more and more complex program transformations. The search space of the possible program optimizations is huge and unstructured. Selecting the best transformation and predicting the potential performance benefits of that transformation is the major problem in today's optimizing compilers. The promising approach to handling the program optimizations is to focus on the automatic loop optimizations expressed in the polyhedral model. The current approaches for optimizing programs in the polyhedral model broadly fall into two classes. The first class of the methods is based on the linear optimization of the analytical cost function. The second class is based on the exhaustive iterative search. While the first approach is fast, it can easily miss the optimal solution. The iterative approach is more precise, but its running time might be prohibitively expensive. In this thesis we present a novel search-based approach to program transformations in the polyhedral model. The new method combines the benefits - effectiveness and precision - of the current approaches, while it tries to minimize their drawbacks. Our approach is based on enumerating the evaluations of the precise, nonlinear performance predicting cost-function. The current practice is to use the polyhedral model in the context of source-to-source compilers. We have implemented our techniques in a GCC framework that is based on the low level three address code representation. We show that the chosen level of abstraction for the intermediate representation poses scalability challenges, and we show the ways to overcome those problems. On the other hand, it is shown that the low level IR abstraction opens new degrees of freedom that are beneficial for the search-based transformation strategies and for the polyhedral compilation in general.

La vérification déductive de programmes consiste à annoter des programmes par une spécification, c'est-à-dire un ensemble de formules logiques décrivant le comportement du programme, et à prouver que les programmes vérifient bien leur spécification. Des outils tels que la plate-forme Why prennent en entrée un programme et sa spécification et calculent des formules logiques telles que, si elles sont prouvées, le programme vérifie sa spécification. Ces formules logiques peuvent être prouvées automatiquement ou à l'aide d'assistants de preuve.Lorsqu'un programme est écrit dans un langage supportant les alias de pointeurs, c'est-à-dire si plusieurs variables peuvent désigner la même case mémoire, alors le raisonnement sur le programme devient particulièrement ardu. Il est nécessaire de spécifier quels pointeurs peuvent être égaux ou non. Les invariants des structures de données, en particulier, sont plus difficiles à vérifier.Cette thèse propose un système de type permettant de structurer la mémoire de façon modulaire afin de contrôler les alias de pointeurs et les invariants de données. Il est basé sur les notions de région et de permission. Les programmes sont ensuite interprétés vers Why de telle façon que les pointeurs soient séparés au mieux, facilitant ainsi le raisonnement. Cette thèse propose aussi un mécanisme d'inférence permettant d'alléger le travail d'annotation des opérations de régions introduites par le langage. Un modèle est introduit pour décrire la sémantique du langage et prouver sa sûreté. En particulier, il est prouvé que si le type d'un pointeur affirme que celui-ci vérifie son invariant, alors cet invariant est effectivement vérifié dans le modèle. Cette thèse a fait l'objet d'une implémentation sous la forme d'un outil nommé Capucine. Plusieurs exemples ont été écrits pour illustrer le langage, et ont été vérifié à l'aide de Capucine. / Deductive verification consists in annotating programs by a specification, i.e. logic formulas which describe the behavior of the program, and prove that programs verify their specification. Tools such as the Why platform take a program and its specification as input and compute logic formulas such that, if they are valid, the program verifies its specification. These logic formulas can be proven automatically or using proof assistants.When a program is written in a language supporting pointer aliasing, i.e. if several variables may denote the same memory cell, then reasoning about the program becomes particularly tricky. It is necessary to specify which pointers may or may not be equal. Invariants of data structures, in particular, are harder to maintain.This thesis proposes a type system which allows to structure the heap in a modular fashion in order to control pointer aliases and data invariants. It is based on the notions of region and permission. Programs are then translated to Why such that pointers are separated as best as possible, to facilitate reasoning. This thesis also proposes an inference mechanism to alleviate the need to write region operations introduced by the language. A model is introduced to describe the semantics of the language and prove its safety. In particular, it is proven that if the type of a pointer tells that its invariant holds, then this invariant indeed holds in the model. This work has been implemented as a tool named Capucine. Several examples have been written to illustrate the language, and where verified using Capucine.