Search

Spectrum-based fault localization (SBFL) works well for single-fault programs but its accuracy decays for increasing fault numbers. We present FLITSR (Fault Localization by Iterative Test Suite Reduction), a novel SBFL extension that improves the localization of a given base metric specifically in the presence of multiple faults. FLITSR iteratively selects reduced versions of the test suite that better localize the individual faults in the system. This allows it to identify and re-rank faults ranked too low by the base metric because they were masked by other program elements. We evaluated FLITSR over method-level spectra from an existing large synthetic dataset comprising 75000 variants of 15 open-source projects with up to 32 injected faults, as well as method-level and statement-level spectra from a new dataset with 326 true multi-fault versions from the Defects4J benchmark set containing up to 14 real faults. For all three spectrum types we consistently see substantial reductions of the average wasted efforts at different fault levels, of 30%-90% over the best base metric, and generally similarly large increases in precision and recall, albeit with larger variance across the underlying projects. For the method-level real faults, FLITSR also substantially outperforms GRACE, a state-of-the-art learning-based fault localizer.

Programming language implementations are often one-sizefits-all. Irrespective of the ethnographic background or proficiency of their users, they offer a single, canonical syntax for all language users. Whereas professional software developers might be willing to learn a programming language all in one go, this might be a significant barrier for non-technical users, such as children who learn to program, or domain experts using domain-specific languages (DSLs). Parser tools, however, do not offer sufficient support for graduality or internationalization, leading (worst case) to maintaining multiple parsers, for each target class of users. In this paper we present Fabric, a grammar formalism that supports: 1) the gradual extension with (and deprecation of) syntactic constructs in consecutive levels (“vertical”), and, orthogonally, 2) the internationalization of syntax by translating keywords and shuffling sentence order (“horizontal”). This is done in such a way that downstream language processors (compilers, interpreters, type checkers etc.) are affected as little as possible. We discuss the design of Fabric and its implementation on top of the LARK parser generator, and how Fabric can be embedded in the Rascal language workbench. A case study on the gradual programming language Hedy shows that language levels can be represented and internationalized concisely, with hardly any duplication. We evaluate the Fabric library using the Rebel2 DSL, by translating it to Dutch, and “untranslating” its concrete syntax trees, to reuse its existing compiler. Fabric thus provides a principled approach to gradual syntax definition in levels and locales.

Block-based environments are visual-programming environments that allow users to create programs by dragging and dropping blocks that resemble jigsaw puzzle pieces. These environments have proven to lower the entry barrier of programming for end-users. Besides using block-based environments for programming, they can also help edit popular semi-structured data languages such as JSON and YAML. However, creating new block-based environments is still challenging; developers can develop them in an ad-hoc way or using context-free grammars in a language workbench. Given the visual nature of block-based environments, both options are valid; however, developers have some limitations when describing them. In this paper, we present Blocklybench, which is a meta-block-based environment for describing block-based environments for both programming and semi-structured data languages. This tool allows developers to express the specific elements of block-based environments using the blocks notation. To evaluate Blocklybench, we present three case studies. Our results show that Blocklybench allows developers to describe block-based specific aspects of language constructs such as layout, color, block connections, and code generators.

Packages and Supplementary Data for Castello, A., Fischer, B., Frese, C.K., Horos, R., Alleaume, A.M., Foehr, S., Curk, T., Krijgsveld, J. and Hentze, M.W., 2016. Comprehensive identification of RNA-binding domains in human cells. Molecular cell, 63(4), pp.696-710., {"references":["Castello, A., Fischer, B., Frese, C.K., Horos, R., Alleaume, A.M., Foehr, S., Curk, T., Krijgsveld, J. and Hentze, M.W., 2016. Comprehensive identification of RNA-binding domains in human cells. Molecular cell, 63(4), pp.696-710."]}

