@article{1132, abstract = {The hippocampus is thought to initiate systems-wide mnemonic processes through the reactivation of previously acquired spatial and episodic memory traces, which can recruit the entorhinal cortex as a first stage of memory redistribution to other brain areas. Hippocampal reactivation occurs during sharp wave-ripples, in which synchronous network firing encodes sequences of places.We investigated the coordination of this replay by recording assembly activity simultaneously in the CA1 region of the hippocampus and superficial layers of the medial entorhinal cortex. We found that entorhinal cell assemblies can replay trajectories independently of the hippocampus and sharp wave-ripples. This suggests that the hippocampus is not the sole initiator of spatial and episodic memory trace reactivation. Memory systems involved in these processes may include nonhierarchical, parallel components.}, author = {O'Neill, Joseph and Boccara, Charlotte and Stella, Federico and Schönenberger, Philipp and Csicsvari, Jozsef L}, issn = {0036-8075}, journal = {Science}, number = {6321}, pages = {184 -- 188}, publisher = {American Association for the Advancement of Science}, title = {{Superficial layers of the medial entorhinal cortex replay independently of the hippocampus}}, doi = {10.1126/science.aag2787}, volume = {355}, year = {2017}, } @article{1133, abstract = {It is a common knowledge that an effective interaction of a quantum impurity with an electromagnetic field can be screened by surrounding charge carriers, whether mobile or static. Here we demonstrate that very strong, "anomalous" screening can take place in the presence of a neutral, weakly polarizable environment, due to an exchange of orbital angular momentum between the impurity and the bath. Furthermore, we show that it is possible to generalize all phenomena related to isolated impurities in an external field to the case when a many-body environment is present, by casting the problem in terms of the angulon quasiparticle. As a result, the relevant observables such as the effective Rabi frequency, geometric phase, and impurity spatial alignment are straightforward to evaluate in terms of a single parameter: the angular-momentum-dependent screening factor.}, author = {Yakaboylu, Enderalp and Lemeshko, Mikhail}, issn = {0031-9007}, journal = {Physical Review Letters}, number = {8}, publisher = {American Physical Society}, title = {{Anomalous screening of quantum impurities by a neutral environment}}, doi = {10.1103/PhysRevLett.118.085302}, volume = {118}, year = {2017}, } @inproceedings{1000, abstract = {We study probabilistic models of natural images and extend the autoregressive family of PixelCNN models by incorporating latent variables. Subsequently, we describe two new generative image models that exploit different image transformations as latent variables: a quantized grayscale view of the image or a multi-resolution image pyramid. The proposed models tackle two known shortcomings of existing PixelCNN models: 1) their tendency to focus on low-level image details, while largely ignoring high-level image information, such as object shapes, and 2) their computationally costly procedure for image sampling. We experimentally demonstrate benefits of our LatentPixelCNN models, in particular showing that they produce much more realistically looking image samples than previous state-of-the-art probabilistic models. }, author = {Kolesnikov, Alexander and Lampert, Christoph}, booktitle = {34th International Conference on Machine Learning}, isbn = {978-151085514-4}, location = {Sydney, Australia}, pages = {1905 -- 1914}, publisher = {JMLR}, title = {{PixelCNN models with auxiliary variables for natural image modeling}}, volume = {70}, year = {2017}, } @inproceedings{1003, abstract = {Network games (NGs) are played on directed graphs and are extensively used in network design and analysis. Search problems for NGs include finding special strategy profiles such as a Nash equilibrium and a globally optimal solution. The networks modeled by NGs may be huge. In formal verification, abstraction has proven to be an extremely effective technique for reasoning about systems with big and even infinite state spaces. We describe an abstraction-refinement methodology for reasoning about NGs. Our methodology is based on an abstraction function that maps the state space of an NG to a much smaller state space. We search for a global optimum and a Nash equilibrium by reasoning on an under- and an overapproximation defined on top of this smaller state space. When the approximations are too coarse to find such profiles, we refine the abstraction function. Our experimental results demonstrate the efficiency of the methodology.}, author = {Avni, Guy and Guha, Shibashis and Kupferman, Orna}, issn = {1045-0823}, location = {Melbourne, Australia}, pages = {70 -- 76}, publisher = {AAAI Press}, title = {{An abstraction-refinement methodology for reasoning about network games}}, doi = {10.24963/ijcai.2017/11}, year = {2017}, } @article{1006, abstract = {Background: The phenomenon of immune priming, i.e. enhanced protection following a secondary exposure to a pathogen, has now been demonstrated in a wide range of invertebrate species. Despite accumulating phenotypic evidence, knowledge of its mechanistic underpinnings is currently very limited. Here we used the system of the red flour beetle, Tribolium castaneum and the insect pathogen Bacillus thuringiensis (Bt) to further our molecular understanding of the oral immune priming phenomenon. We addressed how ingestion of bacterial cues (derived from spore supernatants) of an orally pathogenic and non-pathogenic Bt strain affects gene expression upon later challenge exposure, using a whole-transcriptome sequencing approach. Results: Whereas gene expression of individuals primed with the orally non-pathogenic strain showed minor changes to controls, we found that priming with the pathogenic strain induced regulation of a large set of distinct genes, many of which are known immune candidates. Intriguingly, the immune repertoire activated upon priming and subsequent challenge qualitatively differed from the one mounted upon infection with Bt without previous priming. Moreover, a large subset of priming-specific genes showed an inverse regulation compared to their regulation upon challenge only. Conclusions: Our data demonstrate that gene expression upon infection is strongly affected by previous immune priming. We hypothesise that this shift in gene expression indicates activation of a more targeted and efficient response towards a previously encountered pathogen, in anticipation of potential secondary encounter.}, author = {Greenwood, Jenny and Milutinovic, Barbara and Peuß, Robert and Behrens, Sarah and Essar, Daniela and Rosenstiel, Philip and Schulenburg, Hinrich and Kurtz, Joachim}, issn = {1471-2164}, journal = {BMC Genomics}, number = {1}, pages = {329}, publisher = {BioMed Central}, title = {{Oral immune priming with Bacillus thuringiensis induces a shift in the gene expression of Tribolium castaneum larvae}}, doi = {10.1186/s12864-017-3705-7}, volume = {18}, year = {2017}, } @article{1007, abstract = {A nonlinear system possesses an invariance with respect to a set of transformations if its output dynamics remain invariant when transforming the input, and adjusting the initial condition accordingly. Most research has focused on invariances with respect to time-independent pointwise transformations like translational-invariance (u(t) -> u(t) + p, p in R) or scale-invariance (u(t) -> pu(t), p in R>0). In this article, we introduce the concept of s0-invariances with respect to continuous input transformations exponentially growing/decaying over time. We show that s0-invariant systems not only encompass linear time-invariant (LTI) systems with transfer functions having an irreducible zero at s0 in R, but also that the input/output relationship of nonlinear s0-invariant systems possesses properties well known from their linear counterparts. Furthermore, we extend the concept of s0-invariances to second- and higher-order s0-invariances, corresponding to invariances with respect to transformations of the time-derivatives of the input, and encompassing LTI systems with zeros of multiplicity two or higher. Finally, we show that nth-order 0-invariant systems realize – under mild conditions – nth-order nonlinear differential operators: when excited by an input of a characteristic functional form, the system’s output converges to a constant value only depending on the nth (nonlinear) derivative of the input.}, author = {Lang, Moritz and Sontag, Eduardo}, issn = {0005-1098}, journal = {Automatica}, pages = {46 -- 55}, publisher = {International Federation of Automatic Control}, title = {{Zeros of nonlinear systems with input invariances}}, doi = {10.1016/j.automatica.2017.03.030}, volume = {81C}, year = {2017}, } @inproceedings{1009, abstract = {A standard objective in partially-observable Markov decision processes (POMDPs) is to find a policy that maximizes the expected discounted-sum payoff. However, such policies may still permit unlikely but highly undesirable outcomes, which is problematic especially in safety-critical applications. Recently, there has been a surge of interest in POMDPs where the goal is to maximize the probability to ensure that the payoff is at least a given threshold, but these approaches do not consider any optimization beyond satisfying this threshold constraint. In this work we go beyond both the “expectation” and “threshold” approaches and consider a “guaranteed payoff optimization (GPO)” problem for POMDPs, where we are given a threshold t and the objective is to find a policy σ such that a) each possible outcome of σ yields a discounted-sum payoff of at least t, and b) the expected discounted-sum payoff of σ is optimal (or near-optimal) among all policies satisfying a). We present a practical approach to tackle the GPO problem and evaluate it on standard POMDP benchmarks.}, author = {Chatterjee, Krishnendu and Novotny, Petr and Pérez, Guillermo and Raskin, Jean and Zikelic, Djordje}, booktitle = {Proceedings of the 31st AAAI Conference on Artificial Intelligence}, location = {San Francisco, CA, United States}, pages = {3725 -- 3732}, publisher = {AAAI Press}, title = {{Optimizing expectation with guarantees in POMDPs}}, volume = {5}, year = {2017}, } @inproceedings{1011, abstract = {Pushdown systems (PDSs) and recursive state machines (RSMs), which are linearly equivalent, are standard models for interprocedural analysis. Yet RSMs are more convenient as they (a) explicitly model function calls and returns, and (b) specify many natural parameters for algorithmic analysis, e.g., the number of entries and exits. We consider a general framework where RSM transitions are labeled from a semiring and path properties are algebraic with semiring operations, which can model, e.g., interprocedural reachability and dataflow analysis problems. Our main contributions are new algorithms for several fundamental problems. As compared to a direct translation of RSMs to PDSs and the best-known existing bounds of PDSs, our analysis algorithm improves the complexity for finite-height semirings (that subsumes reachability and standard dataflow properties). We further consider the problem of extracting distance values from the representation structures computed by our algorithm, and give efficient algorithms that distinguish the complexity of a one-time preprocessing from the complexity of each individual query. Another advantage of our algorithm is that our improvements carry over to the concurrent setting, where we improve the bestknown complexity for the context-bounded analysis of concurrent RSMs. Finally, we provide a prototype implementation that gives a significant speed-up on several benchmarks from the SLAM/SDV project.}, author = {Chatterjee, Krishnendu and Kragl, Bernhard and Mishra, Samarth and Pavlogiannis, Andreas}, editor = {Yang, Hongseok}, issn = {0302-9743}, location = {Uppsala, Sweden}, pages = {287 -- 313}, publisher = {Springer}, title = {{Faster algorithms for weighted recursive state machines}}, doi = {10.1007/978-3-662-54434-1_11}, volume = {10201}, year = {2017}, } @article{1013, abstract = {From microwave ovens to satellite television to the GPS and data services on our mobile phones, microwave technology is everywhere today. But one technology that has so far failed to prove its worth in this wavelength regime is quantum communication that uses the states of single photons as information carriers. This is because single microwave photons, as opposed to classical microwave signals, are extremely vulnerable to noise from thermal excitations in the channels through which they travel. Two new independent studies, one by Ze-Liang Xiang at Technische Universität Wien (Vienna), Austria, and colleagues [1] and another by Benoît Vermersch at the University of Innsbruck, also in Austria, and colleagues [2] now describe a theoretical protocol for microwave quantum communication that is resilient to thermal and other types of noise. Their approach could become a powerful technique to establish fast links between superconducting data processors in a future all-microwave quantum network.}, author = {Fink, Johannes M}, journal = {Physics}, number = {32}, publisher = {American Physical Society}, title = {{Viewpoint: Microwave quantum states beat the heat}}, doi = {10.1103/Physics.10.32}, volume = {10}, year = {2017}, } @article{1015, abstract = {Vortices are commonly observed in the context of classical hydrodynamics: from whirlpools after stirring the coffee in a cup to a violent atmospheric phenomenon such as a tornado, all classical vortices are characterized by an arbitrary circulation value of the local velocity field. On the other hand the appearance of vortices with quantized circulation represents one of the fundamental signatures of macroscopic quantum phenomena. In two-dimensional superfluids quantized vortices play a key role in determining finite-temperature properties, as the superfluid phase and the normal state are separated by a vortex unbinding transition, the Berezinskii-Kosterlitz-Thouless transition. Very recent experiments with two-dimensional superfluid fermions motivate the present work: we present theoretical results based on the renormalization group showing that the universal jump of the superfluid density and the critical temperature crucially depend on the interaction strength, providing a strong benchmark for forthcoming investigations.}, author = {Bighin, Giacomo and Salasnich, Luca}, issn = {2045-2322}, journal = {Scientific Reports}, publisher = {Nature Publishing Group}, title = {{Vortices and antivortices in two-dimensional ultracold Fermi gases}}, doi = {10.1038/srep45702}, volume = {7}, year = {2017}, } @article{1017, abstract = {The development of the vertebrate central nervous system is reliant on a complex cascade of biological processes that include mitotic division, relocation of migrating neurons, and the extension of dendritic and axonal processes. Each of these cellular events requires the diverse functional repertoire of the microtubule cytoskeleton for the generation of forces, assembly of macromolecular complexes and transport of molecules and organelles. The tubulins are a multi-gene family that encode for the constituents of microtubules, and have been implicated in a spectrum of neurological disorders. Evidence is building that different tubulins tune the functional properties of the microtubule cytoskeleton dependent on the cell type, developmental profile and subcellular localisation. Here we review of the origins of the functional specification of the tubulin gene family in the developing brain at a transcriptional, translational, and post-transcriptional level. We remind the reader that tubulins are not just loading controls for your average Western blot.}, author = {Breuss, Martin and Leca, Ines and Gstrein, Thomas and Hansen, Andi H and Keays, David}, issn = {1044-7431}, journal = {Molecular and Cellular Neuroscience}, pages = {58 -- 67}, publisher = {Academic Press}, title = {{Tubulins and brain development: The origins of functional specification}}, doi = {10.1016/j.mcn.2017.03.002}, volume = {84}, year = {2017}, } @article{1018, abstract = {In plants, the multistep phosphorelay (MSP) pathway mediates a range of regulatory processes, including those activated by cytokinins. The crosstalk between cytokinin response and light is known for a long time. However, the molecular mechanism underlying the interactionbetween light and cytokinin signaling remains elusive. In the screen for upstream regulators we identified a LONG PALE HYPOCOTYL (LPH) gene whose activity is indispensable for spatiotemporally correct expression of CYTOKININ INDEPENDENT-1 (CKI1), encoding the constitutively active sensor histidine kinase that activates MSP signaling. lph is a new allele of HEME OXYGENASE 1 (HY1) which encodes the key protein in the biosynthesis of phytochromobilin, a cofactor of photoconvertiblephytochromes. Our analysis confirmed the light-dependent regulation oftheCKI1 expression pattern. We show that CKI1 expression is under the control of phytochrome A (phyA), functioning as a dual (both positive and negative) regulator of CKI1 expression, presumably via the phyA-regulated transcription factors PHYTOCHROME INTERACTING FACTOR 3 (PIF3) and CIRCADIAN CLOCK ASSOCIATED 1 (CCA1). Changes in CKI1 expression observed in lph/hy1-7 and phy mutants correlatewithmisregulation of MSP signaling, changedcytokinin sensitivity and developmental aberrations,previously shown to be associated with cytokinin and/or CKI1 action. Besides that, we demonstrate novel role of phyA-dependent CKI1 expression in the hypocotyl elongation and hook development during skotomorphogenesis. Based on these results, we propose that the light-dependent regulation of CKI1 provides a plausible mechanistic link underlying the well-known interaction between light- and cytokinin-controlled plant development.}, author = {Dobisova, Tereza and Hrdinova, Vendula and Cuesta, Candela and Michlickova, Sarka and Urbankova, Ivana and Hejatkova, Romana and Zadnikova, Petra and Pernisová, Markéta and Benková, Eva and Hejátko, Jan}, journal = {Plant Physiology}, number = {1}, pages = {387 -- 404}, publisher = {American Society of Plant Biologists}, title = {{Light regulated expression of sensor histidine kinase CKI1 controls cytokinin related development}}, doi = {10.1104/pp.16.01964}, volume = {174}, year = {2017}, } @article{1019, abstract = {As a consequence of its difference in copy number between males and females, the X chromosome is subject to unique evolutionary forces and gene regulatory mechanisms. Previous studies of Drosophila melanogaster have shown that the expression of X-linked, testis-specific reporter genes is suppressed in the male germline. However, it is not known whether this phenomenon is restricted to testis-expressed genes or if it is a more general property of genes with tissue-specific expression, which are also underrepresented on the X chromosome. To test this, we compared the expression of three tissue-specific reporter genes (ovary, accessory gland and Malpighian tubule) inserted at various autosomal and X-chromosomal locations. In contrast to testis-specific reporter genes, we found no reduction of X-linked expression in any of the other tissues. In accessory gland and Malpighian tubule, we detected higher expression of the X-linked reporter genes, which suggests that they are at least partially dosage compensated. We found no difference in the tissue-specificity of X-linked and autosomal reporter genes. These findings indicate that, in general, the X chromosome is not a detrimental environment for tissue-specific gene expression and that the suppression of X-linked expression is limited to the male germline.}, author = {Argyridou, Eliza and Huylmans, Ann K and Königer, Annabella and Parsch, John}, issn = {0018-067X}, journal = {Heredity}, number = {1}, pages = {27 -- 34}, publisher = {Nature Publishing Group}, title = {{X-linkage is not a general inhibitor of tissue-specific gene expression in Drosophila melanogaster}}, doi = {10.1038/hdy.2017.12}, volume = {119}, year = {2017}, } @article{1020, abstract = {Cellulose is the most abundant biopolymer on Earth. Cellulose fibers, such as the one extracted form cotton or woodpulp, have been used by humankind for hundreds of years to make textiles and paper. Here we show how, by engineering light-matter interaction, we can optimize light scattering using exclusively cellulose nanocrystals. The produced material is sustainable, biocompatible, and when compared to ordinary microfiber-based paper, it shows enhanced scattering strength (×4), yielding a transport mean free path as low as 3.5 μm in the visible light range. The experimental results are in a good agreement with the theoretical predictions obtained with a diffusive model for light propagation.}, author = {Caixeiro, Soraya and Peruzzo, Matilda and Onelli, Olimpia and Vignolini, Silvia and Sapienza, Riccardo}, issn = {1944-8244}, journal = {ACS Applied Materials and Interfaces}, number = {9}, pages = {7885 -- 7890}, publisher = {American Chemical Society}, title = {{Disordered cellulose based nanostructures for enhanced light scattering}}, doi = {10.1021/acsami.6b15986}, volume = {9}, year = {2017}, } @article{1021, abstract = {Most flows in nature and engineering are turbulent because of their large velocities and spatial scales. Laboratory experiments on rotating quasi-Keplerian flows, for which the angular velocity decreases radially but the angular momentum increases, are however laminar at Reynolds numbers exceeding one million. This is in apparent contradiction to direct numerical simulations showing that in these experiments turbulence transition is triggered by the axial boundaries. We here show numerically that as the Reynolds number increases, turbulence becomes progressively confined to the boundary layers and the flow in the bulk fully relaminarizes. Our findings support that turbulence is unlikely to occur in isothermal constant-density quasi-Keplerian flows.}, author = {Lopez Alonso, Jose M and Avila, Marc}, issn = {0022-1120}, journal = {Journal of Fluid Mechanics}, pages = {21 -- 34}, publisher = {Cambridge University Press}, title = {{Boundary layer turbulence in experiments on quasi Keplerian flows}}, doi = {10.1017/jfm.2017.109}, volume = {817}, year = {2017}, } @article{1022, abstract = {We introduce a multiscale topological description of the Megaparsec web-like cosmic matter distribution. Betti numbers and topological persistence offer a powerful means of describing the rich connectivity structure of the cosmic web and of its multiscale arrangement of matter and galaxies. Emanating from algebraic topology and Morse theory, Betti numbers and persistence diagrams represent an extension and deepening of the cosmologically familiar topological genus measure and the related geometric Minkowski functionals. In addition to a description of the mathematical background, this study presents the computational procedure for computing Betti numbers and persistence diagrams for density field filtrations. The field may be computed starting from a discrete spatial distribution of galaxies or simulation particles. The main emphasis of this study concerns an extensive and systematic exploration of the imprint of different web-like morphologies and different levels of multiscale clustering in the corresponding computed Betti numbers and persistence diagrams. To this end, we use Voronoi clustering models as templates for a rich variety of web-like configurations and the fractal-like Soneira-Peebles models exemplify a range of multiscale configurations. We have identified the clear imprint of cluster nodes, filaments, walls, and voids in persistence diagrams, along with that of the nested hierarchy of structures in multiscale point distributions. We conclude by outlining the potential of persistent topology for understanding the connectivity structure of the cosmic web, in large simulations of cosmic structure formation and in the challenging context of the observed galaxy distribution in large galaxy surveys.}, author = {Pranav, Pratyush and Edelsbrunner, Herbert and Van De Weygaert, Rien and Vegter, Gert and Kerber, Michael and Jones, Bernard and Wintraecken, Mathijs}, issn = {0035-8711}, journal = {Monthly Notices of the Royal Astronomical Society}, number = {4}, pages = {4281 -- 4310}, publisher = {Oxford University Press}, title = {{The topology of the cosmic web in terms of persistent Betti numbers}}, doi = {10.1093/mnras/stw2862}, volume = {465}, year = {2017}, } @article{1023, abstract = {We consider products of independent square non-Hermitian random matrices. More precisely, let X1,…, Xn be independent N × N random matrices with independent entries (real or complex with independent real and imaginary parts) with zero mean and variance 1/N. Soshnikov-O’Rourke [19] and Götze-Tikhomirov [15] showed that the empirical spectral distribution of the product of n random matrices with iid entries converges to (equation found). We prove that if the entries of the matrices X1,…, Xn are independent (but not necessarily identically distributed) and satisfy uniform subexponential decay condition, then in the bulk the convergence of the ESD of X1,…, Xn to (0.1) holds up to the scale N–1/2+ε.}, author = {Nemish, Yuriy}, issn = {1083-6489}, journal = {Electronic Journal of Probability}, publisher = {Institute of Mathematical Statistics}, title = {{Local law for the product of independent non-Hermitian random matrices with independent entries}}, doi = {10.1214/17-EJP38}, volume = {22}, year = {2017}, } @article{1025, abstract = {Many organ surfaces are covered by a protective epithelial-cell layer. It emerges that such layers are maintained by cell stretching that triggers cell division mediated by the force-sensitive ion-channel protein Piezo1. See Letter p.118}, author = {Heisenberg, Carl-Philipp J}, issn = {0028-0836}, journal = {Nature}, number = {7643}, pages = {43 -- 44}, publisher = {Nature Publishing Group}, title = {{Cell biology: Stretched divisions}}, doi = {10.1038/nature21502}, volume = {543}, year = {2017}, } @article{10416, abstract = {A fundamental algorithmic problem at the heart of static analysis is Dyck reachability. The input is a graph where the edges are labeled with different types of opening and closing parentheses, and the reachability information is computed via paths whose parentheses are properly matched. We present new results for Dyck reachability problems with applications to alias analysis and data-dependence analysis. Our main contributions, that include improved upper bounds as well as lower bounds that establish optimality guarantees, are as follows: First, we consider Dyck reachability on bidirected graphs, which is the standard way of performing field-sensitive points-to analysis. Given a bidirected graph with n nodes and m edges, we present: (i) an algorithm with worst-case running time O(m + n · α(n)), where α(n) is the inverse Ackermann function, improving the previously known O(n2) time bound; (ii) a matching lower bound that shows that our algorithm is optimal wrt to worst-case complexity; and (iii) an optimal average-case upper bound of O(m) time, improving the previously known O(m · logn) bound. Second, we consider the problem of context-sensitive data-dependence analysis, where the task is to obtain analysis summaries of library code in the presence of callbacks. Our algorithm preprocesses libraries in almost linear time, after which the contribution of the library in the complexity of the client analysis is only linear, and only wrt the number of call sites. Third, we prove that combinatorial algorithms for Dyck reachability on general graphs with truly sub-cubic bounds cannot be obtained without obtaining sub-cubic combinatorial algorithms for Boolean Matrix Multiplication, which is a long-standing open problem. Thus we establish that the existing combinatorial algorithms for Dyck reachability are (conditionally) optimal for general graphs. We also show that the same hardness holds for graphs of constant treewidth. Finally, we provide a prototype implementation of our algorithms for both alias analysis and data-dependence analysis. Our experimental evaluation demonstrates that the new algorithms significantly outperform all existing methods on the two problems, over real-world benchmarks.}, author = {Chatterjee, Krishnendu and Choudhary, Bhavya and Pavlogiannis, Andreas}, issn = {2475-1421}, journal = {Proceedings of the ACM on Programming Languages}, location = {Los Angeles, CA, United States}, number = {POPL}, publisher = {Association for Computing Machinery}, title = {{Optimal Dyck reachability for data-dependence and Alias analysis}}, doi = {10.1145/3158118}, volume = {2}, year = {2017}, } @article{10418, abstract = {We present a new proof rule for proving almost-sure termination of probabilistic programs, including those that contain demonic non-determinism. An important question for a probabilistic program is whether the probability mass of all its diverging runs is zero, that is that it terminates "almost surely". Proving that can be hard, and this paper presents a new method for doing so. It applies directly to the program's source code, even if the program contains demonic choice. Like others, we use variant functions (a.k.a. "super-martingales") that are real-valued and decrease randomly on each loop iteration; but our key innovation is that the amount as well as the probability of the decrease are parametric. We prove the soundness of the new rule, indicate where its applicability goes beyond existing rules, and explain its connection to classical results on denumerable (non-demonic) Markov chains.}, author = {Mciver, Annabelle and Morgan, Carroll and Kaminski, Benjamin Lucien and Katoen, Joost P}, issn = {2475-1421}, journal = {Proceedings of the ACM on Programming Languages}, location = {Los Angeles, CA, United States}, number = {POPL}, publisher = {Association for Computing Machinery}, title = {{A new proof rule for almost-sure termination}}, doi = {10.1145/3158121}, volume = {2}, year = {2017}, }