@inproceedings{4581, abstract = {We have extended the software model checker BLAST to automatically generate test suites that guarantee full coverage with respect to a given predicate. More precisely, given a C program and a target predicate p, BLAST determines the set L of program locations which program execution can reach with p true, and automatically generates a set of test vectors that exhibit the truth of p at all locations in L. We have used BLAST to generate test suites and to detect dead code in C programs with up to 30 K lines of code. The analysis and test vector generation is fully automatic (no user intervention) and exact (no false positives).}, author = {Beyer, Dirk and Chlipala, Adam J and Thomas Henzinger and Jhala, Ranjit and Majumdar, Ritankar S}, pages = {326 -- 335}, publisher = {IEEE}, title = {{Generating tests from counterexamples}}, doi = {10.1109/ICSE.2004.1317455}, year = {2004}, } @inproceedings{4629, abstract = {Temporal logic is two-valued: a property is either true or false. When applied to the analysis of stochastic systems, or systems with imprecise formal models, temporal logic is therefore fragile: even small changes in the model can lead to opposite truth values for a specification. We present a generalization of the branching-time logic Ctl which achieves robustness with respect to model perturbations by giving a quantitative interpretation to predicates and logical operators, and by discounting the importance of events according to how late they occur. In every state, the value of a formula is a real number in the interval [0,1], where 1 corresponds to truth and 0 to falsehood. The boolean operators and and or are replaced by min and max, the path quantifiers ∃ and ∀ determine sup and inf over all paths from a given state, and the temporal operators and □ specify sup and inf over a given path; a new operator averages all values along a path. Furthermore, all path operators are discounted by a parameter that can be chosen to give more weight to states that are closer to the beginning of the path. We interpret the resulting logic Dctl over transition systems, Markov chains, and Markov decision processes. We present two semantics for Dctl: a path semantics, inspired by the standard interpretation of state and path formulas in CTL, and a fixpoint semantics, inspired by the μ-calculus evaluation of CTL formulas. We show that, while these semantics coincide for CTL, they differ for Dctl, and we provide model-checking algorithms for both semantics.}, author = {de Alfaro, Luca and Faella, Marco and Thomas Henzinger and Majumdar, Ritankar S and Stoelinga, Mariëlle}, pages = {77 -- 92}, publisher = {Springer}, title = {{Model checking discounted temporal properties}}, doi = {10.1007/978-3-540-24730-2_6}, volume = {2988}, year = {2004}, } @article{847, abstract = {The accumulation of genome-wide information on single nucleotide polymorphisms in humans provides an unprecedented opportunity to detect the evolutionary forces responsible for heterogeneity of the level of genetic variability across loci. Previous studies have shown that history of recombination events has produced long haplotype blocks in the human genome, which contribute to this heterogeneity. Other factors, however, such as natural selection or the heterogeneity of mutation rates across loci, may also lead to heterogeneity of genetic variability. We compared synonymous and non-synonymous variability within human genes with their divergence from murine orthologs. We separately analyzed the non-synonymous variants predicted to damage protein structure or function and the variants predicted to be functionally benign. The predictions were based on comparative sequence analysis and, in some cases, on the analysis of protein structure. A strong correlation between non-synonymous, benign variability and non-synonymous human-mouse divergence suggests that selection played an important role in shaping the pattern of variability in coding regions of human genes. However, the lack of correlation between deleterious variability and evolutionary divergence shows that a substantial proportion of the observed non-synonymous single-nucleotide polymorphisms reduces fitness and never reaches fixation. Evolutionary and medical implications of the impact of selection on human polymorphisms are discussed.}, author = {Sunyaev, Shamil R and Fyodor Kondrashov and Bork, Peer and Ramensky, Vasily}, journal = {Human Molecular Genetics}, number = {24}, pages = {3325 -- 3330}, publisher = {Oxford University Press}, title = {{Impact of selection, mutation rate and genetic drift on human genetic variation}}, doi = {10.1093/hmg/ddg359}, volume = {12}, year = {2003}, } @article{8519, author = {Kaloshin, Vadim}, issn = {0020-9910}, journal = {Inventiones mathematicae}, keywords = {General Mathematics}, number = {3}, pages = {451--512}, publisher = {Springer Nature}, title = {{The existential Hilbert 16-th problem and an estimate for cyclicity of elementary polycycles}}, doi = {10.1007/s00222-002-0244-9}, volume = {151}, year = {2003}, } @article{876, abstract = {Alternative splicing is thought to be a major source of functional diversity in animal proteins. We analyzed the evolutionary conservation of proteins encoded by alternatively spliced genes and predicted the ancestral state for 73 cases of alternative splicing (25 insertions and 48 deletions). The amino acid sequences of most of the inserts in proteins produced by alternative splicing are as conserved as the surrounding sequences. Thus, alternative splicing often creates novel isoforms by the insertion of new, functional protein sequences that probably originated from noncoding sequences of introns.}, author = {Fyodor Kondrashov and Koonin, Eugene V}, journal = {Trends in Genetics}, number = {3}, pages = {115 -- 119}, publisher = {Elsevier}, title = {{Evolution of alternative splicing: Deletions, insertions and origin of functional parts of proteins from intron sequences}}, doi = {10.1016/S0168-9525(02)00029-X}, volume = {19}, year = {2003}, } @article{166, abstract = {For any number field k, upper bounds are established for the number of k-rational points of bounded height on non-singular del Pezzo surfaces defined over k, which are equipped with suitable conic bundle structures over k.}, author = {Browning, Timothy D and Swarbick Jones, M}, journal = {Proceedings of the Bonn session in analytic number theory and diophantine equations}, publisher = {Mathematisches Institut der Universität Bonn}, title = {{Counting rational points on del Pezzo surfaces of degree 5}}, volume = {360}, year = {2003}, } @article{1959, abstract = {The molecular organization of bacterial NADH: ubiquinone oxidoreductase (complex I or NDH-1) is not established, apart from a rough separation into dehydrogenase, connecting and membrane domains. In this work, complex I was purified from Escherichia coli and fragmented by replacing dodecylmaltoside with other detergents. Exchange into decyl maltoside led to the removal of the hydrophobic subunit NuoL from the otherwise intact complex. Diheptanoyl phosphocholine led to the loss of NuoL and NuoM subunits, whereas other subunits remained in the complex. The presence of N,N-dimethyldodecylamine N-oxide or Triton X-100 led to further disruption of the membrane domain into fragments containing NuoL/M/N, NuoA/K/N, and NuoH/J subunits. Among the hydrophilic subunits, NuoCD was most readily dissociated from the complex, whereas NuoB was partially dissociated from the peripheral arm assembly in N,N-dimethyldodecylamine N-oxide. A model of subunit arrangement in bacterial complex I based on these data is proposed. Subunits NuoL and NuoM, which are homologous to antiporters and are implicated in proton pumping, are located at the distal end of the membrane arm, spatially separated from the redox centers of the peripheral arm. This is consistent with proposals that the mechanism of proton pumping by complex I is likely to involve long range conformational changes.}, author = {Holt, Peter J and Morgan, David J and Leonid Sazanov}, journal = {Journal of Biological Chemistry}, number = {44}, pages = {43114 -- 43120}, publisher = {American Society for Biochemistry and Molecular Biology}, title = {{The location of NuoL and NuoM subunits in the membrane domain of the Escherichia coli Complex I: implications for the mechanism of proton pumping}}, doi = {10.1074/jbc.M308247200}, volume = {278}, year = {2003}, } @article{1960, abstract = {NADH-ubiquinone oxidoreductase (complex I or NDH-1) was purified from the BL21 strain of Escherichia coli using an improved procedure. The complex was effectively stabilized by addition of divalent cations and lipids, making the preparation suitable for structural studies. The ubiquinone reductase activity of the enzyme was fully restored by addition of native E. coli lipids. Two different two-dimensional crystal forms, with p2 and p3 symmetry, were obtained using lipids containing native E. coli extracts. Analysis of the crystals showed that they are formed by fully intact complex I in an L-shaped conformation. Activity assays and single particle analysis indicated that complex I maintains this structure in detergent solution and does not adopt a different conformation in the active state. Thus, we provide the first experimental evidence that complex I from E. coli has an L-shape in a lipid bilayer and confirm that this is also the case for the active enzyme in solution. This suggests strongly that bacterial complex I exists in an L-shaped conformation in vivo. Our results also indicate that native lipids play an important role in the activation, stabilization and, as a consequence, crystallization of purified complex I from E. coli.}, author = {Leonid Sazanov and Carroll, Joe D and Holt, Peter J and Toime, Laurence J and Fearnley, Ian M}, journal = {Journal of Biological Chemistry}, number = {21}, pages = {19483 -- 19491}, publisher = {American Society for Biochemistry and Molecular Biology}, title = {{A role for native lipids in the stabilization and two dimensional crystallization of the Escherichia coli NADH ubiquinone oxidoreductase (complex I)}}, doi = {10.1074/jbc.M208959200}, volume = {278}, year = {2003}, } @article{205, author = {Timothy Browning}, journal = {Acta Arithmetica}, number = {3}, pages = {275 -- 295}, publisher = {Instytut Matematyczny}, title = {{Counting rational points on cubic and quartic surfaces}}, doi = {10.4064/aa108-3-7}, volume = {108}, year = {2003}, } @article{206, abstract = {Let T ⊂ ℙ 4 be a non-singular threefold of degree at least four. Then we show that the number of points in T(ℚ), with height at most B, is o(B 3) or B → ∞.}, author = {Timothy Browning}, journal = {Quarterly Journal of Mathematics}, number = {1}, pages = {33 -- 39}, publisher = {Unknown}, title = {{A note on the distribution of rational points on threefolds}}, doi = {10.1093/qjmath/54.1.33}, volume = {54}, year = {2003}, } @article{13436, abstract = {Cross-metathesis reactions of α,β-unsaturated sulfones and sulfoxides in the presence of molybdenum and ruthenium pre-catalysts were tested. A selective metahesis reaction was achieved between functionalized terminal olefins and vinyl sulfones by using the ‘second generation’ ruthenium catalysts 1c–h while the highly active Schrock catalyst 1b was found to be functional group incompatible with vinyl sulfones. The cross-metathesis products were isolated in good yields with an excellent (E)-selectivity. Both the molybdenum and ruthenium-based complexes were, however, incompatible with α,β- and β,γ-unsaturated sulfoxides.}, author = {Michrowska, Anna and Bieniek, Michał and Kim, Mikhail and Klajn, Rafal and Grela, Karol}, issn = {1464-5416}, journal = {Tetrahedron}, keywords = {Organic Chemistry, Drug Discovery, Biochemistry}, number = {25}, pages = {4525--4531}, publisher = {Elsevier}, title = {{Cross-metathesis reaction of vinyl sulfones and sulfoxides}}, doi = {10.1016/s0040-4020(03)00682-3}, volume = {59}, year = {2003}, } @article{1457, abstract = {Among the major mathematical approaches to mirror symmetry are those of Batyrev-Borisov and Stromdnger-Yau-Zaslow (SYZ). The first is explicit and amenable to computation but is not clearly related to the physical motivation; the second is the opposite. Furthermore, it is far from obvious that mirror partners in one sense will also be mirror partners in the other. This paper concerns a class of examples that can be shown to satisfy the requirements of SYZ, but whose Hodge numbers are also equal. This provides significant evidence in support of SYZ. Moreover, the examples are of great interest in their own right: they are spaces of flat SLr-connections on a smooth curve. The mirror is the corresponding space for the Langlands dual group PGLr. These examples therefore throw a bridge from mirror symmetry to the duality theory of Lie groups and, more broadly, to the geometric Langlands program.}, author = {Tamas Hausel and Thaddeus, Michael}, journal = {Inventiones Mathematicae}, number = {1}, pages = {197 -- 229}, publisher = {Springer}, title = {{Mirror symmetry, langlands duality, and the Hitchin system}}, doi = {10.1007/s00222-003-0286-7}, volume = {153}, year = {2003}, } @article{1458, abstract = {The moduli space of stable bundles of rank $2$ and degree $1$ on a Riemann surface has rational cohomology generated by the so-called universal classes. The work of Baranovsky, King-Newstead, Siebert-Tian and Zagier provided a complete set of relations between these classes, expressed in terms of a recursion in the genus. This paper accomplishes the same thing for the noncompact moduli spaces of Higgs bundles, in the sense of Hitchin and Simpson. There are many more independent relations than for stable bundles, but in a sense the answer is simpler, since the formulas are completely explicit, not recursive. The results of Kirwan on equivariant cohomology for holomorphic circle actions are of key importance.}, author = {Tamas Hausel and Thaddeus, Michael}, journal = {Journal of the American Mathematical Society}, number = {2}, pages = {303 -- 329}, publisher = {American Mathematical Society}, title = {{Relations in the cohomology ring of the moduli space of rank 2 Higgs bundles}}, doi = {10.1090/S0894-0347-02-00417-4}, volume = {16}, year = {2003}, } @article{1459, abstract = {In this paper we explicitly calculate the analogue of the 't Hooft SU (2) Yang-Mills instantons on Gibbons-Hawking multi-centered gravitational instantons, which come in two parallel families: the multi-Eguchi-Hanson, or Ak ALE gravitational instantons and the multi-Taub-NUT spaces, or Ak ALF gravitational instantons. We calculate their energy and find the reducible ones. Following Kronheimer we also exploit the U(1) invariance of our solutions and study the corresponding explicit singular SU (2) magnetic monopole solutions of the Bogomolny equations on flat ℝ3.}, author = {Etesi, Gábor and Tamas Hausel}, journal = {Communications in Mathematical Physics}, number = {2}, pages = {275 -- 288}, publisher = {Springer}, title = {{On Yang-Mills instantons over multi-centered gravitational instantons}}, doi = {10.1007/s00220-003-0806-8}, volume = {235}, year = {2003}, } @article{576, abstract = {We study the free expansion of a pancake-shaped Bose-condensed gas, which is initially trapped under harmonic confinement and containing a vortex at its centre. In the case of a radial expansion holding the axial confinement fixed we consider various models for the interactions, depending on the thickness of the condensate relative to the value of the scattering length. We are thus able to evaluate different scattering regimes ranging from quasi-three-dimensional (Q3D) to strictly two-dimensional (2D). We find that as the system goes from Q3D to 2D the expansion rate of the condensate increases whereas that of the vortex core decreases. In the Q3D scattering regime we also examine a fully free expansion in 3D and find oscillatory behaviour for the vortex core radius: an initial fast expansion of the vortex core is followed by a slowing down. Such a nonuniform expansion rate of the vortex core implies that the timing of its observation should be chosen appropriately.}, author = {Onur Hosten and Vignolo, Patrizia and Minguzzi, Anna and Tanatar, Bilal and Tosi, Mario P}, journal = {Journal of Physics B: Atomic, Molecular and Optical Physics}, number = {12}, pages = {2455 -- 2463}, publisher = {IOP Publishing Ltd.}, title = {{Free expansion of two-dimensional condensates with a vortex}}, doi = {10.1088/0953-4075/36/12/306}, volume = {36}, year = {2003}, } @article{6156, abstract = {Social and solitary feeding in natural Caenorhabditis elegans isolates are associated with two alleles of the orphan G-protein-coupled receptor (GPCR) NPR-1: social feeders contain NPR-1 215F, whereas solitary feeders contain NPR-1 215V. Here we identify FMRFamide-related neuropeptides (FaRPs) encoded by the flp-18 and flp-21 genes as NPR-1 ligands and show that these peptides can differentially activate the NPR-1 215F and NPR-1 215V receptors. Multicopy overexpression of flp-21 transformed wild social animals into solitary feeders. Conversely, a flp-21 deletion partially phenocopied the npr-1(null) phenotype, which is consistent with NPR-1 activation by FLP-21 in vivo but also implicates other ligands for NPR-1. Phylogenetic studies indicate that the dominant npr-1 215V allele likely arose from an ancestral npr-1 215F gene in C. elegans. Our data suggest a model in which solitary feeding evolved in an ancestral social strain of C. elegans by a gain-of-function mutation that modified the response of NPR-1 to FLP-18 and FLP-21 ligands.}, author = {Rogers, Candida and Reale, Vincenzina and Kim, Kyuhyung and Chatwin, Heather and Li, Chris and Evans, Peter and de Bono, Mario}, issn = {1097-6256}, journal = {Nature Neuroscience}, number = {11}, pages = {1178--1185}, publisher = {Springer Nature}, title = {{Inhibition of Caenorhabditis elegans social feeding by FMRFamide-related peptide activation of NPR-1}}, doi = {10.1038/nn1140}, volume = {6}, year = {2003}, } @article{6157, abstract = {In many animal species individuals aggregate to live in groups. A range of experimental approaches in different animals, including studies of social feeding in nematodes, maternal behavior in rats and sheep, and pair-bonding in voles, are providing insights into the neural bases for these behaviors. These studies are delineating multiple neural circuits and gene networks in the brain that interact in ways that are as yet poorly understood to coordinate social behavior.}, author = {de Bono, Mario}, issn = {0022-3034}, journal = {Journal of Neurobiology}, number = {1}, pages = {78--92}, publisher = {Wiley}, title = {{Molecular approaches to aggregation behavior and social attachment}}, doi = {10.1002/neu.10162}, volume = {54}, year = {2003}, } @article{9455, abstract = {Proteins of the ARGONAUTE family are important in diverse posttranscriptional RNA-mediated gene-silencing systems as well as in transcriptional gene silencing in Drosophila and fission yeast and in programmed DNA elimination in Tetrahymena. We cloned ARGONAUTE4 (AGO4) from a screen for mutants that suppress silencing of the Arabidopsis SUPERMAN(SUP) gene. The ago4-1 mutant reactivated silentSUP alleles and decreased CpNpG and asymmetric DNA methylation as well as histone H3 lysine-9 methylation. In addition,ago4-1 blocked histone and DNA methylation and the accumulation of 25-nucleotide small interfering RNAs (siRNAs) that correspond to the retroelement AtSN1. These results suggest that AGO4 and long siRNAs direct chromatin modifications, including histone methylation and non-CpG DNA methylation.}, author = {Zilberman, Daniel and Cao, Xiaofeng and Jacobsen, Steven E.}, issn = {1095-9203}, journal = {Science}, keywords = {Multidisciplinary}, number = {5607}, pages = {716--719}, publisher = {American Association for the Advancement of Science}, title = {{ARGONAUTE4 control of locus-specific siRNA accumulation and DNA and histone methylation}}, doi = {10.1126/science.1079695}, volume = {299}, year = {2003}, } @article{9495, abstract = {RNA interference is a conserved process in which double-stranded RNA is processed into 21–25 nucleotide siRNAs that trigger posttranscriptional gene silencing. In addition, plants display a phenomenon termed RNA-directed DNA methylation (RdDM) in which DNA with sequence identity to silenced RNA is de novo methylated at its cytosine residues. This methylation is not only at canonical CpG sites but also at cytosines in CpNpG and asymmetric sequence contexts. In this report, we study the role of the DRM and CMT3 DNA methyltransferase genes in the initiation and maintenance of RdDM. Neither drm nor cmt3 mutants affected the maintenance of preestablished RNA-directed CpG methylation. However, drm mutants showed a nearly complete loss of asymmetric methylation and a partial loss of CpNpG methylation. The remaining asymmetric and CpNpG methylation was dependent on the activity of CMT3, showing that DRM and CMT3 act redundantly to maintain non-CpG methylation. These DNA methyltransferases appear to act downstream of siRNAs, since drm1 drm2 cmt3 triple mutants show a lack of non-CpG methylation but elevated levels of siRNAs. Finally, we demonstrate that DRM activity is required for the initial establishment of RdDM in all sequence contexts including CpG, CpNpG, and asymmetric sites.}, author = {Cao, Xiaofeng and Aufsatz, Werner and Zilberman, Daniel and Mette, M.Florian and Huang, Michael S. and Matzke, Marjori and Jacobsen, Steven E.}, issn = {1879-0445}, journal = {Current Biology}, number = {24}, pages = {2212--2217}, publisher = {Elsevier}, title = {{Role of the DRM and CMT3 methyltransferases in RNA-directed DNA methylation}}, doi = {10.1016/j.cub.2003.11.052}, volume = {13}, year = {2003}, } @article{11121, abstract = {In metazoa, the nuclear envelope breaks down and reforms during each cell cycle. Nuclear pore complexes (NPCs), which serve as channels for transport between the nucleus and cytoplasm1, assemble into the reforming nuclear envelope in a sequential process involving association of a subset of NPC proteins, nucleoporins, with chromatin followed by the formation of a closed nuclear envelope fenestrated by NPCs2,3,4,5,6,7. How chromatin recruitment of nucleoporins and NPC assembly are regulated is unknown. Here we demonstrate that RanGTP production is required to dissociate nucleoporins Nup107, Nup153 and Nup358 from Importin β, to target them to chromatin and to induce association between separate NPC subcomplexes. Additionally, either an excess of RanGTP or removal of Importin β induces formation of NPC-containing membrane structures—annulate lamellae—both in vitro in the absence of chromatin and in vivo. Annulate lamellae formation is strongly and specifically inhibited by an excess of Importin β. The data demonstrate that RanGTP triggers distinct steps of NPC assembly, and suggest a mechanism for the spatial restriction of NPC assembly to the surface of chromatin.}, author = {Walther, Tobias C. and Askjaer, Peter and Gentzel, Marc and Habermann, Anja and Griffiths, Gareth and Wilm, Matthias and Mattaj, Iain W. and HETZER, Martin W}, issn = {1476-4687}, journal = {Nature}, keywords = {Multidisciplinary}, number = {6949}, pages = {689--694}, publisher = {Springer Nature}, title = {{RanGTP mediates nuclear pore complex assembly}}, doi = {10.1038/nature01898}, volume = {424}, year = {2003}, }