Search

We present Bioconda (https://bioconda.github.io), a distribution of bioinformatics software for the lightweight, multiplatform and language-agnostic package manager Conda. Currently, Bioconda offers a collection of over 3000 software packages, which is continuously maintained, updated, and extended by a growing global community of more than 200 contributors. Bioconda improves analysis reproducibility by allowing users to define isolated environments with defined software versions, all of which are easily installed and managed without administrative privileges.

This paper presents a lightweight interval analysis technique for determining the lower and upper bounds for program variables and its application in improving software model checking techniques. The experiments demonstrate that it is an effective approach to alleviate the state explosion problem in software model checking.

New DNA sequencing technologies deliver data at dramatically lower costs but demand new analytical methods to take full advantage of the very short reads that they produce. We provide an initial, theoretical solution to the challenge of de novo assembly from whole-genome shotgun “microreads.” For 11 genomes of sizes up to 39 Mb, we generated high-quality assemblies from 80× coverage by paired 30-base simulated reads modeled after real Illumina-Solexa reads. The bacterial genomes of Campylobacter jejuni and Escherichia coli assemble optimally, yielding single perfect contigs, and larger genomes yield assemblies that are highly connected and accurate. Assemblies are presented in a graph form that retains intrinsic ambiguities such as those arising from polymorphism, thereby providing information that has been absent from previous genome assemblies. For both C. jejuni and E. coli, this assembly graph is a single edge encompassing the entire genome. Larger genomes produce more complicated graphs, but the vast majority of the bases in their assemblies are present in long edges that are nearly always perfect. We describe a general method for genome assembly that can be applied to all types of DNA sequence data, not only short read data, but also conventional sequence reads.

Consider the problem of testing for existence of an n-node graph G satisfying some condition P, expressed as a Boolean constraint among the nxn Boolean entries of the adjacency matrix M. This problem reduces to satisfiability of P(M). If P is preserved by isomorphism, P(M) is satisfiable iff P(M)@?SB(M) is satisfiable, where SB(M) is a symmetry-breaking predicate-a predicate satisfied by at least one matrix M in each isomorphism class. P(M)@?SB(M) is more constrained than P(M), so it is solved faster by backtracking than P(M)-especially if SB(M) rules out most matrices in each isomorphism class. This method, proposed by Crawford et al., applies not just to graphs but to testing existence of a combinatorial object satisfying any property that respects isomorphism, as long as the property can be compactly specified as a Boolean constraint on the object's binary representation. We present methods for generating symmetry-breaking predicates for several classes of combinatorial objects: acyclic digraphs, permutations, functions, and arbitrary-arity relations (direct products). We define a uniform optimality measure for symmetry-breaking predicates, and evaluate our constraints according to this measure. Results indicate that these constraints are either optimal or near-optimal for their respective classes of objects.

The 1000 Genomes Project set out to provide a comprehensive description of common human genetic variation by applying whole-genome sequencing to a diverse set of individuals from multiple populations. Here we report completion of the project, having reconstructed the genomes of 2,504 individuals from 26 populations using a combination of low-coverage whole-genome sequencing, deep exome sequencing, and dense microarray genotyping. We characterized a broad spectrum of genetic variation, in total over 88 million variants (84.7 million single nucleotide polymorphisms (SNPs), 3.6 million short insertions/deletions (indels), and 60,000 structural variants), all phased onto high-quality haplotypes. This resource includes >99% of SNP variants with a frequency of >1% for a variety of ancestries. We describe the distribution of genetic variation across the global sample, and discuss the implications for common disease studies., Wellcome Trust (London, England) (Core Award 090532/Z/09/Z), Wellcome Trust (London, England) (Senior Investigator Award 095552/Z/11/Z ), Wellcome Trust (London, England) (WT095908), Wellcome Trust (London, England) (WT109497), Wellcome Trust (London, England) (WT098051), Wellcome Trust (London, England) (WT086084/Z/08/Z), Wellcome Trust (London, England) (WT100956/Z/13/Z ), Wellcome Trust (London, England) (WT097307), Wellcome Trust (London, England) (WT0855322/Z/08/Z ), Wellcome Trust (London, England) (WT090770/Z/09/Z ), Wellcome Trust (London, England) (Major Overseas program in Vietnam grant 089276/Z.09/Z), Medical Research Council (Great Britain) (grant G0801823), Biotechnology and Biological Sciences Research Council (Great Britain) (grant BB/I02593X/1), Biotechnology and Biological Sciences Research Council (Great Britain) (grant BB/I021213/1), Zhongguo ke xue ji shu qing bao yan jiu suo. Office of 863 Programme of China (2012AA02A201), National Basic Research Program of China (2011CB809201), National Basic Research Program of China (2011CB809202), National Basic Research Program of China (2011CB809203), National Natural Science Foundation of China (31161130357), Shenzhen Municipal Government of China (grant ZYC201105170397A), Canadian Institutes of Health Research (grant 136855), Quebec Ministry of Economic Development, Innovation, and Exports (PSR-SIIRI-195), Germany. Bundesministerium für Bildung und Forschung (0315428A), Germany. Bundesministerium für Bildung und Forschung (01GS08201), Germany. Bundesministerium für Bildung und Forschung (BMBF-EPITREAT grant 0316190A), Deutsche Forschungsgemeinschaft (Emmy Noether Grant KO4037/1-1), Beatriu de Pinos Program (2006 BP-A 10144), Beatriu de Pinos Program (2009 BP-B 00274), Spanish National Institute for Health (grant PRB2 IPT13/0001-ISCIII-SGEFI/FEDER), Japan Society for the Promotion of Science (fellowship number PE13075), Marie Curie Actions Career Integration (grant 303772), Fonds National Suisse del la Recherche, SNSF, Scientifique (31003A_130342), National Center for Biotechnology Information (U.S.) (U54HG3067), National Center for Biotechnology Information (U.S.) (U54HG3273), National Center for Biotechnology Information (U.S.) (U01HG5211), National Center for Biotechnology Information (U.S.) (U54HG3079), National Center for Biotechnology Information (U.S.) (R01HG2898), National Center for Biotechnology Information (U.S.) (R01HG2385), National Center for Biotechnology Information (U.S.) (RC2HG5552), National Center for Biotechnology Information (U.S.) (U01HG6513), National Center for Biotechnology Information (U.S.) (U01HG5214), National Center for Biotechnology Information (U.S.) (U01HG5715), National Center for Biotechnology Information (U.S.) (U01HG5718), National Center for Biotechnology Information (U.S.) (U01HG5728), National Center for Biotechnology Information (U.S.) (U41HG7635), National Center for Biotechnology Information (U.S.) (U41HG7497), National Center for Biotechnology Information (U.S.) (R01HG4960), National Center for Biotechnology Information (U.S.) (R01HG5701), National Center for Biotechnology Information (U.S.) (R01HG5214), National Center for Biotechnology Information (U.S.) (R01HG6855), National Center for Biotechnology Information (U.S.) (R01HG7068), National Center for Biotechnology Information (U.S.) (R01HG7644), National Center for Biotechnology Information (U.S.) (DP2OD6514), National Center for Biotechnology Information (U.S.) (DP5OD9154), National Center for Biotechnology Information (U.S.) (R01CA166661), National Center for Biotechnology Information (U.S.) (R01CA172652), National Center for Biotechnology Information (U.S.) (P01GM99568), National Center for Biotechnology Information (U.S.) (R01GM59290), National Center for Biotechnology Information (U.S.) (R01GM104390), National Center for Biotechnology Information (U.S.) (T32GM7790), National Center for Biotechnology Information (U.S.) (R01HL87699), National Center for Biotechnology Information (U.S.) (R01HL104608), National Center for Biotechnology Information (U.S.) (T32HL94284), National Center for Biotechnology Information (U.S.) (HHSN268201100040C), National Center for Biotechnology Information (U.S.) (HHSN272201000025C), Lundbeck Foundation (grant R170-2014-1039, Simons Foundation (SFARI award SF51), National Science Foundation (U.S.) (Research Fellowship DGE-1147470)

Motivation: Efficient simulation of population genetic samples under a given demographic model is a prerequisite for many analyses. Coalescent theory provides an efficient framework for such simulations, but simulating longer regions and higher recombination rates remains challenging. Simulators based on a Markovian approximation to the coalescent scale well, but do not support simulation of selection. Gene conversion is not supported by any published coalescent simulators that support selection. Results: We describe cosi2, an efficient simulator that supports both exact and approximate coalescent simulation with positive selection. cosi2 improves on the speed of existing exact simulators, and permits further speedup in approximate mode while retaining support for selection. cosi2 supports a wide range of demographic scenarios, including recombination hot spots, gene conversion, population size changes, population structure and migration. cosi2 implements coalescent machinery efficiently by tracking only a small subset of the Ancestral Recombination Graph, sampling only relevant recombination events, and using augmented skip lists to represent tracked genetic segments. To preserve support for selection in approximate mode, the Markov approximation is implemented not by moving along the chromosome but by performing a standard backwards-in-time coalescent simulation while restricting coalescence to node pairs with overlapping or near-overlapping genetic material. We describe the algorithms used by cosi2 and present comparisons with existing selection simulators. Availability and implementation: A free C++ implementation of cosi2 is available at http://broadinstitute.org/mpg/cosi2. Contact: ilya@broadinstitute.org Supplementary information: Supplementary data are available at Bioinformatics online.

Our computer modeling technique reproduces a tree's 3D volume and skeleton from instrumented photographs. The technique involves first constructing the skeleton (trunk and the major branches) of the tree, and then applying an L-system starting from this skeleton. L-systems are one of the better known procedural models in the graphics community, especially after their popularization by P. Prusinkiewicz and A. Lindenmayer (1990).

As an ancient disease with high fatality, cholera has likely exerted strong selective pressure on affected human populations. We performed a genome-wide study of natural selection in a population from the Ganges River Delta, the historic geographic epicenter of cholera. We identified 305 candidate selected regions using the composite of multiple signals (CMS) method. The regions were enriched for potassium channel genes involved in cyclic adenosine monophosphate–mediated chloride secretion and for components of the innate immune system involved in nuclear factor k B( NF-kB) signaling. We demonstrate that a number of these strongly selected genes are associated with cholera susceptibility in two separate cohorts. We further identify repeated examples of selection and association in an NF-kB/inflammasome–dependent pathway that is activated in vitro by Vibrio cholerae. Our findings shed light on the genetic basis of cholera resistance in a population from the Ganges River Delta and present a promising approach for identifying genetic factors influencing susceptibility to infectious diseases.

SummaryAlthough several hundred regions of the human genome harbor signals of positive natural selection, few of the relevant adaptive traits and variants have been elucidated. Using full-genome sequence variation from the 1000 Genomes (1000G) Project and the composite of multiple signals (CMS) test, we investigated 412 candidate signals and leveraged functional annotation, protein structure modeling, epigenetics, and association studies to identify and extensively annotate candidate causal variants. The resulting catalog provides a tractable list for experimental follow-up; it includes 35 high-scoring nonsynonymous variants, 59 variants associated with expression levels of a nearby coding gene or lincRNA, and numerous variants associated with susceptibility to infectious disease and other phenotypes. We experimentally characterized one candidate nonsynonymous variant in Toll-like receptor 5 (TLR5) and show that it leads to altered NF-κB signaling in response to bacterial flagellin.PaperFlick

The Plasmodium falciparum parasite's ability to adapt to environmental pressures, such as the human immune system and antimalarial drugs, makes malaria an enduring burden to public health. Understanding the genetic basis of these adaptations is critical to intervening successfully against malaria. To that end, we created a high-density genotyping array that assays over 17,000 single nucleotide polymorphisms (~1 SNP/kb), and applied it to 57 culture-adapted parasites from three continents. We characterized genome-wide genetic diversity within and between populations and identified numerous loci with signals of natural selection, suggesting their role in recent adaptation. In addition, we performed a genome-wide association study (GWAS), searching for loci correlated with resistance to thirteen antimalarials; we detected both known and novel resistance loci, including a new halofantrine resistance locus, PF10_0355. Through functional testing we demonstrated that PF10_0355 overexpression decreases sensitivity to halofantrine, mefloquine, and lumefantrine, but not to structurally unrelated antimalarials, and that increased gene copy number mediates resistance. Our GWAS and follow-on functional validation demonstrate the potential of genome-wide studies to elucidate functionally important loci in the malaria parasite genome., Bill & Melinda Gates Foundation, Ellison Medical Foundation, Exxon Mobil Foundation, Fogarty International Center, National Institute of Allergy and Infectious Diseases (U.S.), Burroughs Wellcome Fund, David & Lucile Packard Foundation, National Science Foundation (U.S.). Graduate Research Fellowship Program

Summary Genomic structural variants (SVs) are abundant in humans, differing from other variation classes in extent, origin, and functional impact. Despite progress in SV characterization, the nucleotide resolution architecture of most SVs remains unknown. We constructed a map of unbalanced SVs (i.e., copy number variants) based on whole genome DNA sequencing data from 185 human genomes, integrating evidence from complementary SV discovery approaches with extensive experimental validations. Our map encompassed 22,025 deletions and 6,000 additional SVs, including insertions and tandem duplications. Most SVs (53%) were mapped to nucleotide resolution, which facilitated analyzing their origin and functional impact. We examined numerous whole and partial gene deletions with a genotyping approach and observed a depletion of gene disruptions amongst high frequency deletions. Furthermore, we observed differences in the size spectra of SVs originating from distinct formation mechanisms, and constructed a map constructed a map of SV hotspots formed by common mechanisms. Our analytical framework and SV map serves as a resource for sequencing-based association studies.

With the success of formal verification techniques like equivalence checking and model checking for hardware designs, there has been growing interest in applying such techniques for formal analysis and automatic verification of software programs. This paper provides a brief tutorial on model checking of C programs. The essential approach is to model the semantics of C programs in the form of finite state systems by using suitable abstractions. The use of abstractions is key, both for modeling programs as finite state systems and for reducing the model sizes in order to manage verification complexity. We provide illustrative details of a verification platform called F-Soft, which provides a range of abstractions for modeling software, and uses customized SAT-based and BDD-based model checking techniques targeted for software.

The convexity of numerical domains such as polyhedra, octagons, intervals and linear equalities enables tractable analysis of software for buffer overflows, null pointer dereferences and floating point errors. However, convexity also causes the analysis to fail in many common cases. Powerset extensions can remedy this shortcoming by considering disjunctions of predicates. Unfortunately, analysis using powerset domains can be exponentially more expensive as compared to analysis on the base domain. In this paper, we prove structural properties of fixed points computed in commonly used powerset extensions. We show that a fixed point computed on a powerset extension is also a fixed point in the base domain computed on an “elaboration” of the program's CFG structure. Using this insight, we build analysis algorithms that approach path sensitive static analysis algorithms by performing the fixed point computation on the base domain while discovering an “elaboration” on the fly. Using restrictions on the nature of the elaborations, we design algorithms that scale polynomially in terms of the number of disjuncts. We have implemented a light-weight static analyzer for C programs with encouraging initial results.

In this paper, we describe our verification tool F-Soft, which is developed for the analysis of C programs. Its novelty lies in the combination of several recent advances in formal verification research including SAT-based verification, static analyses and predicate abstraction. As shown in the tool overview in Figure 1, we translate a program into a Boolean model to be analyzed by our verification engine DiVer [4], which includes BDD-based and SAT-based model checking techniques. We include various static analyses, such as computing the control flow graph of the program, program slicing with respect to the property, and performing range analysis as described in Section 2.2. We model the software using a Boolean representation, and use customized heuristics for the SAT-based analysis as described in Section [2.1]. We can also perform a localized predicate abstraction with register sharing as described in Section [2.3], if the user so chooses. The actual analysis of the resulting Boolean model is performed using DiVer. If a counter-example is discovered, we use a testbench generator that automatically generates an executable program for the user to examine the bug in his/her favorite debugger. The F-Soft tool has been applied on numerous case studies and publicly available benchmarks for sequential C programs. We are currently working on extending it to handle concurrent programs.

Declarative models, in which conjunction and negation are freely used, are susceptible to unintentional overconstraint. Core extraction is a new analysis that mitigates this problem in the context of a checker based on reduction to SAT (systems analysis tools). It exploits a recently developed facility of SAT solvers that provides an "unsatisfiable core" of an unsatisfiable set of clauses, often much smaller than the clause set as a whole. The unsatisfiable core is mapped back into the syntax of the original model, showing the user fragments of the model found to be irrelevant. This information can be a great help in discovering and localizing overconstraint, and in some cases pinpoints it immediately. The construction of the mapping is given for a generalized modeling language, along with a justification of the soundness of the claim that the marked portions of the model are irrelevant. Experiences in applying core extraction to a variety of existing models are discussed.

SAT solvers have been ranked primarily by the time they take to find a solution or show that none exists. And indeed, for many problems that are reduced to SAT, finding a single solution is what matters. As a result, much less attention has been paid to the problem of efficiently generating all solutions.

The authors analyze the time trends in five large nuclear data sets and describe a practical approach which utilizes these data in estimating the range of uncertainty in the individual physical measurements, observational and environmental studies and their meta-analytic syntheses. The time trends in the sequential series of measurements of the same physical quantity show a general pattern. The normal distribution grossly underestimates the probability of large deviations from the true values and the probability is well described by exponential functions. By analogy with physical measurements, the results indicate that the 95% confidence intervals in epidemiology and environmental studies should be expanded to account for unsuspected systematic errors. >

Alcoa is a tool for analyzing object models. It has a range of uses. At one end, it can act as a support tool for object model diagrams, checking for consistency of multiplicities and generating sample snapshots. At the other end, it embodies a lightweight formal method in which subtle properties of behaviour can be investigated. Alcoa's input language, Alloy, is a new notation based on Z. Its development was motivated by the need for a notation that is more closely tailored to object models (in the style of UML), and more amenable to automatic analysis. Like Z, Alloy supports the description of systems whose state involves complex relational structure. State and behavioural properties are described declaratively, by conjoining constraints. This makes it possible to develop and analyze a model incrementally, with Alcoa investigating the consequences of whatever constraints are given. Alcoa works by translating constraints to boolean formulas, and then applying state-of-the-art SAT solvers. It can analyze billions of states in seconds.

This study was stimulated by a recent U.S. Environmental Protection Agency (EPA, 1994) statement in draft environmental carcinogen risk assessment guidelines: “Several kinds of observations from animal studies can contribute to the judgment whether animal responses indicate a significant carcinogenic hazard to humans.” We have investigated each of these kinds of observation using the cancer bioassay data system database. We obtained concordances from rat to mouse (and vice versa) for various subgroups of chemicals as follows: chemicals that induced tumors at multiple sites, chemicals that induce cancer in both sexes, chemicals that display reduced latency, and chemicals increasing the rates of rare tumors. The concordances are much higher for these chemical subgroups than the chemical groups that induce tumor at a single site, in only one sex, or without reduced latency, respectively. Thus, our findings support some of the EPA's suggested factors.

The human genome contains hundreds of regions in which the patterns of genetic variation indicate recent positive natural selection, yet for most of these the underlying gene and the advantageous mutation remain unknown. We recently reported the development of a method, Composite of Multiple Signals (CMS), that combines tests for multiple signals of natural selection and increases resolution by up to 100-fold. Applying CMS to candidate selected regions from the International Haplotype Map, we localized several hundred signals to ~50-100 kb, identifying individual gene and polymorphism targets of selection. These regions included genes involved in processes known to be targets of selection, such as infectious disease, skin pigment, metabolism, and hair and sweat. We further identified many candidates that are similar to regulatory elements. In several regions, we identified variants that are significantly associated with the expression of nearby genes in the selected population. Moreover nearly half of the ~200 regions we examined localized to regions with no genes. Thirty of the regions contain long non-coding RNAs that have been shown to often regulate nearby genes, suggesting that variation within the RNAs might have functional consequences. With preliminary data now available from the 1000 Genomes Project, we are beginning to explore full sequence data, which should contains most if not all of the causal selected polymorphisms. We extended the CMS method to the preliminary data set, validating our previously identified candidates and identifying many new intriguing coding and regulatory variants.

Allpaths2, a method for accurately assembling small genomes with high continuity using short paired reads., We demonstrate that genome sequences approaching finished quality can be generated from short paired reads. Using 36 base (fragment) and 26 base (jumping) reads from five microbial genomes of varied GC composition and sizes up to 40 Mb, ALLPATHS2 generated assemblies with long, accurate contigs and scaffolds. Velvet and EULER-SR were less accurate. For example, for Escherichia coli, the fraction of 10-kb stretches that were perfect was 99.8% (ALLPATHS2), 68.7% (Velvet), and 42.1% (EULER-SR).