In a software life-cycle Source code repositories serve as vast storage areas for program code, ensuring its maintenance and version control throughout the development process. It is not uncommon for these repositories to house programs with hidden errors, which only manifest under specific input conditions, causing the program to deviate from its intended functionality. The growing intricacy of software design has amplified the time and resources required to pinpoint and rectify these issues. These errors, often unintended by developers, can be challenging to identify and correct. While there are techniques to auto-correct faulty code, the expansive realm of potential solutions for a single bug means there's a scarcity of tools and datasets for effective evaluation of the corrected code. This study presents FIXEVAL, a benchmark that includes flawed code entries from competitive coding challenges and their corresponding corrections. FIXEVAL offers an extensive test suite that not only gauges the accuracy of fixes generated by models but also allows for the assessment of a program's functional correctness. This suite further sheds light on time, memory limits, and acceptance based on specific outcomes. We utilize cutting-edge language models, trained on coding languages, as our reference point and juxtapose them using match-based (essentially token similarity) and execution-based (focusing on functional assessment) criteria. Our research indicates that while match-based criteria might not truly represent the functional precision of fixes generated by models, execution-based approaches offer a comprehensive evaluation tailored to the solution. Consequently, we posit that FIXEVAL paves the way for practical automated error correction and assessment of code generated by models. Dataset and models for all of our experiments are made publicly available at https://github.com/mahimanzum/FixEval. / Master of Science / Think of source code repositories as big digital libraries where computer programs are kept safe and updated. Sometimes, these programs have hidden mistakes that only show up under certain conditions, making the program act differently than planned which we call bugs or errors. As software gets more complex, it takes more time and effort to find and fix these mistakes. Even though there are ways to automatically fix these errors, finding the best solution can be like looking for a needle in a haystack. That's why there aren't many tools to check if the automatic fixes are right. Enter FIXEVAL: our new tool that tests and compares faulty computer code from coding competitions and their fixes. It has a set of tests to see how well the fixed code works and gives insights into its performance and results. We used the latest computer language tools to see how well they fix code, comparing them in two ways: by looking at the code's structure and by testing its function. Our findings? Just looking at the code's structure isn't enough; we need to test how it works in action. We believe FIXEVAL is a big step forward in making sure automatic code fixes are spot-on. Dataset and models for all of our experiments are made publicly available at https://github.com/mahimanzum/FixEval.

<p>Binary analysis, a cornerstone technique in cybersecurity, enables the examination of binary executables, irrespective of source code availability.</p> <p>It plays a critical role in understanding program behaviors, detecting software bugs, and mitigating potential vulnerabilities, specially in situations where the source code remains out of reach.</p> <p>However, aligning the efficacy of binary analysis with that of source-level analysis remains a significant challenge, primarily due to the uncertainty caused by the loss of semantic information during the compilation process.</p> <p><br></p> <p>This dissertation presents an innovative probabilistic approach, termed as <em>probabilistic binary analysis</em>, designed to combat the intrinsic uncertainty in binary analysis.</p> <p>It builds on the fundamental principles of program sampling and probabilistic inference, enhanced further by an iterative refinement architecture.</p> <p>The dissertation suggests that a thorough and practical method of sampling program behaviors can yield a substantial quantity of hints which could be instrumental in recovering lost information, despite the potential inclusion of some inaccuracies.</p> <p>Consequently, a probabilistic inference technique is applied to systematically incorporate and process the collected hints, suppressing the incorrect ones, thereby enabling the interpretation of high-level semantics.</p> <p>Furthermore, an iterative refinement mechanism is deployed to augment the efficiency of the probabilistic analysis in subsequent applications, facilitating the progressive enhancement of analysis outcomes through an automated or human-guided feedback loop.</p> <p><br></p> <p>This work offers an in-depth understanding of the challenges and solutions related to assessing low-level program representations and systematically handling the inherent uncertainty in binary analysis. </p> <p>It aims to contribute to the field by advancing the development of precise, reliable, and interpretable binary analysis solutions, thereby setting the groundwork for future exploration in this domain.</p>

