Search

Fast numerical libraries have been a cornerstone of scientific computing for decades, but this comes at a price. Programs may be tied to vendor specific software ecosystems resulting in polluted, non-portable code. As we enter an era of heterogeneous computing, there is an explosion in the number of accelerator libraries required to harness specialized hardware. We need a system that allows developers to exploit ever-changing accelerator libraries, without over-specializing their code. As we cannot know the behavior of future libraries ahead of time, this paper develops a scheme that assists developers in matching their code to new libraries, without requiring the source code for these libraries. Furthermore, it can recover equivalent code from programs that use existing libraries and automatically port them to new interfaces. It first uses program synthesis to determine the meaning of a library, then maps the synthesized description into generalized constraints which are used to search the program for replacement opportunities to present to the developer. We applied this approach to existing large applications from the scientific computing and deep learning domains. Using our approach, we show speedups ranging from 1.1$\times$ to over 10$\times$ on end to end performance when using accelerator libraries., Comment: Accepted to PACT 2019

This paper introduces a vision of Miking, a language framework for constructing efficient and sound language environments and compilers for domain-specific modeling languages. In particular, this language framework has three key objectives: (i) to automatically generate interactive programmatic modeling environments, (ii) to guarantee sound compositions of language fragments that enable both rapid and safe domain-specific language development, (iii) to include first-class support for self-learning compilation, targeting heterogeneous execution platforms. The initiative is motivated in the domain of mathematical modeling languages. Specifically, two different example domains are discussed: (i) modeling, simulation, and verification of cyber-physical systems, and (ii) domain-specific differentiable probabilistic programming. The paper describes the main objectives of the vision, as well as concrete research challenges and research directions. QC 20210621

International audience; This volume constitutes the thoroughly refereed post-conference proceedings of the 9th International Conference on Verified Software: Theories, Tools, and Experiments, VSTTE 2017, held in Heidelberg, Germany, in July 2017.The 12 full papers presented were carefully revised and selected from 20 submissions. The papers describe large-scale verification efforts that involve collaboration, theory unification, tool integration, and formalized domain knowledge as well as novel experiments and case studies evaluating verification techniques and technologies.

International audience; This paper addresses the problem of code optimization for Real-Time and Embedded Systems (RTES). Such systems are designed using Model-Based Development (MBD)approach that consists of performing three major steps: building models, generating code from them and compiling the generated code. Actually, during the code generation, an important part of the modeling language semantics which could be useful for optimization is lost, thus, making impossible some optimizations achievement. This paper shows how adding a new level of optimization at the model level results in a more compact code. It also discusses the impact of the code generation on optimization: whether this step promotes or prevents optimizations. We conclude on a proposal of a new MBD approach containing only steps that advance optimization: modeling and compiling steps.

Commercial-off-the-shelf (COTS) components are black box software products. The absence of their code precludes them from any kind of inspection of certify that the code is safe. This increases the security risk for safety-sensitive applications. The application, before interfacing with COTS component, needs an assurance that it is secure. This paper presents a framework to assure security of components for such applications. This framework uses Aspect Oriented Programming (AOP) paradigm to capture security characteristics of the components and weaves the corresponding security checks into them. It also introduces a novel verification mechanism to ensure that the COTS components are developed as per security contract.

International audience; Dassault Aviation is a French aircraft manufacturer building civil business jets (the Falcon family) and military jet fighters (the Mirage and Rafale families). It has been concerned with formal methods inside the development process of avionic software since 1989. In this paper, we give a comprehensive account of three industrial-size studies carried out at Dassault Aviation using the reactive synchronous language ESTEREL and its toolset, in collaboration with the public research team that develops ESTEREL at Ecole des Mines de Paris and INRIA Sophia-Antipolis. We deal with software engineering issues related to compilation, optimization and verification of safety-critical embedded software. The goal is to ensure production of efficient and reliable code.