@article{4226, abstract = {In the developing fly wing, secreted morphogens such as Decapentaplegic (Dpp) and Wingless (Wg) form gradients of concentration providing positional information. Dpp forms a longer-range gradient than Wg. To understand how the range is controlled, we measured the four key kinetic parameters governing morphogen spreading: the production rate, the effective diffusion coefficient, the degradation rate, and the immobile fraction. The four parameters had different values for Dpp versus Wg. In addition, Dynamin-dependent endocytosis was required for spreading of Dpp, but not Wg. Thus, the cellular mechanisms of Dpp and Wingless spreading are different: Dpp spreading requires endocytic, intracellular trafficking.}, author = {Anna Kicheva and Pantazis, Periklis and Bollenbach, Tobias and Kalaidzidis, Yannis and Bittig, Thomas and Julicher, Frank and Gonzalez-Gaitan, Marcos}, journal = {Science}, number = {5811}, pages = {521 -- 525}, publisher = {American Association for the Advancement of Science}, title = {{Kinetics of morphogen gradient formation}}, doi = {10.1126/science.1135774}, volume = {315}, year = {2007}, } @inproceedings{4233, author = {Vladar, Harold}, editor = {Falcón, N. and Loyo De Sardi, Y.}, pages = {91 -- 109}, publisher = {Consejo de Desarrollo Cientifico y Tecnologico}, title = {{Alternativas prebióticas para la síntesis de amino- ácidos y otras moléculas relacionadas}}, year = {2007}, } @article{4234, abstract = {We study a generalised model of population growth in which the state variable is population growth rate instead of population size. Stochastic parametric perturbations, modelling phenotypic variability, lead to a Langevin system with two sources of multiplicative noise. The stationary probability distributions have two characteristic power-law scales. Numerical simulations show that noise suppresses the explosion of the growth rate which occurs in the deterministic counterpart. Instead, in different parameter regimes populations will grow with "anomalous" stochastic rates and (i) stabilise at "random carrying capacities", or (ii) go extinct in random times. Using logistic fits to reconstruct the simulated data, we find that even highly significant estimations do not recover or reflect information about the deterministic part of the process. Therefore, the logistic interpretation is not biologically meaningful. These results have implications for distinct model-aided calculations in biological situations because these kinds of estimations could lead to spurious conclusions. (c) 2006 Elsevier B.V. All rights reserved.}, author = {de Vladar, Harold and Pen, I.}, journal = {Physica A}, pages = {477 -- 485}, publisher = {Elsevier}, title = {{Determinism, noise, and spurious estimations in a generalised model of population growth}}, doi = {10.1016/j.physa.2006.06.025}, volume = {373}, year = {2007}, } @article{4246, abstract = {Gaia theory, which describes the life–environment system of the Earth as stable and self-regulating, has remained at the fringes of mainstream biological science owing to its historically inadequate definition and apparent incompatibility with individual-level natural selection. The key issue is whether and why the biosphere might tend towards stability and self-regulation. We review the various ways in which these issues have been addressed by evolutionary and ecological theory, and relate these to ‘Gaia theory’. We then ask how this theory extends the perspectives offered by these disciplines, and how it might be tested by novel modelling approaches and laboratory experiments using emergent technologies.}, author = {Free, Andrew and Nicholas Barton}, journal = {Trends in Ecology and Evolution}, number = {11}, pages = {611 -- 619}, publisher = {Cell Press}, title = {{Do evolution and ecology need the Gaia hypothesis?}}, doi = {10.1016/j.tree.2007.07.007}, volume = {22}, year = {2007}, } @article{4247, abstract = {Evolution at multiple gene positions is complicated. Direct selection on one gene disturbs the evolutionary dynamics of associated genes. Recent years have seen the development of a multilocus methodology for modeling evolution at arbitrary numbers of gene positions with arbitrary dominance and epistatic relations, mode of inheritance, genetic linkage, and recombination. We show that the approach is conceptually analogous to social evolutionary methodology, which focuses on selection acting on associated individuals. In doing so, we (1) make explicit the links between the multilocus methodology and the foundations of social evolution theory, namely, Price’s theorem and Hamilton’s rule; (2) relate the multilocus approach to levels‐of‐selection and neighbor‐modulated‐fitness approaches in social evolution; (3) highlight the equivalence between genetical hitchhiking and kin selection; (4) demonstrate that the multilocus methodology allows for social evolutionary analyses involving coevolution of multiple traits and genetical associations between nonrelatives, including individuals of different species; (5) show that this methodology helps solve problems of dynamic sufficiency in social evolution theory; (6) form links between invasion criteria in multilocus systems and Hamilton’s rule of kin selection; (7) illustrate the generality and exactness of Hamilton’s rule, which has previously been described as an approximate, heuristic result.}, author = {Gardner, Andy and West, Stuart A and Nicholas Barton}, journal = {American Naturalist}, number = {2}, pages = {207 -- 226}, publisher = {University of Chicago Press}, title = {{The relation between multilocus population genetics and social evolution theory}}, doi = {10.1086/510602}, volume = {169}, year = {2007}, } @inproceedings{4342, abstract = {Library 2.0 and user-generated content are two terms, which are closely connected. In the presentation, I will briefly define both terms. Two example projects where user- generated content and libraries interact will be presented. The cooperation of Wikipedia and the Personennamendatei, the German cooperative name authority files is the first. The second will be Wikisource where users provide transcribed source material. Another important area of user-generated content is social tagging where users index different resources. And if the users will do so much in the future, is there still a place for librarians? But in the future user and librarians become partners and the library will provide the platform: the library 2.0.}, author = {Danowski, Patrick}, location = {Durban, South Africa}, publisher = {IFLA}, title = {{Library 2.0 and User-Generated Content - What can the users do for us?}}, doi = {601}, year = {2007}, } @article{4343, abstract = {Wikipedia and libraries share the same goal: simple and fast knowledge transfer. Through linking different information resources on the Internet, knowledge gets comprehensively accessible. The co-operation with the Personennamendatei, the German authority file for names of persons is an example for linking between Wikipedia and library catalogs. The article highlights, how this co-operation works and what the benefits are.}, author = {Danowski, Patrick and Pfeifer, Barbara}, journal = {Bibliothek - Forschung und Praxis}, number = {2}, pages = {149 -- 155}, publisher = {De Gruyter}, title = {{Wikipedia und Normdateien: Wege der Vernetzung am Beispiel der Kooperation mit der Personennamendatei}}, doi = {10.1515/BFUP.2007.149}, volume = {31}, year = {2007}, } @article{4344, abstract = {Anknüpfend an ihren Aufsatz „Bibliothek 2.0 – Die Zukunft der Bibliothek?“ (2006) geben Patrick Danowski und Lambert Heller, verantwortlich für das Schwerpunktthema der vorliegenden Ausgabe, einen Überblick über den erreichten Diskussionsstand über verschiedene Teilaspekte der Bibliothek 2.0 unter besonderer Berücksichtigung der deutschen Fachöffentlichkeit. Einige charakteristische Fragen und Probleme der Weiterentwicklung, Öffnung und Vernetzung bibliothekarischer Dienste und Informationen werden angesprochen.}, author = {Danowski, Patrick and Heller, Lambert}, journal = {Bibliothek - Forschung und Praxis}, number = {2}, pages = {130 -- 136}, publisher = {De Gruyter}, title = {{Bibliothek 2.0? Wird alles anders?}}, doi = {10.1515/BFUP.2007.130}, volume = {31}, year = {2007}, } @article{4353, abstract = {BACKGROUND: The invention of the Genome Sequence 20 DNA Sequencing System (454 parallel sequencing platform) has enabled the rapid and high-volume production of sequence data. Until now, however, individual emulsion PCR (emPCR) reactions and subsequent sequencing runs have been unable to combine template DNA from multiple individuals, as homologous sequences cannot be subsequently assigned to their original sources. METHODOLOGY: We use conventional PCR with 5'-nucleotide tagged primers to generate homologous DNA amplification products from multiple specimens, followed by sequencing through the high-throughput Genome Sequence 20 DNA Sequencing System (GS20, Roche/454 Life Sciences). Each DNA sequence is subsequently traced back to its individual source through 5'tag-analysis. CONCLUSIONS: We demonstrate that this new approach enables the assignment of virtually all the generated DNA sequences to the correct source once sequencing anomalies are accounted for (miss-assignment rate<0.4%). Therefore, the method enables accurate sequencing and assignment of homologous DNA sequences from multiple sources in single high-throughput GS20 run. We observe a bias in the distribution of the differently tagged primers that is dependent on the 5' nucleotide of the tag. In particular, primers 5' labelled with a cytosine are heavily overrepresented among the final sequences, while those 5' labelled with a thymine are strongly underrepresented. A weaker bias also exists with regards to the distribution of the sequences as sorted by the second nucleotide of the dinucleotide tags. As the results are based on a single GS20 run, the general applicability of the approach requires confirmation. However, our experiments demonstrate that 5'primer tagging is a useful method in which the sequencing power of the GS20 can be applied to PCR-based assays of multiple homologous PCR products. The new approach will be of value to a broad range of research areas, such as those of comparative genomics, complete mitochondrial analyses, population genetics, and phylogenetics.}, author = {Binladen, Jonas and Gilbert, M Thomas and Jonathan Bollback and Panitz, Frank and Bendixen, Christian and Nielsen, Rasmus and Willerslev, Eske}, journal = {PLoS One}, number = {2}, publisher = {Public Library of Science}, title = {{The use of coded PCR primers enables high-throughput sequencing of multiple homolog amplification products by 454 parallel sequencing}}, doi = {10.1371/journal.pone.0000197}, volume = {2}, year = {2007}, } @article{4354, abstract = {Homology search is one of the most ubiquitous bioinformatic tasks, yet it is unknown how effective the currently available tools are for identifying noncoding RNAs (ncRNAs). In this work, we use reliable ncRNA data sets to assess the effectiveness of methods such as BLAST, FASTA, HMMer, and Infernal. Surprisingly, the most popular homology search methods are often the least accurate. As a result, many studies have used inappropriate tools for their analyses. On the basis of our results, we suggest homology search strategies using the currently available tools and some directions for future development.}, author = {Freyhult, Eva K and Jonathan Bollback and Gardner, Paul P}, journal = {Genome Research}, number = {1}, pages = {117 -- 25}, publisher = {Cold Spring Harbor Laboratory Press}, title = {{Exploring genomic dark matter: a critical assessment of the performance of homology search methods on noncoding RNA}}, doi = {10.1101/gr.5890907}, volume = {17}, year = {2007}, } @article{4355, abstract = {When a beneficial mutation is fixed in a population that lacks recombination, the genetic background linked to that mutation is fixed. As a result, beneficial mutations on different backgrounds experience competition, or "clonal interference," that can cause asexual populations to evolve more slowly than their sexual counterparts. Factors such as a large population size (N) and high mutation rates (mu) increase the number of competing beneficial mutations, and hence are expected to increase the intensity of clonal interference. However, recent theory suggests that, with very large values of Nmu, the severity of clonal interference may instead decline. The reason is that, with large Nmu, genomes including both beneficial mutations are rapidly created by recurrent mutation, obviating the need for recombination. Here, we analyze data from experimentally evolved asexual populations of a bacteriophage and find that, in these nonrecombining populations with very large Nmu, recurrent mutation does appear to ameliorate this cost of asexuality.}, author = {Jonathan Bollback and Huelsenbeck, John P}, journal = {Molecular Biology and Evolution}, number = {6}, pages = {1397 -- 1406}, publisher = {Oxford University Press}, title = {{Clonal interference is alleviated by high mutation rates in large populations}}, doi = {10.1093/molbev/msm056}, volume = {24}, year = {2007}, } @article{4356, abstract = {We used a comparative genomics approach to identify genes that are under positive selection in six strains of Escherichia coli and Shigella flexneri, including five strains that are human pathogens. We find that positive selection targets a wide range of different functions in the E. coli genome, including cell surface proteins such as beta barrel porins, presumably because of the involvement of these genes in evolutionary arms races with other bacteria, phages, and/or the host immune system. Structural mapping of positively selected sites on trans-membrane beta barrel porins reveals that the residues under positive selection occur almost exclusively in the extracellular region of the proteins that are enriched with sites known to be targets of phages, colicins, or the host immune system. More surprisingly, we also find a number of other categories of genes that show very strong evidence for positive selection, such as the enigmatic rhs elements and transposases. Based on structural evidence, we hypothesize that the selection acting on transposases is related to the genomic conflict between transposable elements and the host genome.}, author = {Petersen, Lise and Jonathan Bollback and Dimmic, Matt and Hubisz, Melissa and Nielsen, Rasmus}, journal = {Genome Research}, number = {9}, pages = {1336 -- 1343}, publisher = {Cold Spring Harbor Laboratory Press}, title = {{Genes under positive selection in Escherichia coli}}, doi = {10.1101/gr.6254707}, volume = {17}, year = {2007}, } @inproceedings{4368, abstract = {In this paper we describe AMT, a tool for monitoring temporal properties of continuous signals. We first introduce Stl/Psl, a specification formalism based on the industrial standard language Psl and the real-time temporal logic Mitl, extended with constructs that allow describing behaviors of real-valued variables. The tool automatically builds property observers from an Stl/Psl specification and checks, in an offline or incremental fashion, whether simulation traces satisfy the property. The AMT tool is validated through a Flash memory case-study.}, author = {Nickovic, Dejan and Maler, Oded}, booktitle = {5th International Conference on Formal Modeling and Analysis of Timed Systems}, location = {Salzburg, Austria}, pages = {304 -- 319}, publisher = {Springer}, title = {{AMT: A property-based monitoring tool for analog systems}}, doi = {10.1007/978-3-540-75454-1_22}, volume = {4763}, year = {2007}, } @inproceedings{4370, abstract = {In this paper we propose a complete chain for synthesizing controllers from high-level specifications. From real-time properties expressed in the logic mtl we generate, under bounded-variability assumptions, deterministic timed automata to which we apply safety synthesis algorithms to derive a controller that satisfies the properties by construction. Some preliminary experimental results are reported.}, author = {Maler, Oded and Nickovic, Dejan and Pnueli, Amir}, booktitle = {19th International Conference on Computer Aided Verification}, location = {Berlin, Germany}, pages = {95 -- 107}, publisher = {Springer}, title = {{On synthesizing controllers from bounded-response properties}}, doi = {10.1007/978-3-540-73368-3_12}, volume = {4590}, year = {2007}, } @inproceedings{4394, abstract = {This paper presents our integration of efficient resolution-based theorem provers into the Jahob data structure verification system. Our experimental results show that this approach enables Jahob to automatically verify the correctness of a range of complex dynamically instantiable data structures, such as hash tables and search trees, without the need for interactive theorem proving or techniques tailored to individual data structures. Our primary technical results include: (1) a translation from higher-order logic to first-order logic that enables the application of resolution-based theorem provers and (2) a proof that eliminating type (sort) information in formulas is both sound and complete, even in the presence of a generic equality operator. Our experimental results show that the elimination of type information often dramatically decreases the time required to prove the resulting formulas. These techniques enabled us to verify complex correctness properties of Java programs such as a mutable set implemented as an imperative linked list, a finite map implemented as a functional ordered tree, a hash table with a mutable array, and a simple library system example that uses these container data structures. Our system verifies (in a matter of minutes) that data structure operations correctly update the finite map, that they preserve data structure invariants (such as ordering of elements, membership in appropriate hash table buckets, or relationships between sets and relations), and that there are no run-time errors such as null dereferences or array out of bounds accesses.}, author = {Bouillaguet, Charles and Kuncak, Viktor and Wies, Thomas and Zee, Karen and Rinard, Martin}, booktitle = {8th International Conference on Verification, Model Checking, and Abstract Interpretation}, location = {Nice, France}, pages = {74 -- 88}, publisher = {Springer}, title = {{Using first-order theorem provers in the Jahob data structure verification system}}, doi = {10.1007/978-3-540-69738-1_5}, volume = {4349}, year = {2007}, } @inproceedings{4398, abstract = {We propose a shape analysis that adapts to some of the complex composite data structures found in industrial systems-level programs. Examples of such data structures include “cyclic doubly-linked lists of acyclic singly-linked lists”, “singly-linked lists of cyclic doubly-linked lists with back-pointers to head nodes”, etc. The analysis introduces the use of generic higher-order inductive predicates describing spatial relationships together with a method of synthesizing new parameterized spatial predicates which can be used in combination with the higher-order predicates. In order to evaluate the proposed approach for realistic programs we have performed experiments on examples drawn from device drivers: the analysis proved safety of the data structure manipulation of several routines belonging to an IEEE 1394 (firewire) driver, and also found several previously unknown memory safety bugs.}, author = {Berdine, Josh and Calcagno, Cristiano and Cook, Byron and Distefano, Dino and O'Hearn, Peter and Wies, Thomas and Yang, Hongseok}, booktitle = {19th International Conference on Computer Aided Verification}, location = {Berlin, Germany}, pages = {178 -- 192}, publisher = {Springer}, title = {{Shape analysis for composite data structures}}, doi = {10.1007/978-3-540-73368-3_22}, volume = {4590}, year = {2007}, } @inproceedings{4399, abstract = {A temporal interface for a software component is a finite automaton that specifies the legal sequences of calls to functions that are provided by the component. We compare and evaluate three different algorithms for automatically extracting temporal interfaces from program code: (1) a game algorithm that computes the interface as a representation of the most general environment strategy to avoid a safety violation; (2) a learning algorithm that repeatedly queries the program to construct the minimal interface automaton; and (3) a CEGAR algorithm that iteratively refines an abstract interface hypothesis by adding relevant program variables. For comparison purposes, we present and implement the three algorithms in a unifying formal setting. While the three algorithms compute the same output and have similar worst-case complexities, their actual running times may differ considerably for a given input program. On the theoretical side, we provide for each of the three algorithms a family of input programs on which that algorithm outperforms the two alternatives. On the practical side, we evaluate the three algorithms experimentally on a variety of Java libraries. }, author = {Beyer, Dirk and Thomas Henzinger and Vasu Singh}, pages = {4 -- 19}, publisher = {Springer}, title = {{Algorithms for interface synthesis}}, doi = {10.1007/978-3-540-73368-3_4}, volume = {4590}, year = {2007}, } @inproceedings{4402, abstract = {For specifying and verifying branching-time requirements, a reactive system is traditionally modeled as a labeled tree, where a path in the tree encodes a possible execution of the system. We propose to enrich such tree models with “jump-edges” that capture observational indistinguishability: for an agent a, an a-labeled edge is added between two nodes if the observable behaviors of the agent a along the paths to these nodes are identical. We show that it is possible to specify information flow properties and partial information games in temporal logics interpreted on this enriched structure. We study complexity and decidability of the model checking problem for these logics. We show that it is PSPACE-complete and EXPTIME-complete respectively for fragments of CTL and μ-calculus-like logics. These fragments are expressive enough to allow specifications of information flow properties such as “agent A does not reveal x (a secret) until agent B reveals y (a password)” and of partial information games.}, author = {Alur, Rajeev and Cerny, Pavol and Chaudhuri, Swarat}, booktitle = {13th International Conference on Tools and Algorithms for the Construction and Analysis of Systems}, location = {Braga, Portugal}, pages = {664 -- 678}, publisher = {Springer}, title = {{Model checking on trees with path equivalences}}, doi = {10.1007/978-3-540-71209-1_51}, volume = {4424}, year = {2007}, } @article{4405, abstract = {Background A central goal of Systems Biology is to model and analyze biological signaling pathways that interact with one another to form complex networks. Here we introduce Qualitative networks, an extension of Boolean networks. With this framework, we use formal verification methods to check whether a model is consistent with the laboratory experimental observations on which it is based. If the model does not conform to the data, we suggest a revised model and the new hypotheses are tested in-silico. Results We consider networks in which elements range over a small finite domain allowing more flexibility than Boolean values, and add target functions that allow to model a rich set of behaviors. We propose a symbolic algorithm for analyzing the steady state of these networks, allowing us to scale up to a system consisting of 144 elements and state spaces of approximately 1086 states. We illustrate the usefulness of this approach through a model of the interaction between the Notch and the Wnt signaling pathways in mammalian skin, and its extensive analysis. Conclusion We introduce an approach for constructing computational models of biological systems that extends the framework of Boolean networks and uses formal verification methods for the analysis of the model. This approach can scale to multicellular models of complex pathways, and is therefore a useful tool for the analysis of complex biological systems. The hypotheses formulated during in-silico testing suggest new avenues to explore experimentally. Hence, this approach has the potential to efficiently complement experimental studies in biology.}, author = {Schaub, Marc A and Thomas Henzinger and Fisher, Jasmin}, journal = {BMC Systems Biology}, number = {4}, publisher = {BioMed Central}, title = {{Qualitative networks: A symbolic approach to analyze biological signaling networks}}, doi = {10.1186/1752-0509-1-4}, volume = {1}, year = {2007}, } @inbook{4417, abstract = {Counterexample-guided abstraction refinement (CEGAR) is a powerful technique to scale automatic program analysis techniques to large programs. However, so far it has been used primarily for model checking in the context of predicate abstraction. We formalize CEGAR for general powerset domains. If a spurious abstract counterexample needs to be removed through abstraction refinement, there are often several choices, such as which program location(s) to refine, which abstract domain(s) to use at different locations, and which abstract values to compute. We define several plausible preference orderings on abstraction refinements, such as refining as “late” as possible and as “coarse” as possible. We present generic algorithms for finding refinements that are optimal with respect to the different preference orderings. We also compare the different orderings with respect to desirable properties, including the property if locally optimal refinements compose to a global optimum. Finally, we point out some difficulties with CEGAR for non-powerset domains.}, author = {Manevich, Roman and Field, John and Thomas Henzinger and Ramalingam, Ganesan and Sagiv, Mooly}, booktitle = {Program Analysis and Compilation, Theory and Practice: Essays Dedicated to Reinhard Wilhelm on the Occasion of His 60th Birthday}, pages = {273 -- 292}, publisher = {Springer}, title = {{Abstract counterexample-based refinement for powerset domains}}, doi = {10.1007/978-3-540-71322-7_13}, volume = {4444}, year = {2007}, }