<p>Static program analyzers are vital tools to produce useful insights about programs without executing these programs. These insights can be used to improve the quality of programs, e.g., detecting defects in programs, or optimizing programs to use fewer resources. However, building static program analyzers that are simultaneously sound, performant, and flexible is notoriously challenging.</p> <p>This dissertation aims to address this challenge by exploring the potential of applying correct-by-construction metaprogramming techniques to build static program analyzers. Metaprogramming techniques manipulate and transform programs as data objects.  In this thesis, we consider static program analyzers as the objects to be manipulated or transformed. We show that metaprogramming techniques can improve our understanding, the construction, flexibility, and performance of program analyzers.</p> <p>We first study the inter-derivation of abstract interpreters. Using off-the-shelf program transformation techniques such as refunctionalization, we demonstrate that big-step abstract interpreters can be mechanically derived from their small-step counterparts, thus building a functional correspondence between two different styles of abstract interpretation.</p> <p>To build high-performance program analyzers, we exploit the first Futamura projection to build compilers for abstract interpretation and symbolic execution. The first Futamura projection states that specializing an interpreter with respect to an input program is a process equivalent to compilation, thus providing a practical way to repurpose interpreters for compilation and code generation. We systematically apply this idea to build program-analysis compilers by writing analyzers as staged interpreters using higher-level abstractions. The staged interpreter can be used for generating sound and performant analysis code given a specific input program. Moreover, the approach enables using abstractions without regret: by using higher-level program abstractions, the analyzer can be written in a way that is close to its high-level specification (e.g. big-step operational semantics), and by compilation, the analyzer is performant since it does not need to pay the runtime overhead of using these abstraction mechanisms.</p> <p>We also develop novel type systems that track sharing and separation in higher-order imperative languages. Such type systems are useful both for general-purpose programming languages and for optimization of domain-specific metaprograms such as those program-analysis compilers.</p> <p><br></p>

<p dir="ltr">Proof assistants based on dependent types are powerful tools for building certified software. In order to verify programs written in a different language, however, a representation of those programs in the proof assistant is required. When that language is sufficiently similar to that of the proof assistant, one solution is to use a <i>shallow embedding</i> to directly encode source programs as programs in the proof assistant. One challenge with this approach is ensuring that any semantic gaps between the two languages are accounted for. In this thesis, we present <i>GSet</i>, a mixed embedding that bridges the gap between OCaml GADTs and inductive datatypes in Coq. This embedding retains the rich typing information of GADTs while also allowing pattern matching with impossible branches to be translated without additional axioms. We formalize this with GADTml, a minimal calculus that captures GADTs in OCaml, and gCIC, an impredicative variant of the Calculus of Inductive Constructions. Furthermore, we present the translation algorithm between GADTml and gCIC, together with a proof of the soundness of this translation. We have integrated this technique into coq-of-ocaml, a tool for automatically translating OCaml programs into Coq. Finally, we demonstrate the feasibility of our approach by using our enhanced version of coq-of-ocaml, to translate a portion of the Tezos code base into Coq.</p>

