@article{9603,
  abstract     = {Mosaic analysis with double markers (MADM) offers one approach to visualize and concomitantly manipulate genetically defined cells in mice with single-cell resolution. MADM applications include the analysis of lineage, single-cell morphology and physiology, genomic imprinting phenotypes, and dissection of cell-autonomous gene functions in vivo in health and disease. Yet, MADM can only be applied to <25% of all mouse genes on select chromosomes to date. To overcome this limitation, we generate transgenic mice with knocked-in MADM cassettes near the centromeres of all 19 autosomes and validate their use across organs. With this resource, >96% of the entire mouse genome can now be subjected to single-cell genetic mosaic analysis. Beyond a proof of principle, we apply our MADM library to systematically trace sister chromatid segregation in distinct mitotic cell lineages. We find striking chromosome-specific biases in segregation patterns, reflecting a putative mechanism for the asymmetric segregation of genetic determinants in somatic stem cell division.},
  author       = {Contreras, Ximena and Amberg, Nicole and Davaatseren, Amarbayasgalan and Hansen, Andi H and Sonntag, Johanna and Andersen, Lill and Bernthaler, Tina and Streicher, Carmen and Heger, Anna-Magdalena and Johnson, Randy L. and Schwarz, Lindsay A. and Luo, Liqun and Rülicke, Thomas and Hippenmeyer, Simon},
  issn         = {22111247},
  journal      = {Cell Reports},
  number       = {12},
  publisher    = {Cell Press},
  title        = {{A genome-wide library of MADM mice for single-cell genetic mosaic analysis}},
  doi          = {10.1016/j.celrep.2021.109274},
  volume       = {35},
  year         = {2021},
}

@inproceedings{9604,
  abstract     = {Generalizing Lee’s inductive argument for counting the cells of higher order Voronoi tessellations in ℝ² to ℝ³, we get precise relations in terms of Morse theoretic quantities for piecewise constant functions on planar arrangements. Specifically, we prove that for a generic set of n ≥ 5 points in ℝ³, the number of regions in the order-k Voronoi tessellation is N_{k-1} - binom(k,2)n + n, for 1 ≤ k ≤ n-1, in which N_{k-1} is the sum of Euler characteristics of these function’s first k-1 sublevel sets. We get similar expressions for the vertices, edges, and polygons of the order-k Voronoi tessellation.},
  author       = {Biswas, Ranita and Cultrera di Montesano, Sebastiano and Edelsbrunner, Herbert and Saghafian, Morteza},
  booktitle    = {Leibniz International Proceedings in Informatics},
  isbn         = {9783959771849},
  issn         = {18688969},
  location     = {Online},
  publisher    = {Schloss Dagstuhl - Leibniz-Zentrum für Informatik},
  title        = {{Counting cells of order-k voronoi tessellations in ℝ<sup>3</sup> with morse theory}},
  doi          = {10.4230/LIPIcs.SoCG.2021.16},
  volume       = {189},
  year         = {2021},
}

@inproceedings{9605,
  abstract     = {Given a finite set A ⊂ ℝ^d, let Cov_{r,k} denote the set of all points within distance r to at least k points of A. Allowing r and k to vary, we obtain a 2-parameter family of spaces that grow larger when r increases or k decreases, called the multicover bifiltration. Motivated by the problem of computing the homology of this bifiltration, we introduce two closely related combinatorial bifiltrations, one polyhedral and the other simplicial, which are both topologically equivalent to the multicover bifiltration and far smaller than a Čech-based model considered in prior work of Sheehy. Our polyhedral construction is a bifiltration of the rhomboid tiling of Edelsbrunner and Osang, and can be efficiently computed using a variant of an algorithm given by these authors as well. Using an implementation for dimension 2 and 3, we provide experimental results. Our simplicial construction is useful for understanding the polyhedral construction and proving its correctness. },
  author       = {Corbet, René and Kerber, Michael and Lesnick, Michael and Osang, Georg F},
  booktitle    = {Leibniz International Proceedings in Informatics},
  isbn         = {9783959771849},
  issn         = {18688969},
  location     = {Online},
  publisher    = {Schloss Dagstuhl - Leibniz-Zentrum für Informatik},
  title        = {{Computing the multicover bifiltration}},
  doi          = {10.4230/LIPIcs.SoCG.2021.27},
  volume       = {189},
  year         = {2021},
}