International audience; Exploratory programming is a software development style in which code is a medium for prototyping ideas and solutions, and in which even the end-goal can evolve over time. Exploratory programming is valuable in various contexts such as programming education, data science, and end-user programming. However, there is a lack of appropriate tooling and language design principles to support exploratory programming. This paper presents a host language-and object language-independent protocol for exploratory programming akin to the Language Server Protocol. The protocol serves as a basis to develop novel (or extend existing) programming environments for exploratory programming such as computational notebooks and command-line REPLs. An architecture is presented on top of which prototype environments can be developed with relative ease, because existing (language) components can be reused. Our prototypes demonstrate that the proposed protocol is sufficiently expressive to support exploratory programming scenarios as encountered in literature within the software engineering, human-computer interaction and data science domains.

International audience

Karten, Illustrationen

Although atmospheric 222radon (222Rn) activity concentration measurements are currently performed worldwide, they are being made by many different laboratories and with fundamentally different measurement principles, so compatibility issues can limit their utility for regional-to-global applications. Consequently, we conducted a European-wide 222Rn ∕ 222Rn progeny comparison study in order to evaluate the different measurement systems in use, determine potential systematic biases between them, and estimate correction factors that could be applied to harmonize data for their use as a tracer in atmospheric applications. Two compact portable Heidelberg radon monitors (HRM) were moved around to run for at least 1 month at each of the nine European measurement stations included in this comparison. Linear regressions between parallel data sets were calculated, yielding correction factors relative to the HRM ranging from 0.68 to 1.45. A calibration bias between ANSTO (Australian Nuclear Science and Technology Organisation) two-filter radon monitors and the HRM of ANSTO ∕ HRM = 1.11 ± 0.05 was found. Moreover, for the continental stations using one-filter systems that derive atmospheric 222Rn activity concentrations from measured atmospheric progeny activity concentrations, preliminary 214Po ∕ 222Rn disequilibrium values were also estimated. Mean station-specific disequilibrium values between 0.8 at mountain sites (e.g. Schauinsland) and 0.9 at non-mountain sites for sampling heights around 20 to 30 m above ground level were determined. The respective corrections for calibration biases and disequilibrium derived in this study need to be applied to obtain a compatible European atmospheric 222Rn data set for use in quantitative applications, such as regional model intercomparison and validation or trace gas flux estimates with the radon tracer method.

Patient derived organoids (PDOs) closely resemble individual tumor biology and allow testing of small molecules ex vivo . To systematically dissect compound effects on 3D organoids, we developed a high-throughput imaging and quantitative analysis approach. We generated PDOs from colorectal cancer patients, treated them with >500 small molecules and captured >3 million images by confocal microscopy. We developed the software framework SCOPE to measure compound induced re-organization of PDOs. We found diverse, but re-occurring phenotypes that clustered by compound mode-of-action. Complex phenotypes were not congruent with PDO viability and many were specific to subsets of PDO lines or were influenced by recurrent mutations. We further analyzed specific phenotypes induced by compound classes and found GSK3 inhibitors to disassemble PDOs via focal adhesion signaling or that MEK inhibition led to bloating of PDOs by enhancing of stemness. Finally, by viability classification, we show heterogeneous susceptibilities of PDOs to clinical anticancer drugs.

International audience

This work was done by Bernd Fischer, who sadly passed away in 2017. Thomas Schwarzl did make this data available. This is Supplementary Data for 'Horos, R., Büscher, M., Kleinendorst, R., Alleaume, A.M., Tarafder, A.K., Schwarzl, T., Dziuba, D., Tischer, C., Zielonka, E.M., Adak, A. and Castello, A., 2019. The small non-coding vault RNA1-1 acts as a riboregulator of autophagy. Cell, 176(5), pp.1054-1067.', {"references":["Horos, R., Büscher, M., Kleinendorst, R., Alleaume, A.M., Tarafder, A.K., Schwarzl, T., Dziuba, D., Tischer, C., Zielonka, E.M., Adak, A. and Castello, A., 2019. The small non-coding vault RNA1-1 acts as a riboregulator of autophagy. Cell, 176(5), pp.1054-1067."]}