Made available in DSpace on 2014-12-17T15:47:58Z (GMT). No. of bitstreams: 1 HeitorMAC_DISSERT.pdf: 3258229 bytes, checksum: 5f7856b140a636bd052147c58ff9dede (MD5) Previous issue date: 2011-03-01 / Coordena??o de Aperfei?oamento de Pessoal de N?vel Superior / Through the adoption of the software product line (SPL) approach, several benefits are achieved when compared to the conventional development processes that are based on creating a single software system at a time. The process of developing a SPL differs from traditional software construction, since it has two essential phases: the domain engineering - when common and variables elements of the SPL are defined and implemented; and the application engineering - when one or more applications (specific products) are derived from the reuse of artifacts created in the domain engineering. The test activity is also fundamental and aims to detect defects in the artifacts produced in SPL development. However, the characteristics of an SPL bring new challenges to this activity that must be considered. Several approaches have been recently proposed for the testing process of product lines, but they have been shown limited and have only provided general guidelines. In addition, there is also a lack of tools to support the variability management and customization of automated case tests for SPLs. In this context, this dissertation has the goal of proposing a systematic approach to software product line testing. The approach offers: (i) automated SPL test strategies to be applied in the domain and application engineering, (ii) explicit guidelines to support the implementation and reuse of automated test cases at the unit, integration and system levels in domain and application engineering; and (iii) tooling support for automating the variability management and customization of test cases. The approach is evaluated through its application in a software product line for web systems. The results of this work have shown that the proposed approach can help the developers to deal with the challenges imposed by the characteristics of SPLs during the testing process / Com o uso da abordagem de linhas de produto de software (LPSs), v?rios benef?cios s?o alcan?ados quando comparados aos processos de desenvolvimento convencionais que se baseiam na cria??o de um ?nico sistema por vez. O processo de desenvolvimento de uma LPS se diferencia da constru??o tradicional de software, uma vez que apresenta duas etapas essenciais: a engenharia de dom?nio - quando elementos comuns e vari?veis da LPS s?o definidos e implementados; e a engenharia de aplica??o quando uma ou mais aplica??es (produtos espec?ficos) s?o derivadas a partir do reuso dos artefatos criados na engenharia de dom?nio. Durante a elabora??o da LPS, assim como no desenvolvimento convencional de sistemas, a atividade de teste ? fundamental e tem como objetivo a detec??o de defeitos nos artefatos produzidos. Contudo, as caracter?sticas de uma LPS trazem novos desafios a essa atividade e que precisam ser considerados. Diversas abordagens foram propostas para o processo de teste de linhas de produto, mas elas se mostram limitadas ou fornecem diretrizes muito gerais. Outro fator preocupante ? a escassez de ferramentas que auxiliem na implementa??o, aplica??o e acompanhamento dos testes, bem como na ger?ncia e customiza??o de tais artefatos. Com base nesse contexto relacionado ao processo de teste de LPSs, esta disserta??o tem como objetivo propor uma abordagem sistem?tica para o teste de linhas de produto de software. A abordagem oferece: (i) estrat?gias de testes automatizados para LPSs tanto na engenharia de dom?nio quanto de aplica??o; (ii) diretrizes para a implementa??o e reuso de casos de teste automatizados nos n?veis de unidade, integra??o e sistema tanto para a engenharia de dom?nio quanto de aplica??o; e (iii) suporte ferramental para ger?ncia e customiza??o autom?tica de casos de teste usando t?cnicas de deriva??o autom?tica de software. A abordagem ? avaliada atrav?s da sua aplica??o em uma linha de produto para sistemas web. Os resultados deste trabalho mostram que a abordagem proposta pode ajudar os desenvolvedores a lidar com os desafios impostos pelas caracter?sticas das LPSs durante o processo de testes

Made available in DSpace on 2014-12-17T15:48:03Z (GMT). No. of bitstreams: 1 AlexandreSGV_DISSERT.pdf: 2732563 bytes, checksum: ab07c81d7e941ed2d721415180865feb (MD5) Previous issue date: 2012-05-25 / Conselho Nacional de Desenvolvimento Cient?fico e Tecnol?gico / Software Products Lines (SPL) is a software engineering approach to developing software system families that share common features and differ in other features according to the requested software systems. The adoption of the SPL approach can promote several benefits such as cost reduction, product quality, productivity, and time to market. On the other hand, the SPL approach brings new challenges to the software evolution that must be considered. Recent research work has explored and proposed automated approaches based on code analysis and traceability techniques for change impact analysis in the context of SPL development. There are existing limitations concerning these approaches such as the customization of the analysis functionalities to address different strategies for change impact analysis, and the change impact analysis of fine-grained variability. This dissertation proposes a change impact analysis tool for SPL development, called Squid Impact Analyzer. The tool allows the implementation of change impact analysis based on information from variability modeling, mapping of variability to code assets, and existing dependency relationships between code assets. An assessment of the tool is conducted through an experiment that compare the change impact analysis results provided by the tool with real changes applied to several evolution releases from a SPL for media management in mobile devices / Linhas de Produtos de Software (LPS) consiste em um paradigma de desenvolvimento de software, no qual fam?lias de sistemas compartilham caracter?sticas comuns e tornam expl?citas outras caracter?sticas que variam de acordo com o sistema final sendo considerado. Esta abordagem oferece benef?cios ao desenvolvimento de software como redu??o de custos, qualidade do produto final, produtividade e tempo de desenvolvimento reduzido. Por outro lado, a abordagem imp?e novos desafios para a atividade de evolu??o dos artefatos que modelam e implementam a LPS. Trabalhos de pesquisa recentes prop?em abordagens com suporte automatizado de ferramentas de an?lise de impacto de mudan?a no contexto de evolu??o de LPSs. Tais abordagens s?o baseadas em t?cnicas de an?lise de impacto de mudan?as e rastreabilidade de artefatos, por?m apresentam limita??es quanto ? an?lise de impacto de mudan?as em variabilidades de granularidade fina, bem como ? customiza??o dos tipos e estrat?gias de an?lise realizadas. Esta disserta??o prop?e uma ferramenta de an?lise de impacto de mudan?a, denominada Squid Impact Analyzer, que utiliza uma estrat?gia de estimativa de impacto baseada em informa??es de caracter?sticas, mapeamento de tais caracter?sticas em artefatos de c?digo, e depend?ncia existente entre artefatos de implementa??o. A ferramenta ? avaliada atrav?s da condu??o de experimentos que realizam a quantifica??o de m?tricas de cobertura, precis?o e m?dia harm?nica nos resultados de buscas de an?lise de impacto de mudan?a da ferramenta proposta em contraposi??o ?s mudan?as reais realizadas nos artefatos de diversas vers?es de evolu??o de uma LPS para gerenciamento de m?dias em dispositivos m?veis. A ferramenta foi desenvolvida com base em uma infraestrutura que serve de base para a instancia??o de ferramentas de an?lise de propriedades de c?digo de LPSs, e que ? tamb?m parte da contribui??o da disserta??o

