TY - CONF AB - We propose a logic-based framework for automated reasoning about sequential programs manipulating singly-linked lists and arrays with unbounded data. We introduce the logic SLAD, which allows combining shape constraints, written in a fragment of Separation Logic, with data and size constraints. We address the problem of checking the entailment between SLAD formulas, which is crucial in performing pre-post condition reasoning. Although this problem is undecidable in general for SLAD, we propose a sound and powerful procedure that is able to solve this problem for a large class of formulas, beyond the capabilities of existing techniques and tools. We prove that this procedure is complete, i.e., it is actually a decision procedure for this problem, for an important fragment of SLAD including known decidable logics. We implemented this procedure and shown its preciseness and its efficiency on a significant benchmark of formulas. AU - Bouajjani, Ahmed AU - Dragoi, Cezara AU - Enea, Constantin AU - Sighireanu, Mihaela ID - 10903 SN - 0302-9743 T2 - Automated Technology for Verification and Analysis TI - Accurate invariant checking for programs manipulating lists and arrays with infinite data VL - 7561 ER - TY - CONF AB - Energy games belong to a class of turn-based two-player infinite-duration games played on a weighted directed graph. It is one of the rare and intriguing combinatorial problems that lie in NP ∩ co−NP, but are not known to be in P. While the existence of polynomial-time algorithms has been a major open problem for decades, there is no algorithm that solves any non-trivial subclass in polynomial time. In this paper, we give several results based on the weight structures of the graph. First, we identify a notion of penalty and present a polynomial-time algorithm when the penalty is large. Our algorithm is the first polynomial-time algorithm on a large class of weighted graphs. It includes several counter examples that show that many previous algorithms, such as value iteration and random facet algorithms, require at least sub-exponential time. Our main technique is developing the first non-trivial approximation algorithm and showing how to convert it to an exact algorithm. Moreover, we show that in a practical case in verification where weights are clustered around a constant number of values, the energy game problem can be solved in polynomial time. We also show that the problem is still as hard as in general when the clique-width is bounded or the graph is strongly ergodic, suggesting that restricting graph structures need not help. AU - Chatterjee, Krishnendu AU - Henzinger, Monika H AU - Krinninger, Sebastian AU - Nanongkai, Danupon ID - 10905 SN - 0302-9743 T2 - Algorithms – ESA 2012 TI - Polynomial-time algorithms for energy games with special weight structures VL - 7501 ER - TY - CONF AB - 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. AU - Grebenshchikov, Sergey AU - Gupta, Ashutosh AU - Lopes, Nuno P. AU - Popeea, Corneliu AU - Rybalchenko, Andrey ED - Flanagan, Cormac ED - König, Barbara ID - 10906 SN - 0302-9743 T2 - Tools and Algorithms for the Construction and Analysis of Systems TI - HSF(C): A software verifier based on Horn clauses VL - 7214 ER - TY - CHAP AU - Gupta, Ashutosh ID - 5745 SN - 0302-9743 T2 - Automated Technology for Verification and Analysis TI - Improved Single Pass Algorithms for Resolution Proof Reduction VL - 7561 ER - TY - CONF AB - Many infinite state systems can be seen as well-structured transition systems (WSTS), i.e., systems equipped with a well-quasi-ordering on states that is also a simulation relation. WSTS are an attractive target for formal analysis because there exist generic algorithms that decide interesting verification problems for this class. Among the most popular algorithms are acceleration-based forward analyses for computing the covering set. Termination of these algorithms can only be guaranteed for flattable WSTS. Yet, many WSTS of practical interest are not flattable and the question whether any given WSTS is flattable is itself undecidable. We therefore propose an analysis that computes the covering set and captures the essence of acceleration-based algorithms, but sacrifices precision for guaranteed termination. Our analysis is an abstract interpretation whose abstract domain builds on the ideal completion of the well-quasi-ordered state space, and a widening operator that mimics acceleration and controls the loss of precision of the analysis. We present instances of our framework for various classes of WSTS. Our experience with a prototype implementation indicates that, despite the inherent precision loss, our analysis often computes the precise covering set of the analyzed system. AU - Zufferey, Damien AU - Wies, Thomas AU - Henzinger, Thomas A ID - 3251 TI - Ideal abstractions for well structured transition systems VL - 7148 ER - TY - JOUR AB - Colorectal tumours that are wild type for KRAS are often sensitive to EGFR blockade, but almost always develop resistance within several months of initiating therapy. The mechanisms underlying this acquired resistance to anti-EGFR antibodies are largely unknown. This situation is in marked contrast to that of small-molecule targeted agents, such as inhibitors of ABL, EGFR, BRAF and MEK, in which mutations in the genes encoding the protein targets render the tumours resistant to the effects of the drugs. The simplest hypothesis to account for the development of resistance to EGFR blockade is that rare cells with KRAS mutations pre-exist at low levels in tumours with ostensibly wild-type KRAS genes. Although this hypothesis would seem readily testable, there is no evidence in pre-clinical models to support it, nor is there data from patients. To test this hypothesis, we determined whether mutant KRAS DNA could be detected in the circulation of 28 patients receiving monotherapy with panitumumab, a therapeutic anti-EGFR antibody. We found that 9 out of 24 (38%) patients whose tumours were initially KRAS wild type developed detectable mutations in KRAS in their sera, three of which developed multiple different KRAS mutations. The appearance of these mutations was very consistent, generally occurring between 5 and 6months following treatment. Mathematical modelling indicated that the mutations were present in expanded subclones before the initiation of panitumumab treatment. These results suggest that the emergence of KRAS mutations is a mediator of acquired resistance to EGFR blockade and that these mutations can be detected in a non-invasive manner. They explain why solid tumours develop resistance to targeted therapies in a highly reproducible fashion. AU - Diaz Jr, Luis AU - Williams, Richard AU - Wu, Jian AU - Kinde, Isaac AU - Hecht, Joel AU - Berlin, Jordan AU - Allen, Benjamin AU - Božić, Ivana AU - Reiter, Johannes AU - Nowak, Martin AU - Kinzler, Kenneth AU - Oliner, Kelly AU - Vogelstein, Bert ID - 3157 IS - 7404 JF - Nature TI - The molecular evolution of acquired resistance to targeted EGFR blockade in colorectal cancers VL - 486 ER - TY - JOUR AB - Many scenarios in the living world, where individual organisms compete for winning positions (or resources), have properties of auctions. Here we study the evolution of bids in biological auctions. For each auction, n individuals are drawn at random from a population of size N. Each individual makes a bid which entails a cost. The winner obtains a benefit of a certain value. Costs and benefits are translated into reproductive success (fitness). Therefore, successful bidding strategies spread in the population. We compare two types of auctions. In “biological all-pay auctions”, the costs are the bid for every participating individual. In “biological second price all-pay auctions”, the cost for everyone other than the winner is the bid, but the cost for the winner is the second highest bid. Second price all-pay auctions are generalizations of the “war of attrition” introduced by Maynard Smith. We study evolutionary dynamics in both types of auctions. We calculate pairwise invasion plots and evolutionarily stable distributions over the continuous strategy space. We find that the average bid in second price all-pay auctions is higher than in all-pay auctions, but the average cost for the winner is similar in both auctions. In both cases, the average bid is a declining function of the number of participants, n. The more individuals participate in an auction the smaller is the chance of winning, and thus expensive bids must be avoided. AU - Chatterjee, Krishnendu AU - Reiter, Johannes AU - Nowak, Martin ID - 3260 IS - 1 JF - Theoretical Population Biology TI - Evolutionary dynamics of biological auctions VL - 81 ER - TY - JOUR AB - CA3 pyramidal neurons are important for memory formation and pattern completion in the hippocampal network. It is generally thought that proximal synapses from the mossy fibers activate these neurons most efficiently, whereas distal inputs from the perforant path have a weaker modulatory influence. We used confocally targeted patch-clamp recording from dendrites and axons to map the activation of rat CA3 pyramidal neurons at the subcellular level. Our results reveal two distinct dendritic domains. In the proximal domain, action potentials initiated in the axon backpropagate actively with large amplitude and fast time course. In the distal domain, Na+ channel–mediated dendritic spikes are efficiently initiated by waveforms mimicking synaptic events. CA3 pyramidal neuron dendrites showed a high Na+-to-K+ conductance density ratio, providing ideal conditions for active backpropagation and dendritic spike initiation. Dendritic spikes may enhance the computational power of CA3 pyramidal neurons in the hippocampal network. AU - Kim, Sooyun AU - Guzmán, José AU - Hu, Hua AU - Jonas, Peter M ID - 3258 IS - 4 JF - Nature Neuroscience SN - 1546-1726 TI - Active dendrites support efficient initiation of dendritic spikes in hippocampal CA3 pyramidal neurons VL - 15 ER - TY - THES AB - CA3 pyramidal neurons are important for memory formation and pattern completion in the hippocampal network. These neurons receive multiple excitatory inputs from numerous sources. Therefore, the rules of spatiotemporal integration of multiple synaptic inputs and propagation of action potentials are important to understand how CA3 neurons contribute to higher brain functions at cellular level. By using confocally targeted patch-clamp recording techniques, we investigated the biophysical properties of rat CA3 pyramidal neuron dendrites. We found two distinct dendritic domains critical for action potential initiation and propagation: In the proximal domain, action potentials initiated in the axon backpropagate actively with large amplitude and fast time course. In the distal domain, Na+-channel mediated dendritic spikes are efficiently evoked by local dendritic depolarization or waveforms mimicking synaptic events. These findings can be explained by a high Na+-to-K+ conductance density ratio of CA3 pyramidal neuron dendrites. The results challenge the prevailing view that proximal mossy fiber inputs activate CA3 pyramidal neurons more efficiently than distal perforant inputs by showing that the distal synapses trigger a different form of activity represented by dendritic spikes. The high probability of dendritic spike initiation in the distal area may enhance the computational power of CA3 pyramidal neurons in the hippocampal network. AU - Kim, Sooyun ID - 2964 SN - 2663-337X TI - Active properties of hippocampal CA3 pyramidal neuron dendrites ER - TY - JOUR AB - Visualizing and analyzing shape changes at various scales, ranging from single molecules to whole organisms, are essential for understanding complex morphogenetic processes, such as early embryonic development. Embryo morphogenesis relies on the interplay between different tissues, the properties of which are again determined by the interaction between their constituent cells. Cell interactions, on the other hand, are controlled by various molecules, such as signaling and adhesion molecules, which in order to exert their functions need to be spatiotemporally organized within and between the interacting cells. In this review, we will focus on the role of cell adhesion functioning at different scales to organize cell, tissue and embryo morphogenesis. We will specifically ask how the subcellular distribution of adhesion molecules controls the formation of cell-cell contacts, how cell-cell contacts determine tissue shape, and how tissue interactions regulate embryo morphogenesis. AU - Barone, Vanessa AU - Heisenberg, Carl-Philipp J ID - 3246 IS - 1 JF - Current Opinion in Cell Biology TI - Cell adhesion in embryo morphogenesis VL - 24 ER - TY - JOUR AB - The Arabidopsis thaliana central cell, the companion cell of the egg, undergoes DNA demethylation before fertilization, but the targeting preferences, mechanism, and biological significance of this process remain unclear. Here, we show that active DNA demethylation mediated by the DEMETER DNA glycosylase accounts for all of the demethylation in the central cell and preferentially targets small, AT-rich, and nucleosome-depleted euchromatic transposable elements. The vegetative cell, the companion cell of sperm, also undergoes DEMETER-dependent demethylation of similar sequences, and lack of DEMETER in vegetative cells causes reduced small RNA–directed DNA methylation of transposons in sperm. Our results demonstrate that demethylation in companion cells reinforces transposon methylation in plant gametes and likely contributes to stable silencing of transposable elements across generations. AU - Ibarra, Christian A. AU - Feng, Xiaoqi AU - Schoft, Vera K. AU - Hsieh, Tzung-Fu AU - Uzawa, Rie AU - Rodrigues, Jessica A. AU - Zemach, Assaf AU - Chumak, Nina AU - Machlicova, Adriana AU - Nishimura, Toshiro AU - Rojas, Denisse AU - Fischer, Robert L. AU - Tamaru, Hisashi AU - Zilberman, Daniel ID - 12198 IS - 6100 JF - Science KW - Multidisciplinary SN - 0036-8075 TI - Active DNA demethylation in plant companion cells reinforces transposon methylation in gametes VL - 337 ER - TY - JOUR AB - First we note that the best polynomial approximation to vertical bar x vertical bar on the set, which consists of an interval on the positive half-axis and a point on the negative half-axis, can be given by means of the classical Chebyshev polynomials. Then we explore the cases when a solution of the related problem on two intervals can be given in elementary functions. AU - Pausinger, Florian ID - 6588 IS - 1 JF - Journal of Mathematical Physics, Analysis, Geometry SN - 1812-9471 TI - Elementary solutions of the Bernstein problem on two intervals VL - 8 ER - TY - CONF AB - We introduce the idea of using an explicit triangle mesh to track the air/fluid interface in a smoothed particle hydrodynamics (SPH) simulator. Once an initial surface mesh is created, this mesh is carried forward in time using nearby particle velocities to advect the mesh vertices. The mesh connectivity remains mostly unchanged across time-steps; it is only modified locally for topology change events or for the improvement of triangle quality. In order to ensure that the surface mesh does not diverge from the underlying particle simulation, we periodically project the mesh surface onto an implicit surface defined by the physics simulation. The mesh surface gives us several advantages over previous SPH surface tracking techniques. We demonstrate a new method for surface tension calculations that clearly outperforms the state of the art in SPH surface tension for computer graphics. We also demonstrate a method for tracking detailed surface information (like colors) that is less susceptible to numerical diffusion than competing techniques. Finally, our temporally-coherent surface mesh allows us to simulate high-resolution surface wave dynamics without being limited by the particle resolution of the SPH simulation. AU - Yu, Jihun AU - Wojtan, Christopher J AU - Turk, Greg AU - Yap, Chee ID - 3123 IS - 2 SN - 0167-7055 T2 - Computer Graphics Forum TI - Explicit mesh surfaces for particle based fluids VL - 31 ER - TY - JOUR AB - Bibliothekare haben die Aufgabe, sich mit neuen Medienformen auseinanderzusetzen. AU - Danowski, Patrick ID - 3244 IS - 4 JF - BuB - Forum Bibliothek und Information SN - 1869 -1137 TI - Die Zeit des Abwartens ist vorbei! VL - 64 ER - TY - JOUR AB - Wie wandelt sich das Berufsbild in Wissenschaftlichen Bibliotheken? Patrick Danowski gibt seine Einschätzung ab. AU - Danowski, Patrick ID - 3243 IS - 1 JF - Büchereiperspektiven SN - 1607-7172 TI - Zwischen Technologie und Information VL - 2012 ER - TY - CONF AU - Kroemer, Oliver AU - Lampert, Christoph AU - Peters, Jan ID - 2915 TI - Multi-modal learning for dynamic tactile sensing ER - TY - JOUR AU - Edelsbrunner, Herbert AU - Strelkova, Nataliya ID - 2912 IS - 6 JF - Russian Mathematical Surveys TI - On the configuration space for the shortest networks VL - 67 ER - TY - CONF AB - When searching for characteristic subpatterns in potentially noisy graph data, it appears self-evident that having multiple observations would be better than having just one. However, it turns out that the inconsistencies introduced when different graph instances have different edge sets pose a serious challenge. In this work we address this challenge for the problem of finding maximum weighted cliques. We introduce the concept of most persistent soft-clique. This is subset of vertices, that 1) is almost fully or at least densely connected, 2) occurs in all or almost all graph instances, and 3) has the maximum weight. We present a measure of clique-ness, that essentially counts the number of edge missing to make a subset of vertices into a clique. With this measure, we show that the problem of finding the most persistent soft-clique problem can be cast either as: a) a max-min two person game optimization problem, or b) a min-min soft margin optimization problem. Both formulations lead to the same solution when using a partial Lagrangian method to solve the optimization problems. By experiments on synthetic data and on real social network data, we show that the proposed method is able to reliably find soft cliques in graph data, even if that is distorted by random noise or unreliable observations. AU - Quadrianto, Novi AU - Lampert, Christoph AU - Chen, Chao ID - 3127 T2 - Proceedings of the 29th International Conference on Machine Learning TI - The most persistent soft-clique in a set of sampled graphs ER - TY - JOUR AB - Generalized van der Corput sequences are onedimensional, infinite sequences in the unit interval. They are generated from permutations in integer base b and are the building blocks of the multi-dimensional Halton sequences. Motivated by recent progress of Atanassov on the uniform distribution behavior of Halton sequences, we study, among others, permutations of the form P(i) = ai (mod b) for coprime integers a and b. We show that multipliers a that either divide b - 1 or b + 1 generate van der Corput sequences with weak distribution properties. We give explicit lower bounds for the asymptotic distribution behavior of these sequences and relate them to sequences generated from the identity permutation in smaller bases, which are, due to Faure, the weakest distributed generalized van der Corput sequences. AU - Pausinger, Florian ID - 2904 IS - 3 JF - Journal de Theorie des Nombres des Bordeaux SN - 1246-7405 TI - Weak multipliers for generalized van der Corput sequences VL - 24 ER - TY - JOUR AB - We present an algorithm for simplifying linear cartographic objects and results obtained with a computer program implementing this algorithm. AU - Edelsbrunner, Herbert AU - Musin, Oleg AU - Ukhalov, Alexey AU - Yakimova, Olga AU - Alexeev, Vladislav AU - Bogaevskaya, Victoriya AU - Gorohov, Andrey AU - Preobrazhenskaya, Margarita ID - 2902 IS - 6 JF - Modeling and Analysis of Information Systems TI - Fractal and computational geometry for generalizing cartographic objects VL - 19 ER -