The compendium of RNA-binding proteins (RBPs) has been greatly expanded by the development of RNA-interactome capture (RIC). However, it remained unknown if the complement of RBPs changes in response to environmental perturbations and whether these rearrangements are important. To answer these questions, we developed “comparative RIC” and applied it to cells challenged with an RNA virus called sindbis (SINV). Over 200 RBPs display differential interaction with RNA upon SINV infection. These alterations are mainly driven by the loss of cellular mRNAs and the emergence of viral RNA. RBPs stimulated by the infection redistribute to viral replication factories and regulate the capacity of the virus to infect. For example, ablation of XRN1 causes cells to be refractory to SINV, while GEMIN5 moonlights as a regulator of SINV gene expression. In summary, RNA availability controls RBP localization and function in SINV-infected cells. Garcia-Moreno, Noerenberg, Ni, and colleagues developed “comparative RNA-interactome capture” to analyze the RNA-bound proteome during virus infection. More than 200 cellular RNA-binding proteins change their binding activity in response to this challenge, mainly driven by transcript availability. Many of these RNA-binding proteins regulate viral replication and can be targeted to influence infection outcome., European Union’s Horizon 2020 research and innovation programme under Marie-Sklodowska-Curie grant agreement 700184. I.D. is funded by Wellcome Trust Investigator Award 209412/Z/17/Z. V.P. is funded by a SciLifeLab Fellowship, the Swedish Research Council (VR 2016-01842), a Wallenberg Academy Fellowship (KAW 2016.0123), and the Ragnar Söderberg Foundation. L.C. is funded by grant DGICYT SAF2015-66170-R (MINECO/FEDER).

International audience

International audience

ESBMC is a mature, permissively licensed open-source context-bounded model checker for the verification of single- and multi-threaded C programs. It can verify both safety (e.g., bounds check, pointer safety, overflow) and user-defined (as asserts in the program) properties automatically. ESBMC provides C++ and Python APIs to access internal data structures, allowing inspection and extension at any stage of the verification process. We discuss improvements over previous versions of ESBMC, including the description of new front- and back-ends, IEEE floating-point support, and an improved k-induction algorithm. A demonstration is available at https://www.youtube.com/watch?v=N_qmN-cazvM.

RNA-binding proteins (RBPs) play essential roles in RNA biology, responding to cellular and environmental stimuli to regulate gene expression. Important advances have helped to determine the (near) complete repertoires of cellular RBPs. However, identification of RBPs associated with specific transcripts remains a challenge. Here, we describe “specific ribonucleoprotein (RNP) capture,” a versatile method for the determination of the proteins bound to specific transcripts in vitro and in cellular systems. Specific RNP capture uses UV irradiation to covalently stabilize protein–RNA interactions taking place at “zero distance.” Proteins bound to the target RNA are captured by hybridization with antisense locked nucleic acid (LNA)/DNA oligonucleotides covalently coupled to a magnetic resin. After stringent washing, interacting proteins are identified by quantitative mass spectrometry. Applied to in vitro extracts, specific RNP capture identifies the RBPs bound to a reporter mRNA containing the Sex-lethal (Sxl) binding motifs, revealing that the Sxl homolog sister of Sex lethal (Ssx) displays similar binding preferences. This method also revealed the repertoire of RBPs binding to 18S or 28S rRNAs in HeLa cells, including previously unknown rRNA-binding proteins.

DepthK is a software verification tool that employs a proof by induction algorithm that combines k-induction with invariant inference. In order to efficiently and effectively verify and falsify safety properties in C programs, DepthK infers program invariants using polyhedral constraints. Experimental results show that our approach can handle a wide variety of safety properties in several intricate verification tasks.