Made available in DSpace on 2014-12-17T15:48:08Z (GMT). No. of bitstreams: 1 EdmilsonBCN_DISSERT.pdf: 2688212 bytes, checksum: bae476692f237de556a79c9741333002 (MD5) Previous issue date: 2013-08-05 / The software systems development with domain-specific languages has become increasingly common. Domain-specific languages (DSLs) provide increased of the domain expressiveness, raising the abstraction level by facilitating the generation of models or low-level source code, thus increasing the productivity of systems development. Consequently, methods for the development of software product lines and software system families have also proposed the adoption of domain-specific languages. Recent studies have investigated the limitations of feature model expressiveness and proposing the use of DSLs as a complement or substitute for feature model. However, in complex projects, a single DSL is often insufficient to represent the different views and perspectives of development, being necessary to work with multiple DSLs. In order to address new challenges in this context, such as the management of consistency between DSLs, and the need to methods and tools that support the development with multiple DSLs, over the past years, several approaches have been proposed for the development of generative approaches. However, none of them considers matters relating to the composition of DSLs. Thus, with the aim to address this problem, the main objectives of this dissertation are: (i) to investigate the adoption of the integrated use of feature models and DSLs during the domain and application engineering of the development of generative approaches; (ii) to propose a method for the development of generative approaches with composition DSLs; and (iii) to investigate and evaluate the usage of modern technology based on models driven engineering to implement strategies of integration between feature models and composition of DSLs / A utiliza??o de linguagens espec?ficas de dom?nios para o desenvolvimento de sistemas de software tem se tornado cada vez mais comum. Elas propiciam um aumento da expressividade do dom?nio, elevando o seu n?vel de abstra??o atrav?s de facilidades para gera??o de modelos ou c?digos de baixo-n?vel, que aumentam assim a produtividade do desenvolvimento de sistemas. Como consequ?ncia, m?todos para o desenvolvimento de linhas de produtos de software e fam?lias de sistemas tamb?m t?m proposto a utiliza??o de linguagens espec?ficas de dom?nio (domain-specific languages DSLs). Estudos recentes t?m investigado os limites de expressividade do modelo de features, e propondo o uso de DSLs em sua substitui??o ou complemento. Contudo, em projetos complexos, uma ?nica DSL muitas vezes ? insuficiente para representar as diferentes vis?es e perspectivas do desenvolvimento, sendo necess?rio trabalhar com m?ltiplas DSLs. Com isso surgem novos desafios, tais como a ger?ncia de consist?ncia entre as DSLs, e a necessidade de m?todos e ferramentas que ofere?am suporte ao desenvolvimento com m?ltiplas DSLs. Ao longo dos ?ltimos anos, diversas abordagens t?m sido propostas para o desenvolvimento de abordagens generativas, entretanto, nenhuma delas considera quest?es relacionadas ? composi??o de DSLs. Assim, visando abordar tal problem?tica, os principais objetivos desta disserta??o s?o: (i) investigar a ado??o do uso integrado de modelos de features e DSLs tanto na engenharia de dom?nio quanto de aplica??o de desenvolvimento de abordagens generativas; (ii) propor um m?todo para o desenvolvimento de abordagens generativas com composi??o de DSLs; e (iii) investigar e avaliar o uso de tecnologias atuais de engenharia dirigida por modelos na implementa??o de estrat?gias de integra??o entre modelos de features e composi??o de DSLs

