@inproceedings{4572, abstract = {We present a constraint-based algorithm for the synthesis of invariants expressed in the combined theory of linear arithmetic and uninterpreted function symbols. Given a set of programmer-specified invariant templates, our algorithm reduces the invariant synthesis problem to a sequence of arithmetic constraint satisfaction queries. Since the combination of linear arithmetic and uninterpreted functions is a widely applied predicate domain for program verification, our algorithm provides a powerful tool to statically and automatically reason about program correctness. The algorithm can also be used for the synthesis of invariants over arrays and set data structures, because satisfiability questions for the theories of sets and arrays can be reduced to the theory of linear arithmetic with uninterpreted functions. We have implemented our algorithm and used it to find invariants for a low-level memory allocator written in C.}, author = {Beyer, Dirk and Thomas Henzinger and Majumdar, Ritankar S and Rybalchenko, Andrey}, pages = {378 -- 394}, publisher = {Springer}, title = {{Invariant synthesis for combined theories}}, doi = {10.1007/978-3-540-69738-1_27}, volume = {4349}, year = {2007}, } @inproceedings{4573, abstract = {In automatic software verification, we have observed a theoretical convergence of model checking and program analysis. In practice, however, model checkers are still mostly concerned with precision, e.g., the removal of spurious counterexamples; for this purpose they build and refine reachability trees. Lattice-based program analyzers, on the other hand, are primarily concerned with efficiency. We designed an algorithm and built a tool that can be configured to perform not only a purely tree-based or a purely lattice-based analysis, but offers many intermediate settings that have not been evaluated before. The algorithm and tool take one or more abstract interpreters, such as a predicate abstraction and a shape analysis, and configure their execution and interaction using several parameters. Our experiments show that such customization may lead to dramatic improvements in the precision-efficiency spectrum.}, author = {Beyer, Dirk and Thomas Henzinger and Théoduloz, Grégory}, pages = {504 -- 518}, publisher = {Springer}, title = {{Configurable software verification: Concretizing the convergence of model checking and program analysis}}, doi = {10.1007/978-3-540-73368-3_51}, volume = {4590}, year = {2007}, } @inproceedings{4575, abstract = {We present a case study to illustrate our formalism for the specification and verification of the method-invocation behavior of web-service applications constructed from asynchronously interacting multi-threaded distributed components. Our model is expressive enough to allow the representation of recursion and dynamic thread creation, and yet permits the algorithmic analysis of the following two questions: (1) Does a given service satisfy a safety specification? (2) Can a given service be substituted by a another service in an arbitrary context? Our case study is based on the Amazon.com E-Commerce Services (ECS) platform.}, author = {Beyer, Dirk and Chakrabarti, Arindam and Thomas Henzinger and Seshia, Sanjit A}, pages = {831 -- 838}, publisher = {IEEE}, title = {{An application of web-service interfaces}}, doi = {10.1109/ICWS.2007.32 }, year = {2007}, } @article{4626, abstract = {We consider concurrent two-player games with reachability objectives. In such games, at each round, player 1 and player 2 independently and simultaneously choose moves, and the two choices determine the next state of the game. The objective of player 1 is to reach a set of target states; the objective of player 2 is to prevent this. These are zero-sum games, and the reachability objective is one of the most basic objectives: determining the set of states from which player 1 can win the game is a fundamental problem in control theory and system verification. There are three types of winning states, according to the degree of certainty with which player 1 can reach the target. From type-1 states, player 1 has a deterministic strategy to always reach the target. From type-2 states, player 1 has a randomized strategy to reach the target with probability 1. From type-3 states, player 1 has for every real ε>0 a randomized strategy to reach the target with probability greater than 1−ε. We show that for finite state spaces, all three sets of winning states can be computed in polynomial time: type-1 states in linear time, and type-2 and type-3 states in quadratic time. The algorithms to compute the three sets of winning states also enable the construction of the winning and spoiling strategies.}, author = {de Alfaro, Luca and Thomas Henzinger and Kupferman, Orna}, journal = {Theoretical Computer Science}, number = {3}, pages = {188 -- 217}, publisher = {Elsevier}, title = {{Concurrent reachability games}}, doi = {10.1016/j.tcs.2007.07.008}, volume = {386}, year = {2007}, } @inproceedings{582, abstract = {Using the techniques of "quantum weak-measurements" as a coherent amplification mechanism for small signals, for the first time we have measured the recently proposed "spin Hall effect" of light.}, author = {Onur Hosten and Kwiat, Paul G}, publisher = {OSA}, title = {{Observing the spin hall effect of light via quantum weak measurements}}, doi = {10.1364/FIO.2007.JTuA4}, year = {2007}, } @article{6150, author = {Gumienny, Tina L. and MacNeil, Lesley T. and Wang, Huang and de Bono, Mario and Wrana, Jeffrey L. and Padgett, Richard W.}, issn = {0960-9822}, journal = {Current Biology}, number = {2}, pages = {159--164}, publisher = {Elsevier}, title = {{Glypican LON-2 is a conserved negative regulator of BMP-like signaling in Caenorhabditis elegans}}, doi = {10.1016/j.cub.2006.11.065}, volume = {17}, year = {2007}, } @unpublished{6321, abstract = {These lecture notes describe the current state of affairs for Manin's conjecture in the context of del Pezzo surfaces.}, author = {Browning, Timothy D}, booktitle = {arXiv}, title = {{The Manin conjecture in dimension 2}}, year = {2007}, } @inbook{6323, abstract = {This paper surveys recent progress towards the Manin conjecture for (singular and non-singular) del Pezzo surfaces. To illustrate some of the techniques available, an upper bound of the expected order of magnitude is established for a singular del Pezzo surface of degree four.}, author = {Browning, Timothy D}, booktitle = {A Tribute to Gauss and Dirichlet}, pages = {39--56}, publisher = {American Mathematical Society}, title = {{An overview of Manin's conjecture for del Pezzo surfaces}}, volume = {7}, year = {2007}, } @article{13424, abstract = {Changing shapes: Metastable spherical aggregates of gold nanoparticles undergo a one-to-one, thermally induced transformation into heterodimers comprising connected plate and spherical domains. By controlling the reaction time, it is possible to isolate a variety of structures differing in the relative sizes of the domains and in the overall optical properties (see picture).}, author = {Klajn, Rafal and Pinchuk, Anatoliy O. and Schatz, George C. and Grzybowski, Bartosz A.}, issn = {1521-3773}, journal = {Angewandte Chemie International Edition}, keywords = {General Chemistry, Catalysis}, number = {44}, pages = {8363--8367}, publisher = {Wiley}, title = {{Synthesis of heterodimeric sphere–prism nanostructures via metastable gold supraspheres}}, doi = {10.1002/anie.200702570}, volume = {46}, year = {2007}, } @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}, } @article{904, abstract = {Background: Independently evolving lineages mostly accumulate different changes, which leads to their gradual divergence. However, parallel accumulation of identical changes is also common, especially in traits with only a small number of possible states. Results: We characterize parallelism in evolution of coding sequences in three four-species sets of genomes of mammals, Drosophila, and yeasts. Each such set contains two independent evolutionary paths, which we call paths I and II. An amino acid replacement which occurred along path I also occurs along path II with the probability 50-8211;80% of that expected under selective neutrality. Thus, the per site rate of parallel evolution of proteins is several times higher than their average rate of evolution, but still lower than the rate of evolution of neutral sequences. This deficit may be caused by changes in the fitness landscape, leading to a replacement being possible along path I but not along path II. However, constant, weak selection assumed by the nearly neutral model of evolution appears to be a more likely explanation. Then, the average coefficient of selection associated with an amino acid replacement, in the units of the effective population size, must exceed ∼0.4, and the fraction of effectively neutral replacements must be below ∼30%. At a majority of evolvable amino acid sites, only a relatively small number of different amino acids is permitted. Conclusion: High, but below-neutral, rates of parallel amino acid replacements suggest that a majority of amino acid replacements that occur in evolution are subject to weak, but non-trivial, selection, as predicted by Ohta's nearly-neutral theory.}, author = {Bazykin, Georgii A and Fyodor Kondrashov and Brudno, Michael and Poliakov, Alexander V and Dubchak, Inna L and Kondrashov, Alexey S}, journal = {Biology Direct}, publisher = {BioMed Central}, title = {{Extensive parallelism in protein evolution}}, doi = {10.1186/1745-6150-2-20}, volume = {2}, year = {2007}, } @article{9149, abstract = {The interaction of tidal currents with sea-floor topography results in the radiation of internal gravity waves into the ocean interior. These waves are called internal tides and their dissipation due to nonlinear wave breaking and concomitant three-dimensional turbulence could play an important role in the mixing of the abyssal ocean, and hence in controlling the large-scale ocean circulation. As part of on-going work aimed at providing a theory for the vertical distribution of wave breaking over sea-floor topography, in this paper we investigate the instability of internal tides in a very simple linear model that helps us to relate the formation of unstable regions to simple features in the sea-floor topography. For two-dimensional tides over one-dimensional topography we find that the formation of overturning instabilities is closely linked to the singularities in the topography shape and that it is possible to have stable waves at the sea floor and unstable waves in the ocean interior above. For three-dimensional tides over two-dimensional topography there is in addition an effect of geometric focusing of wave energy into localized regions of high wave amplitude, and we investigate this focusing effect in simple examples. Overall, we find that the distribution of unstable wave breaking regions can be highly non-uniform even for very simple idealized topography shapes.}, author = {Bühler, Oliver and Muller, Caroline J}, issn = {0022-1120}, journal = {Journal of Fluid Mechanics}, keywords = {mechanical engineering, mechanics of materials, condensed matter physics}, pages = {1--28}, publisher = {Cambridge University Press}, title = {{Instability and focusing of internal tides in the deep ocean}}, doi = {10.1017/s0022112007007410}, volume = {588}, year = {2007}, } @article{9487, abstract = {Cytosine DNA methylation is considered to be a stable epigenetic mark, but active demethylation has been observed in both plants and animals. In Arabidopsis thaliana, DNA glycosylases of the DEMETER (DME) family remove methylcytosines from DNA. Demethylation by DME is necessary for genomic imprinting, and demethylation by a related protein, REPRESSOR OF SILENCING1, prevents gene silencing in a transgenic background. However, the extent and function of demethylation by DEMETER-LIKE (DML) proteins in WT plants is not known. Using genome-tiling microarrays, we mapped DNA methylation in mutant and WT plants and identified 179 loci actively demethylated by DML enzymes. Mutations in DML genes lead to locus-specific DNA hypermethylation. Reintroducing WT DML genes restores most loci to the normal pattern of methylation, although at some loci, hypermethylated epialleles persist. Of loci demethylated by DML enzymes, >80% are near or overlap genes. Genic demethylation by DML enzymes primarily occurs at the 5′ and 3′ ends, a pattern opposite to the overall distribution of WT DNA methylation. Our results show that demethylation by DML DNA glycosylases edits the patterns of DNA methylation within the Arabidopsis genome to protect genes from potentially deleterious methylation.}, author = {Penterman, Jon and Zilberman, Daniel and Huh, Jin Hoe and Ballinger, Tracy and Henikoff, Steven and Fischer, Robert L.}, issn = {1091-6490}, journal = {Proceedings of the National Academy of Sciences}, number = {16}, pages = {6752--6757}, publisher = {National Academy of Sciences}, title = {{DNA demethylation in the Arabidopsis genome}}, doi = {10.1073/pnas.0701861104}, volume = {104}, year = {2007}, } @misc{9504, author = {Zilberman, Daniel}, booktitle = {Nature Genetics}, issn = {1546-1718}, number = {4}, pages = {442--443}, publisher = {Nature Publishing Group}, title = {{The human promoter methylome}}, doi = {10.1038/ng0407-442}, volume = {39}, year = {2007}, } @article{9524, abstract = {Cytosine methylation is the most common covalent modification of DNA in eukaryotes. DNA methylation has an important role in many aspects of biology, including development and disease. Methylation can be detected using bisulfite conversion, methylation-sensitive restriction enzymes, methyl-binding proteins and anti-methylcytosine antibodies. Combining these techniques with DNA microarrays and high-throughput sequencing has made the mapping of DNA methylation feasible on a genome-wide scale. Here we discuss recent developments and future directions for identifying and mapping methylation, in an effort to help colleagues to identify the approaches that best serve their research interests.}, author = {Zilberman, Daniel and Henikoff, Steven}, issn = {1477-9129}, journal = {Development}, number = {22}, pages = {3959--3965}, publisher = {The Company of Biologists}, title = {{Genome-wide analysis of DNA methylation patterns}}, doi = {10.1242/dev.001131}, volume = {134}, year = {2007}, } @article{1035, abstract = {We explore the rich internal structure of Cs2 Feshbach molecules. Pure ultracold molecular samples are prepared in a CO2 -laser trap, and a multitude of weakly bound states is populated by elaborate magnetic-field ramping techniques. Our methods use different Feshbach resonances as input ports and various internal level crossings for controlled state transfer. We populate higher partial-wave states of up to eight units of rotational angular momentum (l -wave states). We investigate the molecular structure by measurements of the magnetic moments for various states. Avoided level crossings between different molecular states are characterized through the changes in magnetic moment and by a Landau-Zener tunneling method. Based on microwave spectroscopy, we present a precise measurement of the magnetic-field-dependent binding energy of the weakly bound s -wave state that is responsible for the large background scattering length of Cs. This state is of particular interest because of its quantum-halo character.}, author = {Mark, Michael and Ferlaino, Francesca and Knoop, Steven and Danzl, Johann G and Kraemer, Tobias and Chin, Cheng and Nägerl, Hanns and Grimm, Rudolf}, journal = {Physical Review A - Atomic, Molecular, and Optical Physics}, number = {4}, publisher = {American Physical Society}, title = {{Spectroscopy of ultracold trapped cesium Feshbach molecules}}, doi = {10.1103/PhysRevA.76.042514}, volume = {76}, year = {2007}, } @article{11884, abstract = {About 20% of the world's population uses the Web, and a large majority thereof uses Web search engines to find information. As a result, many Web researchers are devoting much effort to improving the speed and capability of search technology.}, author = {Henzinger, Monika H}, issn = {1095-9203}, journal = {Science}, number = {5837}, pages = {468--471}, publisher = {American Association for the Advancement of Science}, title = {{Search technologies for the internet}}, doi = {10.1126/science.1126557}, volume = {317}, year = {2007}, } @inproceedings{11924, abstract = {How much can smart combinatorial algorithms improve web search engines? To address this question we will describe three algorithms that have had a positive impact on web search engines: The PageRank algorithm, algorithms for finding near-duplicate web pages, and algorithms for index server loadbalancing.}, author = {Henzinger, Monika H}, booktitle = {18th Annual ACM-SIAM Symposium on Discrete Algorithms}, isbn = {9780898716245}, location = {New Orleans, LA, United States}, pages = {1022--1026}, publisher = {Society for Industrial & Applied Mathematics}, title = {{Combinatorial algorithms for web search engines: three success stories}}, year = {2007}, }