Sequentialization is one of the most promising approaches for the symbolic analysis of concurrent programs. However, existing sequentializations assume sequential consistency, which modern hardware architectures no longer guarantee. In this paper we describe an approach to embed weak memory models within eager sequentializations (a la Lal/Reps). Our approach is based on the separation of intra-thread computations from inter-thread communications by means of a shared memory abstraction (SMA). We give details of SMA implementations for the SC, TSO, and PSO memory models that are based on the idea of individual memory unwindings, and sketch an extension to the Power memory model. We use our approach to implement a new, efficient BMC-based bug finding tool for multi-threaded C programs under SC, TSO, or PSO based on these SMAs, and show experimentally that it is competitive to existing tools.

We describe an approach to design static analysis and verification tools for concurrent programs that separates intra-thread computation from inter-thread communication by means of a shared memory abstraction (SMA). We formally characterize the concept of thread-asynchronous transition systems that underpins our approach and that allows us to design tools as two independent components, the intra-thread analysis, which can be optimized separately, and the implementation of the SMA itself, which can be exchanged easily (e.g., from the SC to the TSO memory model). We describe the SMA’s API and show that several concurrent verification techniques from the literature can easily be recast in our setting and thus be extended to weak memory models. We give SMA implementations for the SC, TSO, and PSO memory models that are based on the idea of individual memory unwindings. We instantiate our approach by developing a new, efficient BMC-based bug finding tool for multi-threaded C programs under SC, TSO, or PSO based on these SMAs, and show experimentally that it is competitive to existing tools.

We describe a new CSeq module for the verification of multi-threadedC programs with dynamic thread creation. This module implements a variationof the lazy sequentialization algorithm implemented in Lazy-CSeq. The mainnovelty is that we do not bound here the number of round-robin schedules in anexecution and the loops that do not contain a thread creation statement are notunwound (and thus unboundedly many iterations can be considered). As in Lazy-CSeq the number of thread creations per run is bounded as well as the depth ofrecursive calls. For the experiments we use CPAChecker as backend

Sequentialization translates concurrent programs into (under certain assumptions) equivalent nondeterministic sequential programs and so reduces concurrent verification to its sequential counterpart. In previous work, we have developed and implemented in the Lazy-CSeq tool a lazy sequentialization schema for bounded programs that introduces very small memory overheads and very few sources of nondeterminism and is thus very effective in practice [1, 2].The current version of Lazy-CSeq adds deadlock detection, counterexample generation, and explicit schedule control. It also implements an improved version of the original schema, which uses an optimized representation of the context switch points and eagerly guesses these, but retains its other characteristics. Experiments show that these optimizations lead to some performance gains.

National audience

International audience; DNA methylation is a conservative epigenetic marker. A correct DNA methylation pattern is essential for embryonic development. Mammalian embryos gain a complete de novo DNA methylation design around implantation. DNA methylation is a potential mechanism of periconceptional programming, suggesting that the DNA methylation pattern of developing embryo might be affected in distinct ways, depending on nutritional and hormonal signals. To expand this idea we have investigated the DNA methylation pattern of the promoter region of the POU5F1 (Oct4) pluripotency gene in preimplantation rabbit embryos at day 6 p.c (early gastrulation stage). The blastocysts were collected from healthy and diabetic rabbits. The POU5F1 promoter contains four conservative regions, which are embracing important elements for its transcription: proximal and distal enhancers (PE-1A, PE-1B, DE-1A), a SOX2/Oct4 binding site and hormone responding element (HRE). We have characterized the CpG islands methylation at all mentioned regions in two embryonic tissues: embryoblast and trophoblast, using bisulfite treatment, cloning and sequencing. The analysis has been successfully performed for the trophoblast tissue yet. A higher methylation of the CpG islands for HRE and at the beginning of first exon has been noticed in the trophoblast of diabetic embryos. A hypomethylation in trophoblast from diabetic embryos comparing to trophoblasts from healthy pregnancies was visible for proximal enhancer 1A (PE-1A) in frame of conservative region 3 (CR3). In this context, DNA methylation can be considered as a form of embryo developmental plasticity, which can promote metabolic disorders in adult life.