@article{9606,
  abstract     = {Sound propagation is a macroscopic manifestation of the interplay between the equilibrium thermodynamics and the dynamical transport properties of fluids. Here, for a two-dimensional system of ultracold fermions, we calculate the first and second sound velocities across the whole BCS-BEC crossover, and we analyze the system response to an external perturbation. In the low-temperature regime we reproduce the recent measurements [Phys. Rev. Lett. 124, 240403 (2020)] of the first sound velocity, which, due to the decoupling of density and entropy fluctuations, is the sole mode excited by a density probe. Conversely, a heat perturbation excites only the second sound, which, being sensitive to the superfluid depletion, vanishes in the deep BCS regime and jumps discontinuously to zero at the Berezinskii-Kosterlitz-Thouless superfluid transition. A mixing between the modes occurs only in the finite-temperature BEC regime, where our theory converges to the purely bosonic results.},
  author       = {Tononi, A. and Cappellaro, Alberto and Bighin, Giacomo and Salasnich, L.},
  issn         = {24699934},
  journal      = {Physical Review A},
  number       = {6},
  publisher    = {American Physical Society},
  title        = {{Propagation of first and second sound in a two-dimensional Fermi superfluid}},
  doi          = {10.1103/PhysRevA.103.L061303},
  volume       = {103},
  year         = {2021},
}