<p>    </p> <p>Irregular control-flow structures like deeply nested conditional branches are common in real-world software applications. Improving the performance and efficiency of such programs is often challenging because it is difficult to analyze and optimize programs with irregular control flow. We observe that real-world programs contain similar or identical computations within different code paths of the conditional branches. Compilers can merge similar code to improve performance or code size. However, existing compiler optimizations like code hoisting/sinking, and tail merging do not fully exploit this opportunity. We propose a new technique called Control-Flow Melding (CFM) that can merge similar code sequences at the control-flow region level. We evaluate CFM in two applications. First, we show that CFM reduces the control divergence in GPU programs and improves the performance. Second, we apply CFM to CPU programs and show its effectiveness in reducing code size without sacrificing performance. In the next part of this dissertation, we investigate how CFM can be extended to improve dynamic test generation techniques like Dynamic Symbolic Execution (DSE). DSE suffers from path explosion problem when many conditional branches are present in the program. We propose a non-semantics-preserving branch elimination transformation called CFM-SE that reduces the number of symbolic branches in a program. We also provide a framework for detecting and reasoning about false positive bugs that might be added to the program by non-semantics-preserving transformations like CFM-SE. Furthermore, we evaluate CFM-SE on real-world applications and show its effectiveness in improving DSE performance and code coverage. </p>

Cette thèse a pour but d’améliorer l’automatisation dans l’ingénierie dirigée par les modèles (MDE pour Model Driven Engineering). MDE est un paradigme qui promet de réduire la complexité du logiciel par l’utilisation intensive de modèles et des transformations automatiques entre modèles (TM). D’une façon simplifiée, dans la vision du MDE, les spécialistes utilisent plusieurs modèles pour représenter un logiciel, et ils produisent le code source en transformant automatiquement ces modèles. Conséquemment, l’automatisation est un facteur clé et un principe fondateur de MDE. En plus des TM, d’autres activités ont besoin d’automatisation, e.g. la définition des langages de modélisation et la migration de logiciels. Dans ce contexte, la contribution principale de cette thèse est de proposer une approche générale pour améliorer l’automatisation du MDE. Notre approche est basée sur la recherche méta-heuristique guidée par les exemples. Nous appliquons cette approche sur deux problèmes importants de MDE, (1) la transformation des modèles et (2) la définition précise de langages de modélisation. Pour le premier problème, nous distinguons entre la transformation dans le contexte de la migration et les transformations générales entre modèles. Dans le cas de la migration, nous proposons une méthode de regroupement logiciel (Software Clustering) basée sur une méta-heuristique guidée par des exemples de regroupement. De la même façon, pour les transformations générales, nous apprenons des transformations entre modèles en utilisant un algorithme de programmation génétique qui s’inspire des exemples des transformations passées. Pour la définition précise de langages de modélisation, nous proposons une méthode basée sur une recherche méta-heuristique, qui dérive des règles de bonne formation pour les méta-modèles, avec l’objectif de bien discriminer entre modèles valides et invalides. Les études empiriques que nous avons menées, montrent que les approches proposées obtiennent des bons résultats tant quantitatifs que qualitatifs. Ceux-ci nous permettent de conclure que l’amélioration de l’automatisation du MDE en utilisant des méthodes de recherche méta-heuristique et des exemples peut contribuer à l’adoption plus large de MDE dans l’industrie à là venir. / This thesis aims to improve automation in Model Driven Engineering (MDE). MDE is a paradigm that promises to reduce software complexity by the mean of the intensive use of models and automatic model transformation (MT). Roughly speaking, in MDE vision, stakeholders use several models to represent the software, and produce source code by automatically transforming these models. Consequently, automation is a key factor and founding principle of MDE. In addition to MT, other MDE activities require automation, e.g. modeling language definition and software migration. In this context, the main contribution of this thesis is proposing a general approach for improving automation in MDE. Our approach is based on meta-heuristic search guided by examples. We apply our approach to two important MDE problems, (1) model transformation and (2) precise modeling languages. For transformations, we distinguish between transformations in the context of migration and general model transformations. In the case of migration, we propose a software clustering method based on a search algorithm guided by cluster examples. Similarly, for general transformations, we learn model transformations by a genetic programming algorithm taking inspiration from examples of past transformations. For the problem of precise metamodeling, we propose a meta-heuristic search method to derive well-formedness rules for metamodels with the objective of discriminating examples of valid and invalid models. Our empirical evaluation shows that the proposed approaches exhibit good results. These allow us to conclude that improving automation in MDE using meta-heuristic search and examples can contribute to a wider adoption of MDE in industry in the coming years.