We describe a version of the lazy sequentialization schema by La Torre, Madhusudan, and Parlato that is optimized for bounded programs, and avoids the re-computation of the local state of each process at each context switch. Lazy-CSeq implements this sequentialization schema for sequentially consistent C programs using POSIX threads. Experiments show that it is very competitive.

We implement a new sequentialization algorithm for multi-threaded C programs with dynamic thread creation as a new CSeq module. The novel basic idea of this algorithm is to fix (by a nondeterministic guess) the sequence of write operations in the shared memory and then simulate the behavior of the program according to any scheduling that respects this choice. Simulation is done thread-by-thread and the thread creation mechanism is replaced by function calls.

Sequentialization translates concurrent programs into equivalent nondeterministic sequential programs so that the different concurrent schedules no longer need to be handled explicitly. It can thus be used as a concurrency preprocessing technique for automated sequential program verification tools. Our CSeq tool implements a novel sequentialization for C programs using pthreads, which extends the Lal/Reps sequentialization to support dynamic thread creation. CSeq now works with three different backend tools, CBMC, ESBMC, and LLBMC, and is competitive with state-of-the-art verification tools for concurrent programs.

This work aims to demonstrate the ability of numerical simulations to mode] solid · and liquid interfaces. In the work on the solid interfaces, the GCMC method was used to sin:rnlatc the ads011Jtion isotherrn of acetaldehyde on ice under the conditions of the ·upper tropospherc and the molecular dynamics method was usecl to characterize the adsorption of difünctionalized organic compounds on ice, aiming at interpreting experimental results. Part of this work was devotcd to the simulation of the phase diagrarn (p, T) of organic aerosols (oxalic acid and malonic) in tropospberic conditions to study the ability of aerosols to act as condensation nuclei for icc particlcs. The work: on liquid interfaces concerned firstly the competitive adsorption of polymcrs and surfactants at the water surface. It is based on a very precise desc1iption, by mnncrical simulation, of the structure émd dynamics cif the surface of the considered systems. The second pari of the work on liquid interfaces bas focused on the characterization of ion transfer across a liquid/liquid interface through the calculations of the free energy variations of the system during the transfo·. To obtain a rigorous desc1iptio11 of the details of the corresponding processes, a specific method was developed in this thesis to calculate the free energy profile while taking into account tbe dynamics of the interface., Ce travail a pour objectif de montrer la capacité des simulations numériques à modéliser les phénomènes aux interfaces solides et liquides. Dans le travail sur les interfaces solides, la méthode GCMC a été utilisée pour simuler l'isotherme d'adsorption de !'acétaldéhyde sur la glace dans les conditions de la haute troposphère, puis l'adsorption de composés organiques bi-fonctionnalisés sur la glace a été caractérisée par dynamique moléculaire avec pour objectif d'interpréter des résl1ltats expérimentaux de la littérature. Une partie de ce travail a été consacrée à la circulation du diagramme de phase (p,T) d'aérosols organiques (acide oxalique et malonique) clans les conditions troposphériques afin d'étudier la capacité de ces aérosols à jouer le rôle de noyaux de condensation pour les particules de glace. Le travail sur les interfaces liquides a concerné tout d'abord l'adsorption compétitive de polymères et de smfactants à la surface de l'eau. Il s'appuie sur une description très précise, par simulation, de la structure et de la dynamique de la surface des systèmes considérés. La deuxième partie des travaux sur les interfaces liquides s'est intéressée à la caractérisation du transfert d'ions à travers une interface liquide/liquide par le biais du calcul des variations de l'énergie libre du système au cours du transfc1i. Afin d'obtenir une description très rigoureuse des détails des processus mis enjeu, une méthode spécifique a été développée dans cette thèse pour calculer le profil d'énergie libre en tenant compte directement du caractère très dynamique de l'interface.