@article{9607,
  abstract     = {While high risk of failure is an inherent part of developing innovative therapies, it can be reduced by adherence to evidence-based rigorous research practices. Numerous analyses conducted to date have clearly identified measures that need to be taken to improve research rigor. Supported through the European Union's Innovative Medicines Initiative, the EQIPD consortium has developed a novel preclinical research quality system that can be applied in both public and private sectors and is free for anyone to use. The EQIPD Quality System was designed to be suited to boost innovation by ensuring the generation of robust and reliable preclinical data while being lean, effective and not becoming a burden that could negatively impact the freedom to explore scientific questions. EQIPD defines research quality as the extent to which research data are fit for their intended use. Fitness, in this context, is defined by the stakeholders, who are the scientists directly involved in the research, but also their funders, sponsors, publishers, research tool manufacturers and collaboration partners such as peers in a multi-site research project. The essence of the EQIPD Quality System is the set of 18 core requirements that can be addressed flexibly, according to user-specific needs and following a user-defined trajectory. The EQIPD Quality System proposes guidance on expectations for quality-related measures, defines criteria for adequate processes (i.e., performance standards) and provides examples of how such measures can be developed and implemented. However, it does not prescribe any pre-determined solutions. EQIPD has also developed tools (for optional use) to support users in implementing the system and assessment services for those research units that successfully implement the quality system and seek formal accreditation. Building upon the feedback from users and continuous improvement, a sustainable EQIPD Quality System will ultimately serve the entire community of scientists conducting non-regulated preclinical research, by helping them generate reliable data that are fit for their intended use.},
  author       = {Bespalov, Anton and Bernard, René and Gilis, Anja and Gerlach, Björn and Guillén, Javier and Castagné, Vincent and Lefevre, Isabel A. and Ducrey, Fiona and Monk, Lee and Bongiovanni, Sandrine and Altevogt, Bruce and Arroyo-Araujo, María and Bikovski, Lior and De Bruin, Natasja and Castaños-Vélez, Esmeralda and Dityatev, Alexander and Emmerich, Christoph H. and Fares, Raafat and Ferland-Beckham, Chantelle and Froger-Colléaux, Christelle and Gailus-Durner, Valerie and Hölter, Sabine M. and Hofmann, Martine Cj and Kabitzke, Patricia and Kas, Martien Jh and Kurreck, Claudia and Moser, Paul and Pietraszek, Malgorzata and Popik, Piotr and Potschka, Heidrun and Prado Montes De Oca, Ernesto and Restivo, Leonardo and Riedel, Gernot and Ritskes-Hoitinga, Merel and Samardzic, Janko and Schunn, Michael and Stöger, Claudia and Voikar, Vootele and Vollert, Jan and Wever, Kimberley E. and Wuyts, Kathleen and Macleod, Malcolm R. and Dirnagl, Ulrich and Steckler, Thomas},
  issn         = {2050084X},
  journal      = {eLife},
  publisher    = {eLife Sciences Publications},
  title        = {{Introduction to the EQIPD quality system}},
  doi          = {10.7554/eLife.63294},
  volume       = {10},
  year         = {2021},
}

@article{9618,
  abstract     = {The control of nonequilibrium quantum dynamics in many-body systems is challenging because interactions typically lead to thermalization and a chaotic spreading throughout Hilbert space. We investigate nonequilibrium dynamics after rapid quenches in a many-body system composed of 3 to 200 strongly interacting qubits in one and two spatial dimensions. Using a programmable quantum simulator based on Rydberg atom arrays, we show that coherent revivals associated with so-called quantum many-body scars can be stabilized by periodic driving, which generates a robust subharmonic response akin to discrete time-crystalline order. We map Hilbert space dynamics, geometry dependence, phase diagrams, and system-size dependence of this emergent phenomenon, demonstrating new ways to steer complex dynamics in many-body systems and enabling potential applications in quantum information science.},
  author       = {Bluvstein, D. and Omran, A. and Levine, H. and Keesling, A. and Semeghini, G. and Ebadi, S. and Wang, T. T. and Michailidis, Alexios and Maskara, N. and Ho, W. W. and Choi, S. and Serbyn, Maksym and Greiner, M. and Vuletić, V. and Lukin, M. D.},
  issn         = {1095-9203},
  journal      = {Science},
  keywords     = {Multidisciplinary},
  number       = {6536},
  pages        = {1355--1359},
  publisher    = {AAAS},
  title        = {{Controlling quantum many-body dynamics in driven Rydberg atom arrays}},
  doi          = {10.1126/science.abg2530},
  volume       = {371},
  year         = {2021},
}

@inproceedings{9620,
  abstract     = {In this note, we introduce a distributed twist on the classic coupon collector problem: a set of m collectors wish to each obtain a set of n coupons; for this, they can each sample coupons uniformly at random, but can also meet in pairwise interactions, during which they can exchange coupons. By doing so, they hope to reduce the number of coupons that must be sampled by each collector in order to obtain a full set. This extension is natural when considering real-world manifestations of the coupon collector phenomenon, and has been remarked upon and studied empirically (Hayes and Hannigan 2006, Ahmad et al. 2014, Delmarcelle 2019).

We provide the first theoretical analysis for such a scenario. We find that “coupon collecting with friends” can indeed significantly reduce the number of coupons each collector must sample, and raises interesting connections to the more traditional variants of the problem. While our analysis is in most cases asymptotically tight, there are several open questions raised, regarding finer-grained analysis of both “coupon collecting with friends,” and of a long-studied variant of the original problem in which a collector requires multiple full sets of coupons.},
  author       = {Alistarh, Dan-Adrian and Davies, Peter},
  booktitle    = {Structural Information and Communication Complexity},
  isbn         = {9783030795269},
  issn         = {1611-3349},
  location     = {Wrocław, Poland},
  pages        = {3--12},
  publisher    = {Springer Nature},
  title        = {{Collecting coupons is faster with friends}},
  doi          = {10.1007/978-3-030-79527-6_1},
  volume       = {12810},
  year         = {2021},
}

@phdthesis{9623,
  abstract     = {Cytoplasmic reorganizations are essential for morphogenesis. In large cells like oocytes, these reorganizations become crucial in patterning the oocyte for later stages of embryonic development. Ascidians oocytes reorganize their cytoplasm (ooplasm) in a spectacular manner. Ooplasmic reorganization is initiated at fertilization with the contraction of the actomyosin cortex along the animal-vegetal axis of the oocyte, driving the accumulation of cortical endoplasmic reticulum (cER), maternal mRNAs associated to it and a mitochondria-rich subcortical layer – the myoplasm – in a region of the vegetal pole termed contraction pole (CP). Here we have used the species Phallusia mammillata to investigate the changes in cell shape that accompany these reorganizations and the mechanochemical mechanisms underlining CP formation.
We report that the length of the animal-vegetal (AV) axis oscillates upon fertilization: it first undergoes a cycle of fast elongation-lengthening followed by a slow expansion of mainly the vegetal pole (VP) of the cell. We show that the fast oscillation corresponds to a dynamic polarization of the actin cortex as a result of a fertilization-induced increase in cortical tension in the oocyte that triggers a rupture of the cortex at the animal pole and the establishment of vegetal-directed cortical flows. These flows are responsible for the vegetal accumulation of actin causing the VP to flatten. 
We find that the slow expansion of the VP, leading to CP formation, correlates with a relaxation of the vegetal cortex and that the myoplasm plays a role in the expansion. We show that the myoplasm is a solid-like layer that buckles under compression forces arising from the contracting actin cortex at the VP. Straightening of the myoplasm when actin flows stops, facilitates the expansion of the VP and the CP. Altogether, our results present a previously unrecognized role for the myoplasm in ascidian ooplasmic segregation. 
},
  author       = {Caballero Mancebo, Silvia},
  isbn         = {978-3-99078-012-1},
  issn         = {2663-337X},
  pages        = {111},
  publisher    = {Institute of Science and Technology Austria},
  title        = {{Fertilization-induced deformations are controlled by the actin cortex and a mitochondria-rich subcortical layer in ascidian oocytes}},
  doi          = {10.15479/at:ista:9623},
  year         = {2021},
}

@article{9626,
  abstract     = {SnSe, a wide-bandgap semiconductor, has attracted significant attention from the thermoelectric (TE) community due to its outstanding TE performance deriving from the ultralow thermal conductivity and advantageous electronic structures. Here, we promoted the TE performance of n-type SnSe polycrystals through bandgap engineering and vacancy compensation. We found that PbTe can significantly reduce the wide bandgap of SnSe to reduce the impurity transition energy, largely enhancing the carrier concentration. Also, PbTe-induced crystal symmetry promotion increases the carrier mobility, preserving large Seebeck coefficient. Consequently, a maximum ZT of ∼1.4 at 793 K is obtained in Br doped SnSe–13%PbTe. Furthermore, we found that extra Sn in n-type SnSe can compensate for the intrinsic Sn vacancies and form electron donor-like metallic Sn nanophases. The Sn nanophases near the grain boundary could also reduce the intergrain energy barrier which largely enhances the carrier mobility. As a result, a maximum ZT value of ∼1.7 at 793 K and an average ZT (ZTave) of ∼0.58 in 300–793 K are achieved in Br doped Sn1.08Se–13%PbTe. Our findings provide a novel strategy to promote the TE performance in wide-bandgap semiconductors.},
  author       = {Su, Lizhong and Hong, Tao and Wang, Dongyang and Wang, Sining and Qin, Bingchao and Zhang, Mengmeng and Gao, Xiang and Chang, Cheng and Zhao, Li Dong},
  issn         = {2542-5293},
  journal      = {Materials Today Physics},
  publisher    = {Elsevier},
  title        = {{Realizing high doping efficiency and thermoelectric performance in n-type SnSe polycrystals via bandgap engineering and vacancy compensation}},
  doi          = {10.1016/j.mtphys.2021.100452},
  volume       = {20},
  year         = {2021},
}

@article{9627,
  abstract     = {We compute the deficiency spaces of operators of the form 𝐻𝐴⊗̂ 𝐼+𝐼⊗̂ 𝐻𝐵, for symmetric 𝐻𝐴 and self-adjoint 𝐻𝐵. This enables us to construct self-adjoint extensions (if they exist) by means of von Neumann's theory. The structure of the deficiency spaces for this case was asserted already in Ibort et al. [Boundary dynamics driven entanglement, J. Phys. A: Math. Theor. 47(38) (2014) 385301], but only proven under the restriction of 𝐻𝐵 having discrete, non-degenerate spectrum.},
  author       = {Lenz, Daniel and Weinmann, Timon and Wirth, Melchior},
  issn         = {1464-3839},
  journal      = {Proceedings of the Edinburgh Mathematical Society},
  number       = {3},
  pages        = {443--447},
  publisher    = {Cambridge University Press},
  title        = {{Self-adjoint extensions of bipartite Hamiltonians}},
  doi          = {10.1017/S0013091521000080},
  volume       = {64},
  year         = {2021},
}

@article{9629,
  abstract     = {Intestinal organoids derived from single cells undergo complex crypt–villus patterning and morphogenesis. However, the nature and coordination of the underlying forces remains poorly characterized. Here, using light-sheet microscopy and large-scale imaging quantification, we demonstrate that crypt formation coincides with a stark reduction in lumen volume. We develop a 3D biophysical model to computationally screen different mechanical scenarios of crypt morphogenesis. Combining this with live-imaging data and multiple mechanical perturbations, we show that actomyosin-driven crypt apical contraction and villus basal tension work synergistically with lumen volume reduction to drive crypt morphogenesis, and demonstrate the existence of a critical point in differential tensions above which crypt morphology becomes robust to volume changes. Finally, we identified a sodium/glucose cotransporter that is specific to differentiated enterocytes that modulates lumen volume reduction through cell swelling in the villus region. Together, our study uncovers the cellular basis of how cell fate modulates osmotic and actomyosin forces to coordinate robust morphogenesis.},
  author       = {Yang, Qiutan and Xue, Shi-lei and Chan, Chii Jou and Rempfler, Markus and Vischi, Dario and Maurer-Gutierrez, Francisca and Hiiragi, Takashi and Hannezo, Edouard B and Liberali, Prisca},
  issn         = {1476-4679},
  journal      = {Nature Cell Biology},
  pages        = {733–744},
  publisher    = {Springer Nature},
  title        = {{Cell fate coordinates mechano-osmotic forces in intestinal crypt formation}},
  doi          = {10.1038/s41556-021-00700-2},
  volume       = {23},
  year         = {2021},
}

@misc{9636,
  author       = {Higginbotham, Andrew P},
  publisher    = {Institute of Science and Technology Austria},
  title        = {{Data for "Breakdown of induced p ± ip pairing in a superconductor-semiconductor hybrid"}},
  year         = {2021},
}

@article{9640,
  abstract     = {Selection and random drift determine the probability that novel mutations fixate in a population. Population structure is known to affect the dynamics of the evolutionary process. Amplifiers of selection are population structures that increase the fixation probability of beneficial mutants compared to well-mixed populations. Over the past 15 years, extensive research has produced remarkable structures called strong amplifiers which guarantee that every beneficial mutation fixates with high probability. But strong amplification has come at the cost of considerably delaying the fixation event, which can slow down the overall rate of evolution. However, the precise relationship between fixation probability and time has remained elusive. Here we characterize the slowdown effect of strong amplification. First, we prove that all strong amplifiers must delay the fixation event at least to some extent. Second, we construct strong amplifiers that delay the fixation event only marginally as compared to the well-mixed populations. Our results thus establish a tight relationship between fixation probability and time: Strong amplification always comes at a cost of a slowdown, but more than a marginal slowdown is not needed.},
  author       = {Tkadlec, Josef and Pavlogiannis, Andreas and Chatterjee, Krishnendu and Nowak, Martin A.},
  issn         = {20411723},
  journal      = {Nature Communications},
  number       = {1},
  publisher    = {Springer Nature},
  title        = {{Fast and strong amplifiers of natural selection}},
  doi          = {10.1038/s41467-021-24271-w},
  volume       = {12},
  year         = {2021},
}

@article{9641,
  abstract     = {At the encounter with a novel environment, contextual memory formation is greatly enhanced, accompanied with increased arousal and active exploration. Although this phenomenon has been widely observed in animal and human daily life, how the novelty in the environment is detected and contributes to contextual memory formation has lately started to be unveiled. The hippocampus has been studied for many decades for its largely known roles in encoding spatial memory, and a growing body of evidence indicates a differential involvement of dorsal and ventral hippocampal divisions in novelty detection. In this brief review article, we discuss the recent findings of the role of mossy cells in the ventral hippocampal moiety in novelty detection and put them in perspective with other novelty-related pathways in the hippocampus. We propose a mechanism for novelty-driven memory acquisition in the dentate gyrus by the direct projection of ventral mossy cells to dorsal dentate granule cells. By this projection, the ventral hippocampus sends novelty signals to the dorsal hippocampus, opening a gate for memory encoding in dentate granule cells based on information coming from the entorhinal cortex. We conclude that, contrary to the presently accepted functional independence, the dorsal and ventral hippocampi cooperate to link the novelty and contextual information, and this dorso-ventral interaction is crucial for the novelty-dependent memory formation.},
  author       = {Fredes, Felipe and Shigemoto, Ryuichi},
  issn         = {10959564},
  journal      = {Neurobiology of Learning and Memory},
  publisher    = {Elsevier},
  title        = {{The role of hippocampal mossy cells in novelty detection}},
  doi          = {10.1016/j.nlm.2021.107486},
  volume       = {183},
  year         = {2021},
}

@article{9642,
  abstract     = {Perineuronal nets (PNNs), components of the extracellular matrix, preferentially coat parvalbumin-positive interneurons and constrain critical-period plasticity in the adult cerebral cortex. Current strategies to remove PNN are long-lasting, invasive, and trigger neuropsychiatric symptoms. Here, we apply repeated anesthetic ketamine as a method with minimal behavioral effect. We find that this paradigm strongly reduces PNN coating in the healthy adult brain and promotes juvenile-like plasticity. Microglia are critically involved in PNN loss because they engage with parvalbumin-positive neurons in their defined cortical layer. We identify external 60-Hz light-flickering entrainment to recapitulate microglia-mediated PNN removal. Importantly, 40-Hz frequency, which is known to remove amyloid plaques, does not induce PNN loss, suggesting microglia might functionally tune to distinct brain frequencies. Thus, our 60-Hz light-entrainment strategy provides an alternative form of PNN intervention in the healthy adult brain.},
  author       = {Venturino, Alessandro and Schulz, Rouven and De Jesús-Cortés, Héctor and Maes, Margaret E and Nagy, Balint and Reilly-Andújar, Francis and Colombo, Gloria and Cubero, Ryan J and Schoot Uiterkamp, Florianne E and Bear, Mark F. and Siegert, Sandra},
  issn         = {22111247},
  journal      = {Cell Reports},
  number       = {1},
  publisher    = {Elsevier},
  title        = {{Microglia enable mature perineuronal nets disassembly upon anesthetic ketamine exposure or 60-Hz light entrainment in the healthy brain}},
  doi          = {10.1016/j.celrep.2021.109313},
  volume       = {36},
  year         = {2021},
}

@inproceedings{9644,
  abstract     = {We present a new approach to proving non-termination of non-deterministic integer programs. Our technique is rather simple but efficient. It relies on a purely syntactic reversal of the program's transition system followed by a constraint-based invariant synthesis with constraints coming from both the original and the reversed transition system. The latter task is performed by a simple call to an off-the-shelf SMT-solver, which allows us to leverage the latest advances in SMT-solving. Moreover, our method offers a combination of features not present (as a whole) in previous approaches: it handles programs with non-determinism, provides relative completeness guarantees and supports programs with polynomial arithmetic. The experiments performed with our prototype tool RevTerm show that our approach, despite its simplicity and stronger theoretical guarantees, is at least on par with the state-of-the-art tools, often achieving a non-trivial improvement under a proper configuration of its parameters.},
  author       = {Chatterjee, Krishnendu and Goharshady, Ehsan Kafshdar and Novotný, Petr and Zikelic, Dorde},
  booktitle    = {Proceedings of the 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation},
  isbn         = {9781450383912},
  location     = {Online},
  pages        = {1033--1048},
  publisher    = {Association for Computing Machinery},
  title        = {{Proving non-termination by program reversal}},
  doi          = {10.1145/3453483.3454093},
  year         = {2021},
}

@inproceedings{9645,
  abstract     = {We consider the fundamental problem of reachability analysis over imperative programs with real variables. Previous works that tackle reachability are either unable to handle programs consisting of general loops (e.g. symbolic execution), or lack completeness guarantees (e.g. abstract interpretation), or are not automated (e.g. incorrectness logic). In contrast, we propose a novel approach for reachability analysis that can handle general and complex loops, is complete, and can be entirely automated for a wide family of programs. Through the notion of Inductive Reachability Witnesses (IRWs), our approach extends ideas from both invariant generation and termination to reachability analysis.

We first show that our IRW-based approach is sound and complete for reachability analysis of imperative programs. Then, we focus on linear and polynomial programs and develop automated methods for synthesizing linear and polynomial IRWs. In the linear case, we follow the well-known approaches using Farkas' Lemma. Our main contribution is in the polynomial case, where we present a push-button semi-complete algorithm. We achieve this using a novel combination of classical theorems in real algebraic geometry, such as Putinar's Positivstellensatz and Hilbert's Strong Nullstellensatz. Finally, our experimental results show we can prove complex reachability objectives over various benchmarks that were beyond the reach of previous methods.},
  author       = {Asadi, Ali and Chatterjee, Krishnendu and Fu, Hongfei and Goharshady, Amir Kafshdar and Mahdavi, Mohammad},
  booktitle    = {Proceedings of the 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation},
  isbn         = {9781450383912},
  location     = {Online},
  pages        = {772--787},
  publisher    = {Association for Computing Machinery},
  title        = {{Polynomial reachability witnesses via Stellensätze}},
  doi          = {10.1145/3453483.3454076},
  year         = {2021},
}

@inproceedings{9646,
  abstract     = {We consider the fundamental problem of deriving quantitative bounds on the probability that a given assertion is violated in a probabilistic program. We provide automated algorithms that obtain both lower and upper bounds on the assertion violation probability. The main novelty of our approach is that we prove new and dedicated fixed-point theorems which serve as the theoretical basis of our algorithms and enable us to reason about assertion violation bounds in terms of pre and post fixed-point functions. To synthesize such fixed-points, we devise algorithms that utilize a wide range of mathematical tools, including repulsing ranking supermartingales, Hoeffding's lemma, Minkowski decompositions, Jensen's inequality, and convex optimization. On the theoretical side, we provide (i) the first automated algorithm for lower-bounds on assertion violation probabilities, (ii) the first complete algorithm for upper-bounds of exponential form in affine programs, and (iii) provably and significantly tighter upper-bounds than the previous approaches. On the practical side, we show our algorithms can handle a wide variety of programs from the literature and synthesize bounds that are remarkably tighter than previous results, in some cases by thousands of orders of magnitude.},
  author       = {Wang, Jinyi and Sun, Yican and Fu, Hongfei and Chatterjee, Krishnendu and Goharshady, Amir Kafshdar},
  booktitle    = {Proceedings of the 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation},
  isbn         = {9781450383912},
  location     = {Online},
  pages        = {1171--1186},
  publisher    = {Association for Computing Machinery},
  title        = {{Quantitative analysis of assertion violations in probabilistic programs}},
  doi          = {10.1145/3453483.3454102},
  year         = {2021},
}

@article{9647,
  abstract     = {Gene expression is regulated by the set of transcription factors (TFs) that bind to the promoter. The ensuing regulating function is often represented as a combinational logic circuit, where output (gene expression) is determined by current input values (promoter bound TFs) only. However, the simultaneous arrival of TFs is a strong assumption, since transcription and translation of genes introduce intrinsic time delays and there is no global synchronisation among the arrival times of different molecular species at their targets. We present an experimentally implementable genetic circuit with two inputs and one output, which in the presence of small delays in input arrival, exhibits qualitatively distinct population-level phenotypes, over timescales that are longer than typical cell doubling times. From a dynamical systems point of view, these phenotypes represent long-lived transients: although they converge to the same value eventually, they do so after a very long time span. The key feature of this toy model genetic circuit is that, despite having only two inputs and one output, it is regulated by twenty-three distinct DNA-TF configurations, two of which are more stable than others (DNA looped states), one promoting and another blocking the expression of the output gene. Small delays in input arrival time result in a majority of cells in the population quickly reaching the stable state associated with the first input, while exiting of this stable state occurs at a slow timescale. In order to mechanistically model the behaviour of this genetic circuit, we used a rule-based modelling language, and implemented a grid-search to find parameter combinations giving rise to long-lived transients. Our analysis shows that in the absence of feedback, there exist path-dependent gene regulatory mechanisms based on the long timescale of transients. The behaviour of this toy model circuit suggests that gene regulatory networks can exploit event timing to create phenotypes, and it opens the possibility that they could use event timing to memorise events, without regulatory feedback. The model reveals the importance of (i) mechanistically modelling the transitions between the different DNA-TF states, and (ii) employing transient analysis thereof.},
  author       = {Petrov, Tatjana and Igler, Claudia and Sezgin, Ali and Henzinger, Thomas A and Guet, Calin C},
  issn         = {0304-3975},
  journal      = {Theoretical Computer Science},
  pages        = {1--16},
  publisher    = {Elsevier},
  title        = {{Long lived transients in gene regulation}},
  doi          = {10.1016/j.tcs.2021.05.023},
  volume       = {893},
  year         = {2021},
}

@article{9656,
  abstract     = {Tropisms, growth responses to environmental stimuli such as light or gravity, are spectacular examples of adaptive plant development. The plant hormone auxin serves as a major coordinative signal. The PIN auxin exporters, through their dynamic polar subcellular localizations, redirect auxin fluxes in response to environmental stimuli and the resulting auxin gradients across organs underly differential cell elongation and bending. In this review, we discuss recent advances concerning regulations of PIN polarity during tropisms, focusing on PIN phosphorylation and trafficking. We also cover how environmental cues regulate PIN actions during tropisms, and a crucial role of auxin feedback on PIN polarity during bending termination. Finally, the interactions between different tropisms are reviewed to understand plant adaptive growth in the natural environment.},
  author       = {Han, Huibin and Adamowski, Maciek and Qi, Linlin and Alotaibi, SS and Friml, Jiří},
  issn         = {1469-8137},
  journal      = {New Phytologist},
  number       = {2},
  pages        = {510--522},
  publisher    = {Wiley},
  title        = {{PIN-mediated polar auxin transport regulations in plant tropic responses}},
  doi          = {10.1111/nph.17617},
  volume       = {232},
  year         = {2021},
}

