@article{13425,
  abstract     = {Nanoparticles (NPs) decorated with ligands combining photoswitchable dipoles and covalent cross-linkers can be assembled by light into organized, three-dimensional suprastructures of various types and sizes. NPs covered with only few photoactive ligands form metastable crystals that can be assembled and disassembled “on demand” by using light of different wavelengths. For higher surface concentrations, self-assembly is irreversible, and the NPs organize into permanently cross-linked structures including robust supracrystals and plastic spherical aggregates.},
  author       = {Klajn, Rafal and Bishop, Kyle J. M. and Grzybowski, Bartosz A.},
  issn         = {1091-6490},
  journal      = {Proceedings of the National Academy of Sciences},
  keywords     = {Multidisciplinary},
  number       = {25},
  pages        = {10305--10309},
  publisher    = {Proceedings of the National Academy of Sciences},
  title        = {{Light-controlled self-assembly of reversible and irreversible nanoparticle suprastructures}},
  doi          = {10.1073/pnas.0611371104},
  volume       = {104},
  year         = {2007},
}

@article{13426,
  abstract     = {Photoswelling of thin films of dichromated gelatin provides a basis for fabrication of multilevel surface reliefs via sequential UV illumination through different photomasks. The remarkable feature of this simple, benchtop technique is that by adjusting irradiation times, film thickness, or its hydration state the heights of the developed features can be varied from few nanometers to tens of microns. After UV exposure, the surface structures can be replicated faithfully into either soft or hard PDMS stamps.},
  author       = {Paszewski, Maciej and Smoukov, Stoyan K. and Klajn, Rafal and Grzybowski, Bartosz A.},
  issn         = {1520-5827},
  journal      = {Langmuir},
  keywords     = {Electrochemistry, Spectroscopy, Surfaces and Interfaces, Condensed Matter Physics, General Materials Science},
  number       = {10},
  pages        = {5419--5422},
  publisher    = {American Chemical Society},
  title        = {{Multilevel surface nano- and microstructuring via sequential photoswelling of dichromated gelatin}},
  doi          = {10.1021/la062982c},
  volume       = {23},
  year         = {2007},
}

@article{13427,
  abstract     = {Deformable, spherical aggregates of metal nanoparticles connected by long-chain dithiol ligands self-assemble into nanostructured materials of macroscopic dimensions. These materials are plastic and moldable against arbitrarily shaped masters and can be thermally hardened into polycrystalline metal structures of controllable porosity. In addition, in both plastic and hardened states, the assemblies are electrically conductive and exhibit Ohmic characteristics down to ∼20 volts per meter. The self-assembly method leading to such materials is applicable both to pure metals and to bimetallic structures of various elemental compositions.},
  author       = {Klajn, Rafal and Bishop, Kyle J. M. and Fialkowski, Marcin and Paszewski, Maciej and Campbell, Christopher J. and Gray, Timothy P. and Grzybowski, Bartosz A.},
  issn         = {1095-9203},
  journal      = {Science},
  keywords     = {Multidisciplinary},
  number       = {5822},
  pages        = {261--264},
  publisher    = {American Association for the Advancement of Science},
  title        = {{Plastic and moldable metals by self-assembly of sticky nanoparticle aggregates}},
  doi          = {10.1126/science.1139131},
  volume       = {316},
  year         = {2007},
}

@inbook{167,
  abstract     = {This book contains research articles on Diophantine Geometry, written by participants of a research program held at the Ennio De Giorgi Mathematical Research Center in Pisa, Italy, during the period April – July 2005. The authors are eminent experts in the field. Several subfields of the main topic are presented; the volume thus is particularly useful to get a broad overview of recent research developments.},
  author       = {Browning, Timothy D and Heath Brown, Roger},
  booktitle    = {Diophantine Geometry},
  editor       = {Zannier, Umberto},
  pages        = {93 -- 100},
  publisher    = {Edizioni della Normale},
  title        = {{Simultaneous equal sums of three powers}},
  volume       = {4},
  year         = {2007},
}