There exist a number of software engineering scenarios that essentially involve equivalence or correspondence assertions for some of the context-free grammars in the scenarios. For instance, when applying grammar transformations during parser development—be it for the sake of disambiguation or grammar-class compliance—one would like to preserve the generated language. Even though equivalence is generally undecidable for context-free grammars, we have developed an automated approach that is practically useful in revealing evidence of nonequivalence of grammars and discovering correspondence mappings for grammar nonterminals. Our approach is based on systematic test data generation and parsing. We discuss two studies that show how the approach is used in comparing grammars of open source Java parsers as well as grammars from the course work for a compiler construction class.

There exist a number of software engineering scenarios that essentially involve equivalence or correspondence assertions for some of the context-free grammars in the scenarios. For instance, when applying grammar transformations during parser development---be it for the sake of disambiguation or grammar-class compliance---one would like to preserve the generated language. Even though equivalence is generally undecidable for context-free grammars, we have developed an automated approach that is practically useful in revealing evidence of nonequivalence of grammars and discovering correspondence mappings for grammar nonterminals. The approach is based on systematic test data generation and parsing. We discuss two studies that show how the approach is used in comparing grammars of open source Java parsers as well as grammars from the course work for a compiler construction class.

Embedded systems are everywhere, from home appliances to critical systems such as medical devices. They usually have associated timing constraints that need to be verified for the implementation. Here, we use an untimed bounded model checker to verify timing properties of embedded C programs. We propose an approach to specify discrete time timing constraints using code annotations. The annotated code is then automatically translated to code that manipulates auxiliary timer variables and is thus suitable as input to conventional, untimed software model checker such as ESBMC. Thus, we can check timing constraints in the same way and at the same time as untimed system requirements, and even allow for interaction between them. We applied the proposed method in a case study, and verified timing constraints of a pulse oximeter, a noninvasive medical device that measures the oxygen saturation of arterial blood.

Embedded systems are everywhere, from home appliances to critical systems such as medical devices. They usually have associated timing constraints that need to be verified for the implementation. Here, we use an untimed bounded model checker to verify timing properties of embedded C programs. We propose an approach to specify discrete time timing constraints using code annotations. The annotated code is then automatically translated to code that manipulates auxiliary timer variables and is thus suitable as input to conventional, untimed software model checker such as ESBMC. Thus, we can check timing constraints in the same way and at the same time as untimed system requirements, and even allow for interaction between them. We applied the proposed method in a case study, and verified timing constraints of a pulse oximeter, a noninvasive medical device that measures the oxygen saturation of arterial blood., Comment: 16 pages

National audience

International audience

National audience

International audience

The transition from single-core to multi-core processors has made multi-threaded software an important subject in computer aided verification. Here, we describe and evaluate an extension of the ESBMC model checker to support the verification of multi-threaded software with shared variables and locks using bounded model checking (BMC) based on Satisfiability Modulo Theories (SMT). We describe three approaches to model check multi-threaded software and our modelling of the synchronization primitives of the Pthread library. In the lazy approach, we generate all possible interleavings and call the BMC procedure on each of them individually, until we either find a bug, or have systematically explored all interleavings. In the schedule recording approach, we encode all possible interleavings into one single formula and then exploit the high speed of the SMT solvers. In the underapproximation-widening approach, we reduce the state space by abstracting the number of state variables and interleavings from the proofs of unsatisfiability generated by the SMT solvers. In all three approaches, we use partial-order reduction (POR) techniques to reduce the number of interleavings explored. Experiments show that our approaches can analyze larger problems and substantially reduce the verification time compared to state-of-the-art techniques that combine classic POR methods with symbolic algorithms and others that implement the Counter-Example Guided Abstraction Refinement technique.