Cette thèse a pour but d’améliorer l’automatisation dans l’ingénierie dirigée par les modèles (MDE pour Model Driven Engineering). MDE est un paradigme qui promet de réduire la complexité du logiciel par l’utilisation intensive de modèles et des transformations automatiques entre modèles (TM). D’une façon simplifiée, dans la vision du MDE, les spécialistes utilisent plusieurs modèles pour représenter un logiciel, et ils produisent le code source en transformant automatiquement ces modèles. Conséquemment, l’automatisation est un facteur clé et un principe fondateur de MDE. En plus des TM, d’autres activités ont besoin d’automatisation, e.g. la définition des langages de modélisation et la migration de logiciels. Dans ce contexte, la contribution principale de cette thèse est de proposer une approche générale pour améliorer l’automatisation du MDE. Notre approche est basée sur la recherche méta-heuristique guidée par les exemples. Nous appliquons cette approche sur deux problèmes importants de MDE, (1) la transformation des modèles et (2) la définition précise de langages de modélisation. Pour le premier problème, nous distinguons entre la transformation dans le contexte de la migration et les transformations générales entre modèles. Dans le cas de la migration, nous proposons une méthode de regroupement logiciel (Software Clustering) basée sur une méta-heuristique guidée par des exemples de regroupement. De la même façon, pour les transformations générales, nous apprenons des transformations entre modèles en utilisant un algorithme de programmation génétique qui s’inspire des exemples des transformations passées. Pour la définition précise de langages de modélisation, nous proposons une méthode basée sur une recherche méta-heuristique, qui dérive des règles de bonne formation pour les méta-modèles, avec l’objectif de bien discriminer entre modèles valides et invalides. Les études empiriques que nous avons menées, montrent que les approches proposées obtiennent des bons résultats tant quantitatifs que qualitatifs. Ceux-ci nous permettent de conclure que l’amélioration de l’automatisation du MDE en utilisant des méthodes de recherche méta-heuristique et des exemples peut contribuer à l’adoption plus large de MDE dans l’industrie à là venir. / This thesis aims to improve automation in Model Driven Engineering (MDE). MDE is a paradigm that promises to reduce software complexity by the mean of the intensive use of models and automatic model transformation (MT). Roughly speaking, in MDE vision, stakeholders use several models to represent the software, and produce source code by automatically transforming these models. Consequently, automation is a key factor and founding principle of MDE. In addition to MT, other MDE activities require automation, e.g. modeling language definition and software migration. In this context, the main contribution of this thesis is proposing a general approach for improving automation in MDE. Our approach is based on meta-heuristic search guided by examples. We apply our approach to two important MDE problems, (1) model transformation and (2) precise modeling languages. For transformations, we distinguish between transformations in the context of migration and general model transformations. In the case of migration, we propose a software clustering method based on a search algorithm guided by cluster examples. Similarly, for general transformations, we learn model transformations by a genetic programming algorithm taking inspiration from examples of past transformations. For the problem of precise metamodeling, we propose a meta-heuristic search method to derive well-formedness rules for metamodels with the objective of discriminating examples of valid and invalid models. Our empirical evaluation shows that the proposed approaches exhibit good results. These allow us to conclude that improving automation in MDE using meta-heuristic search and examples can contribute to a wider adoption of MDE in industry in the coming years.