@inproceedings{10906, abstract = {HSF(C) is a tool that automates verification of safety and liveness properties for C programs. This paper describes the verification approach taken by HSF(C) and provides instructions on how to install and use the tool.}, author = {Grebenshchikov, Sergey and Gupta, Ashutosh and Lopes, Nuno P. and Popeea, Corneliu and Rybalchenko, Andrey}, booktitle = {Tools and Algorithms for the Construction and Analysis of Systems}, editor = {Flanagan, Cormac and König, Barbara}, isbn = {9783642287558}, issn = {1611-3349}, location = {Tallinn, Estonia}, pages = {549--551}, publisher = {Springer}, title = {{HSF(C): A software verifier based on Horn clauses}}, doi = {10.1007/978-3-642-28756-5_46}, volume = {7214}, year = {2012}, } @article{11089, abstract = {The Nuclear Envelope (NE) contains over 100 different proteins that associate with nuclear components such as chromatin, the lamina and the transcription machinery. Mutations in genes encoding NE proteins have been shown to result in tissue-specific defects and disease, suggesting cell-type specific differences in NE composition and function. Consistent with these observations, recent studies have revealed unexpected functions for numerous NE associated proteins during cell differentiation and development. Here we review the latest insights into the roles played by the NE in cell differentiation, development, disease and aging, focusing primarily on inner nuclear membrane (INM) proteins and nuclear pore components.}, author = {Gomez-Cavazos, J Sebastian and HETZER, Martin W}, issn = {0955-0674}, journal = {Current Opinion in Cell Biology}, keywords = {Cell Biology}, number = {6}, pages = {775--783}, publisher = {Elsevier}, title = {{Outfits for different occasions: tissue-specific roles of Nuclear Envelope proteins}}, doi = {10.1016/j.ceb.2012.08.008}, volume = {24}, year = {2012}, } @article{11090, abstract = {Nuclear export of mRNAs is thought to occur exclusively through nuclear pore complexes. In this issue of Cell, Speese et al. identify an alternate pathway for mRNA export in muscle cells where ribonucleoprotein complexes involved in forming neuromuscular junctions transit the nuclear envelope by fusing with and budding through the nuclear membrane.}, author = {Hatch, Emily M. and HETZER, Martin W}, issn = {0092-8674}, journal = {Cell}, keywords = {General Biochemistry, Genetics and Molecular Biology}, number = {4}, pages = {733--735}, publisher = {Elsevier}, title = {{RNP export by nuclear envelope budding}}, doi = {10.1016/j.cell.2012.04.018}, volume = {149}, year = {2012}, } @article{11091, abstract = {Neoplastic cells are often characterized by specific morphological abnormalities of the nuclear envelope (NE), which have been used for cancer diagnosis for more than a century. The NE is a double phospholipid bilayer that encapsulates the nuclear genome, regulates all nuclear trafficking of RNAs and proteins and prevents the passive diffusion of macromolecules between the nucleoplasm and the cytoplasm. Whether there is a consequence to the proper functioning of the cell and loss of structural integrity of the nucleus remains unclear. Using live cell imaging, we characterize a phenomenon wherein nuclei of several proliferating human cancer cell lines become temporarily ruptured during interphase. Strikingly, NE rupturing was associated with the mislocalization of nucleoplasmic and cytoplasmic proteins and, in the most extreme cases, the entrapment of cytoplasmic organelles in the nuclear interior. In addition, we observed the formation of micronuclei-like structures during interphase and the movement of chromatin out of the nuclear space. The frequency of these NE rupturing events was higher in cells in which the nuclear lamina, a network of intermediate filaments providing mechanical support to the NE, was not properly formed. Our data uncover the existence of a NE instability that has the potential to change the genomic landscape of cancer cells.}, author = {Vargas, Jesse D. and Hatch, Emily M. and Anderson, Daniel J. and HETZER, Martin W}, issn = {1949-1042}, journal = {Nucleus}, keywords = {Cell Biology}, number = {1}, pages = {88--100}, publisher = {Taylor & Francis}, title = {{Transient nuclear envelope rupturing during interphase in human cancer cells}}, doi = {10.4161/nucl.18954}, volume = {3}, year = {2012}, } @article{11092, abstract = {To combat the functional decline of the proteome, cells use the process of protein turnover to replace potentially impaired polypeptides with new functional copies. We found that extremely long-lived proteins (ELLPs) did not turn over in postmitotic cells of the rat central nervous system. These ELLPs were associated with chromatin and the nuclear pore complex, the central transport channels that mediate all molecular trafficking in and out of the nucleus. The longevity of these proteins would be expected to expose them to potentially harmful metabolites, putting them at risk of accumulating damage over extended periods of time. Thus, it is possible that failure to maintain proper levels and functional integrity of ELLPs in nonproliferative cells might contribute to age-related deterioration in cell and tissue function.}, author = {Savas, Jeffrey N. and Toyama, Brandon H. and Xu, Tao and Yates, John R. and HETZER, Martin W}, issn = {1095-9203}, journal = {Science}, keywords = {Multidisciplinary}, number = {6071}, pages = {942--942}, publisher = {American Association for the Advancement of Science}, title = {{Extremely long-lived nuclear pore proteins in the rat brain}}, doi = {10.1126/science.1217421}, volume = {335}, year = {2012}, } @article{11093, abstract = {Nuclear pore complexes (NPCs) are built from ∼30 different proteins called nucleoporins or Nups. Previous studies have shown that several Nups exhibit cell-type-specific expression and that mutations in NPC components result in tissue-specific diseases. Here we show that a specific change in NPC composition is required for both myogenic and neuronal differentiation. The transmembrane nucleoporin Nup210 is absent in proliferating myoblasts and embryonic stem cells (ESCs) but becomes expressed and incorporated into NPCs during cell differentiation. Preventing Nup210 production by RNAi blocks myogenesis and the differentiation of ESCs into neuroprogenitors. We found that the addition of Nup210 to NPCs does not affect nuclear transport but is required for the induction of genes that are essential for cell differentiation. Our results identify a single change in NPC composition as an essential step in cell differentiation and establish a role for Nup210 in gene expression regulation and cell fate determination.}, author = {D'Angelo, Maximiliano A. and Gomez-Cavazos, J. Sebastian and Mei, Arianna and Lackner, Daniel H. and HETZER, Martin W}, issn = {1534-5807}, journal = {Developmental Cell}, keywords = {Developmental Biology, Cell Biology, General Biochemistry, Genetics and Molecular Biology, Molecular Biology}, number = {2}, pages = {446--458}, publisher = {Elsevier}, title = {{A change in nuclear pore complex composition regulates cell differentiation}}, doi = {10.1016/j.devcel.2011.11.021}, volume = {22}, year = {2012}, } @article{113, abstract = {Although liquids typically flow around intruding objects, a counterintuitive phenomenon occurs in dense suspensions of micrometre-sized particles: they become liquid-like when perturbed lightly, but harden when driven strongly. Rheological experiments have investigated how such thickening arises under shear, and linked it to hydrodynamic interactions or granular dilation. However, neither of these mechanisms alone can explain the ability of suspensions to generate very large, positive normal stresses under impact. To illustrate the phenomenon, such stresses can be large enough to allow a person to run across a suspension without sinking, and far exceed the upper limit observed under shear or extension. Here we show that these stresses originate from an impact-generated solidification front that transforms an initially compressible particle matrix into a rapidly growing jammed region, ultimately leading to extraordinary amounts of momentum absorption. Using high-speed videography, embedded force sensing and X-ray imaging, we capture the detailed dynamics of this process as it decelerates a metal rod hitting a suspension of cornflour (cornstarch) in water. We develop a model for the dynamic solidification and its effect on the surrounding suspension that reproduces the observed behaviour quantitatively. Our findings suggest that prior interpretations of the impact resistance as dominated by shear thickening need to be revisited.}, author = {Waitukaitis, Scott R and Jaeger, Heinrich}, journal = {Nature}, number = {7406}, pages = {205 -- 209}, publisher = {Nature Publishing Group}, title = {{Impact-activated solidification of dense suspensions via dynamic jamming fronts}}, doi = {10.1038/nature11187}, volume = {487}, year = {2012}, } @article{114, abstract = {We report on an investigation of the solidification of a cornstarch and water suspension during normal impact on its surface. We find that a finite time after impact, the suspension displays characteristics reminiscent of a solid, including localized stress transmission, the development of a yield stress, and some elastic energy storage. The time dependence of these characteristics depends on the thickness of the cornstarch layer, showing that the solidification is a dynamic process driven by the impacting object. These findings confirm previous speculations that rapidly applied normal stress transforms the normally fluid-like suspension into a temporarily jammed solid and draw a clear distinction between the effects of normal stress and shear stress in dense suspensions.}, author = {Waitukaitis, Scott R and Jaeger, Heinrich}, journal = {Revista Cubana de Fisica}, number = {1E}, pages = {1E31 -- 1E33}, publisher = {Universidad de La Habana}, title = {{Solidification of a cornstarch and water suspension}}, volume = {29}, year = {2012}, } @inproceedings{11656, abstract = {Suppose your sole interest in recommending a product to me is to maximize the amount paid to you by the seller for a sequence of recommendations. How should you recommend optimally if I become more inclined to ignore you with each irrelevant recommendation you make? Finding an answer to this question is a key challenge in all forms of marketing that rely on and explore social ties; ranging from personal recommendations to viral marketing. We prove that even if the recommendee regains her initial trust on each successful recommendation, the expected revenue the recommender can make over an infinite period due to payments by the seller is bounded. This can only be overcome when the recommendee also incrementally regains trust during periods without any recommendation. Here, we see a connection to "banner blindness," suggesting that showing fewer ads can lead to a higher long-term revenue.}, author = {Dütting, Paul and Henzinger, Monika H and Weber, Ingmar}, booktitle = {Proceedings of the 21st ACM international conference on Information and knowledge management}, isbn = {9781450311564}, location = {Maui, HI, United States}, pages = {2268--2286}, publisher = {Association for Computing Machinery}, title = {{Maximizing revenue from strategic recommendations under decaying trust}}, doi = {10.1145/2396761.2398621}, year = {2012}, } @article{11751, abstract = {The Seebeck coefficients, electrical resistivities, total thermal conductivities, and magnetization are reported for temperatures between 5 and 350 K for n-type Bi0.88Sb0.12 nano-composite alloys made by Ho-doping at the 0, 1, and 3 % atomic levels. The alloys were prepared using a dc hot-pressing method, and are shown to be single phase for both Ho contents with grain sizes on the average of 900 nm. We find the parent compound has a maximum of ZT = 0.28 at 231 K, while doping 1 % Ho increases the maximum ZT to 0.31 at 221 K and the 3 % doped sample suppresses the maximum ZT = 0.24 at a temperature of 260 K.}, author = {Lukas, K. C. and Joshi, G. and Modic, Kimberly A and Ren, Z. F. and Opeil, C. P.}, issn = {1573-4803}, journal = {Journal of Materials Science}, number = {15}, pages = {5729--5734}, publisher = {Springer Nature}, title = {{Thermoelectric properties of Ho-doped Bi0.88Sb0.12}}, doi = {10.1007/s10853-012-6463-6}, volume = {47}, year = {2012}, } @inproceedings{11794, abstract = {We study individual rational, Pareto optimal, and incentive compatible mechanisms for auctions with heterogeneous items and budget limits. For multi-dimensional valuations we show that there can be no deterministic mechanism with these properties for divisible items. We use this to show that there can also be no randomized mechanism that achieves this for either divisible or indivisible items. For single-dimensional valuations we show that there can be no deterministic mechanism with these properties for indivisible items, but that there is a randomized mechanism that achieves this for either divisible or indivisible items. The impossibility results hold for public budgets, while the mechanism allows private budgets, which is in both cases the harder variant to show. While all positive results are polynomial-time algorithms, all negative results hold independent of complexity considerations.}, author = {Dütting, Paul and Henzinger, Monika H and Starnberger, Martin}, booktitle = {8th International Workshop on Internet and Network Economics}, isbn = {9783642353109}, issn = {1611-3349}, location = {Liverpool, United Kingdom}, pages = {44–57}, publisher = {Springer Nature}, title = {{Auctions with heterogeneous items and budget limits}}, doi = {10.1007/978-3-642-35311-6_4}, volume = {7695}, year = {2012}, } @inproceedings{11795, abstract = {We study multiple keyword sponsored search auctions with budgets. Each keyword has multiple ad slots with a click-through rate. The bidders have additive valuations, which are linear in the click-through rates, and budgets, which are restricting their overall payments. Additionally, the number of slots per keyword assigned to a bidder is bounded. We show the following results: (1) We give the first mechanism for multiple keywords, where click-through rates differ among slots. Our mechanism is incentive compatible in expectation, individually rational in expectation, and Pareto optimal. (2) We study the combinatorial setting, where each bidder is only interested in a subset of the keywords. We give an incentive compatible, individually rational, Pareto optimal, and deterministic mechanism for identical click-through rates. (3) We give an impossibility result for incentive compatible, individually rational, Pareto optimal, and deterministic mechanisms for bidders with diminishing marginal valuations.}, author = {Colini-Baldeschi, Riccardo and Henzinger, Monika H and Leonardi, Stefano and Starnberger, Martin}, booktitle = {39th International Colloquium on Automata, Languages, and Programming}, isbn = {9783642315848}, issn = {0302-9743}, location = {Warwick, United Kingdom}, pages = {1–12}, publisher = {Springer Nature}, title = {{On multiple keyword sponsored search auctions with budgets}}, doi = {10.1007/978-3-642-31585-5_1}, volume = {7392}, year = {2012}, } @article{11963, abstract = {Peroxides and ethers in flow: 2-Carbonyl-substituted phenols and β-ketoesters react safely with ethers in a microreactor environment using a copper catalyst and an organic peroxide (TBHP). This protocol results in unsymmetrical acetal scaffolds not easily available otherwise (see scheme).}, author = {Kumar, G. Sathish and Pieber, Bartholomäus and Reddy, K. Rajender and Kappe, C. Oliver}, issn = {1521-3765}, journal = {Chemistry - A European Journal}, number = {20}, pages = {6124--6128}, publisher = {Wiley}, title = {{Copper-catalyzed formation of C-O bonds by direct α-C-H bond activation of ethers using stoichiometric amounts of peroxide in batch and continuous-flow formats}}, doi = {10.1002/chem.201200815}, volume = {18}, year = {2012}, } @article{11964, abstract = {A detailed investigation on the direct arylation of benzene with aryl bromides by using first-row transition metals under high-temperature/high-pressure (high-T/p) conditions is described. By employing a parallel reactor platform for rapid reaction screening and discovery at elevated temperatures, various metal/ligand/base combinations were evaluated for their ability to enable biaryl formation through C-H activation. The combination of cobalt(III) acetylacetonate and lithium bis(trimethylsilyl)amide was subjected to further process intensification at 200 °C (15 bar), allowing a significant reduction of the catalyst/base loading and a dramatic increase in catalytic efficiency (turnover frequency) by a factor of 1000 compared to traditional protocols. The high-throughput screening additionally identified novel nickel- and copper-based metal/ligand combinations that favored an amination pathway competing with C-H activation, with the addition of ligands, such as 1,10-phenanthroline, having a profound influence on the selectivity. In addition to metal-based catalysts, high-T/p process windows were also successfully applied to transition-metal-free systems, utilizing 1,10-phenanthroline as organocatalyst.}, author = {Pieber, Bartholomäus and Cantillo, David and Kappe, C. Oliver}, issn = {1521-3765}, journal = {Chemistry – A European Journal}, number = {16}, pages = {5047--5055}, publisher = {Wiley}, title = {{Direct arylation of benzene with aryl bromides using high‐temperature/high‐pressure process windows: Expanding the scope of C-H activation chemistry}}, doi = {10.1002/chem.201103748}, volume = {18}, year = {2012}, } @article{2073, abstract = {Background: Drosophila albomicans is a unique model organism for studying both sex chromosome and B chromosome evolution. A pair of its autosomes comprising roughly 40% of the whole genome has fused to the ancient X and Y chromosomes only about 0.12 million years ago, thereby creating the youngest and most gene-rich neo-sex system reported to date. This species also possesses recently derived B chromosomes that show non-Mendelian inheritance and significantly influence fertility.Methods: We sequenced male flies with B chromosomes at 124.5-fold genome coverage using next-generation sequencing. To characterize neo-Y specific changes and B chromosome sequences, we also sequenced inbred female flies derived from the same strain but without B's at 28.5-fold.Results: We assembled a female genome and placed 53% of the sequence and 85% of the annotated proteins into specific chromosomes, by comparison with the 12 Drosophila genomes. Despite its very recent origin, the non-recombining neo-Y chromosome shows various signs of degeneration, including a significant enrichment of non-functional genes compared to the neo-X, and an excess of tandem duplications relative to other chromosomes. We also characterized a B-chromosome linked scaffold that contains an actively transcribed unit and shows sequence similarity to the subcentromeric regions of both the ancient X and the neo-X chromosome.Conclusions: Our results provide novel insights into the very early stages of sex chromosome evolution and B chromosome origination, and suggest an unprecedented connection between the births of these two systems in D. albomicans.}, author = {Zhou, Qi and Zhu, Hongmei and Huang, Quanfei and Zhao, Li and Zhang, Guo J and Roy, Scott W and Beatriz Vicoso and Xuan, Zhaolin and Ruan, Jue and Zhang, Yue and Zhao, Ruoping and Ye, Chen and Zhang, Xiuqing and Wang, Jùn and Wang, Wen and Bachtrog, Doris}, journal = {BMC Genomics}, number = {1}, publisher = {BioMed Central}, title = {{Deciphering neo-sex and B chromosome evolution by the draft genome of Drosophila albomicans}}, doi = {10.1186/1471-2164-13-109}, volume = {13}, year = {2012}, } @article{2079, abstract = {We introduce an algorithm and representation for fabricating 3D shape abstractions using mutually intersecting planar cut-outs. The planes have prefabricated slits at their intersections and are assembled by sliding them together. Often such abstractions are used as a sculptural art form or in architecture and are colloquially called ‘cardboard sculptures’. Based on an analysis of construction rules, we propose an extended binary space partitioning tree as an efficient representation of such cardboard models which allows us to quickly evaluate the feasibility of newly added planar elements. The complexity of insertion order quickly increases with the number of planar elements and manual analysis becomes intractable. We provide tools for generating cardboard sculptures with guaranteed constructibility. In combination with a simple optimization and sampling strategy for new elements, planar shape abstraction models can be designed by iteratively adding elements. As an output, we obtain a fabrication plan that can be printed or sent to a laser cutter. We demonstrate the complete process by designing and fabricating cardboard models of various well-known 3D shapes.}, author = {Hildebrand, Kristian and Bernd Bickel and Alexa, Marc}, journal = {Computer Graphics Forum}, number = {2pt3}, pages = {583 -- 592}, publisher = {Wiley-Blackwell}, title = {{crdbrd: Shape fabrication by sliding planar slices}}, doi = {10.1111/j.1467-8659.2012.03037.x}, volume = {31}, year = {2012}, } @article{2101, abstract = {Articulated deformable characters are widespread in computer animation. Unfortunately, we lack methods for their automatic fabrication using modern additive manufacturing (AM) technologies. We propose a method that takes a skinned mesh as input, then estimates a fabricatable single-material model that approximates the 3D kinematics of the corresponding virtual articulated character in a piecewise linear manner. We first extract a set of potential joint locations. From this set, together with optional, user-specified range constraints, we then estimate mechanical friction joints that satisfy inter-joint non-penetration and other fabrication constraints. To avoid brittle joint designs, we place joint centers on an approximate medial axis representation of the input geometry, and maximize each joint's minimal cross-sectional area. We provide several demonstrations, manufactured as single, assembled pieces using 3D printers. }, author = {Bac̈her, Moritz and Bernd Bickel and James, Doug L and Pfister, Hanspeter}, journal = {ACM Transactions on Graphics}, number = {4}, publisher = {ACM}, title = {{Fabricating articulated characters from skinned meshes}}, doi = {10.1145/2185520.2185543}, volume = {31}, year = {2012}, } @article{2102, abstract = {We propose a complete process for designing, simulating, and fabricating synthetic skin for an animatronics character that mimics the face of a given subject and its expressions. The process starts with measuring the elastic properties of a material used to manufacture synthetic soft tissue. Given these measurements we use physicsbased simulation to predict the behavior of a face when it is driven by the underlying robotic actuation. Next, we capture 3D facial expressions for a given target subject. As the key component of our process, we present a novel optimization scheme that determines the shape of the synthetic skin as well as the actuation parameters that provide the best match to the target expressions. We demonstrate this computational skin design by physically cloning a real human face onto an animatronics figure. }, author = {Bernd Bickel and Kaufmann, Peter and Skouras, Mélina and Thomaszewski, Bernhard and Bradley, Derek J and Beeler, Thabo and Jackson, Philip V and Marschner, Steve and Matusik, Wojciech and Groß, Markus S}, journal = {ACM Transactions on Graphics}, number = {4}, publisher = {ACM}, title = {{Physical face cloning}}, doi = {10.1145/2185520.2185614}, volume = {31}, year = {2012}, } @article{2103, abstract = {Although facial hair plays an important role in individual expression, facial-hair reconstruction is not addressed by current facecapture systems. Our research addresses this limitation with an algorithm that treats hair and skin surface capture together in a coupled fashion so that a high-quality representation of hair fibers as well as the underlying skin surface can be reconstructed. We propose a passive, camera-based system that is robust against arbitrary motion since all data is acquired within the time period of a single exposure. Our reconstruction algorithm detects and traces hairs in the captured images and reconstructs them in 3D using a multiview stereo approach. Our coupled skin-reconstruction algorithm uses information about the detected hairs to deliver a skin surface that lies underneath all hairs irrespective of occlusions. In dense regions like eyebrows, we employ a hair-synthesis method to create hair fibers that plausibly match the image data. We demonstrate our scanning system on a number of individuals and show that it can successfully reconstruct a variety of facial-hair styles together with the underlying skin surface.}, author = {Beeler, Thabo and Bernd Bickel and Noris, Gioacchino and Beardsley, Paul A and Marschner, Steve and Sumner, Robert W and Groß, Markus S}, journal = {ACM Transactions on Graphics}, number = {4}, publisher = {ACM}, title = {{Coupled 3D reconstruction of sparse facial hair and skin}}, doi = {10.1145/2185520.2185613}, volume = {31}, year = {2012}, } @inproceedings{2104, abstract = {In recent years, various methods have been introduced to exploit pre-recorded data to improve the performance and/or realism of dynamic deformations, but their differences and similarities have not been adequately analyzed or discussed. So far, the proposed methods have been explored mainly in the research context. They have not been adopted by the computer graphics industry. This course bridges the gap between research labs and industry to present a unifying theory and understanding of data-driven methods for dynamic deformations that may inspire development of novel solutions. It focuses on application of data-driven methods to three areas of computer animation: dynamic deformation of faces, soft volumetric tissue, and cloth. And it describes how to approach these challenges in a data-driven manner, classifies the various methods, and demonstrates how data-driven methods can work in other settings. }, author = {Otaduy, Miguel A and Bernd Bickel and Bradley, Derek J and Wang, Huamin}, publisher = {ACM}, title = {{Data-driven simulation methods in computer graphics: Cloth, tissue and faces}}, doi = {10.1145/2343483.2343495}, year = {2012}, }