@article{1964,
  abstract     = {Complex I of respiratory chains plays a central role in cellular energy production. Mutations in its subunits lead to many human neurodegenerative diseases. Recently, a first atomic structure of the hydrophilic domain of complex I from Thermus thermophilus was determined. This domain represents a catalytic core of the enzyme. It consists of eight different subunits, contains all the redox centers, and comprises more than half of the entire complex. In this review, novel mechanistic implications of the structure are discussed, and the effects of many known mutations of complex I subunits are interpreted in a structural context.},
  author       = {Leonid Sazanov},
  journal      = {Biochemistry},
  number       = {9},
  pages        = {2275 -- 2288},
  publisher    = {ACS},
  title        = {{Respiratory complex I: Mechanistic and structural insights provided by the crystal structure of the hydrophilic domain}},
  doi          = {10.1021/bi602508x},
  volume       = {46},
  year         = {2007},
}

@article{1965,
  abstract     = {Respiratory complex I (NADH:ubiquinone oxidoreductase) is an L-shaped multisubunit protein assembly consisting of a hydrophobic membrane arm and a hydrophilic peripheral arm. It catalyses the transfer of two electrons from NADH to quinone coupled to the translocation of four protons across the membrane. Although we have solved recently the crystal structure of the peripheral arm, the structure of the complete enzyme and the coupling mechanism are not yet known. The membrane domain of Escherichia coli complex I consists of seven different subunits with total molecular mass of 258 kDa. It is significantly more stable than the whole enzyme, which allowed us to obtain well-ordered two-dimensional crystals of the domain, belonging to the space group p22121. Comparison of the projection map of negatively stained crystals with previously published low-resolution structures indicated that the characteristic curved shape of the membrane domain is remarkably well conserved between bacterial and mitochondrial enzymes, helping us to interpret projection maps in the context of the intact complex. Two pronounced stain-excluding densities at the distal end of the membrane domain are likely to represent the two large antiporter-like subunits NuoL and NuoM. Cryo-electron microscopy on frozen-hydrated crystals allowed us to calculate a projection map at 8 Å resolution. About 60 transmembrane α-helices, both perpendicular to the membrane plane and tilted, are present within one membrane domain, which is consistent with secondary structure predictions. A possible binding site and access channel for quinone are found at the interface with the peripheral arm. Tentative assignment of individual subunits to the features of the map has been made. The location of subunits NuoL and NuoM at substantial distance from the peripheral arm, which contains all the redox centres of the complex, indicates that conformational changes are likely to play a role in the mechanism of coupling between electron transfer and proton pumping.},
  author       = {Baranova, Ekaterina A and Holt, Peter J and Leonid Sazanov},
  journal      = {Journal of Molecular Biology},
  number       = {1},
  pages        = {140 -- 154},
  publisher    = {Elsevier},
  title        = {{Projection structure of the membrane domain of Escherichia coli respiratory Complex I at 8 Å resolution}},
  doi          = {10.1016/j.jmb.2006.11.026},
  volume       = {366},
  year         = {2007},
}

@article{1969,
  abstract     = {Respiratory complex I catalyses the transfer of electrons from NADH to quinone coupled to the translocation of protons across the membrane. The mechanism of coupling and the structure of the complete enzyme are not known. The membrane domain of the complex contains three similar antiporter-like subunits NuoL/M/N, probably involved in proton pumping. We have previously shown that subunits NuoL/M can be removed from the rest of the complex, suggesting their location at the distal end of the membrane domain. Here, using electron microscopy and single particle analysis, we show that subunits NuoL and M jointly occupy a distal half of the membrane domain, separated by about 10 nm from the interface with the peripheral arm. This indicates that coupling mechanism of complex I is likely to involve long range conformational changes.},
  author       = {Baranova, Ekaterina A and Morgan, David J and Leonid Sazanov},
  journal      = {Journal of Structural Biology},
  number       = {2 SPEC. ISS.},
  pages        = {238 -- 242},
  publisher    = {Academic Press},
  title        = {{Single particle analysis confirms distal location of subunits NuoL and NuoM in Escherichia coli complex I}},
  doi          = {10.1016/j.jsb.2007.01.009},
  volume       = {159},
  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},
}