@article{6832,
  abstract     = {Steady-state turnover is a hallmark of epithelial tissues throughout adult life. Intestinal epithelial turnover is marked by continuous cell migration, which is assumed to be driven by mitotic pressure from the crypts. However, the balance of forces in renewal remains ill-defined. Combining biophysical modeling and quantitative three-dimensional tissue imaging with genetic and physical manipulations, we revealed the existence of an actin-related protein 2/3 complex–dependent active migratory force, which explains quantitatively the profiles of cell speed, density, and tissue tension along the villi. Cells migrate collectively with minimal rearrangements while displaying dual—apicobasal and front-back—polarity characterized by actin-rich basal protrusions oriented in the direction of migration. We propose that active migration is a critical component of gut epithelial turnover.},
  author       = {Krndija, Denis and Marjou, Fatima El and Guirao, Boris and Richon, Sophie and Leroy, Olivier and Bellaiche, Yohanns and Hannezo, Edouard B and Vignjevic, Danijela Matic},
  journal      = {Science},
  number       = {6454},
  pages        = {705--710},
  publisher    = {American Association for the Advancement of Science},
  title        = {{Active cell migration is critical for steady-state epithelial turnover in the gut}},
  doi          = {10.1126/science.aau3429},
  volume       = {365},
  year         = {2019},
}

@article{6837,
  abstract     = {Migrasomes are a recently discovered type of extracellular vesicles that are characteristically generated along retraction fibers in migrating cells. Two studies now show how migrasomes are formed and how they function in the physiologically relevant context of the developing zebrafish embryo.},
  author       = {Tavano, Ste and Heisenberg, Carl-Philipp J},
  issn         = {1476-4679},
  journal      = {Nature Cell Biology},
  number       = {8},
  pages        = {918--920},
  publisher    = {Springer Nature},
  title        = {{Migrasomes take center stage}},
  doi          = {10.1038/s41556-019-0369-3},
  volume       = {21},
  year         = {2019},
}

@phdthesis{6894,
  abstract     = {Hybrid automata combine finite automata and dynamical systems, and model the interaction of digital with physical systems. Formal analysis that can guarantee the safety of all behaviors or rigorously witness failures, while unsolvable in general, has been tackled algorithmically using, e.g., abstraction, bounded model-checking, assisted theorem proving.
Nevertheless, very few methods have addressed the time-unbounded reachability analysis of hybrid automata and, for current sound and automatic tools, scalability remains critical. We develop methods for the polyhedral abstraction of hybrid automata, which construct coarse overapproximations and tightens them incrementally, in a CEGAR fashion. We use template polyhedra, i.e., polyhedra whose facets are normal to a given set of directions.
While, previously, directions were given by the user, we introduce (1) the first method
for computing template directions from spurious counterexamples, so as to generalize and
eliminate them. The method applies naturally to convex hybrid automata, i.e., hybrid
automata with (possibly non-linear) convex constraints on derivatives only, while for linear
ODE requires further abstraction. Specifically, we introduce (2) the conic abstractions,
which, partitioning the state space into appropriate (possibly non-uniform) cones, divide
curvy trajectories into relatively straight sections, suitable for polyhedral abstractions.
Finally, we introduce (3) space-time interpolation, which, combining interval arithmetic
and template refinement, computes appropriate (possibly non-uniform) time partitioning
and template directions along spurious trajectories, so as to eliminate them.
We obtain sound and automatic methods for the reachability analysis over dense
and unbounded time of convex hybrid automata and hybrid automata with linear ODE.
We build prototype tools and compare—favorably—our methods against the respective
state-of-the-art tools, on several benchmarks.},
  author       = {Giacobbe, Mirco},
  issn         = {2663-337X},
  pages        = {132},
  publisher    = {Institute of Science and Technology Austria},
  title        = {{Automatic time-unbounded reachability analysis of hybrid systems}},
  doi          = {10.15479/AT:ISTA:6894},
  year         = {2019},
}

@inproceedings{6931,
  abstract     = {Consider a distributed system with n processors out of which f can be Byzantine faulty. In the
approximate agreement task, each processor i receives an input value xi and has to decide on an
output value yi such that
1. the output values are in the convex hull of the non-faulty processors’ input values,
2. the output values are within distance d of each other.


Classically, the values are assumed to be from an m-dimensional Euclidean space, where m ≥ 1.
In this work, we study the task in a discrete setting, where input values with some structure
expressible as a graph. Namely, the input values are vertices of a finite graph G and the goal is to
output vertices that are within distance d of each other in G, but still remain in the graph-induced
convex hull of the input values. For d = 0, the task reduces to consensus and cannot be solved with
a deterministic algorithm in an asynchronous system even with a single crash fault. For any d ≥ 1,
we show that the task is solvable in asynchronous systems when G is chordal and n > (ω + 1)f,
where ω is the clique number of G. In addition, we give the first Byzantine-tolerant algorithm for a
variant of lattice agreement. For synchronous systems, we show tight resilience bounds for the exact
variants of these and related tasks over a large class of combinatorial structures.},
  author       = {Nowak, Thomas and Rybicki, Joel},
  booktitle    = {33rd International Symposium on Distributed Computing},
  keywords     = {consensus, approximate agreement, Byzantine faults, chordal graphs, lattice agreement},
  location     = {Budapest, Hungary},
  pages        = {29:1----29:17},
  publisher    = {Schloss Dagstuhl - Leibniz-Zentrum für Informatik},
  title        = {{Byzantine approximate agreement on graphs}},
  doi          = {10.4230/LIPICS.DISC.2019.29},
  volume       = {146},
  year         = {2019},
}

@inproceedings{6942,
  abstract     = {Graph games and Markov decision processes (MDPs) are standard models in reactive synthesis and verification of probabilistic systems with nondeterminism. The class of   𝜔 -regular winning conditions; e.g., safety, reachability, liveness, parity conditions; provides a robust and expressive specification formalism for properties that arise in analysis of reactive systems. The resolutions of nondeterminism in games and MDPs are represented as strategies, and we consider succinct representation of such strategies. The decision-tree data structure from machine learning retains the flavor of decisions of strategies and allows entropy-based minimization to obtain succinct trees. However, in contrast to traditional machine-learning problems where small errors are allowed, for winning strategies in graph games and MDPs no error is allowed, and the decision tree must represent the entire strategy. In this work we propose decision trees with linear classifiers for representation of strategies in graph games and MDPs. We have implemented strategy representation using this data structure and we present experimental results for problems on graph games and MDPs, which show that this new data structure presents a much more efficient strategy representation as compared to standard decision trees.},
  author       = {Ashok, Pranav and Brázdil, Tomáš and Chatterjee, Krishnendu and Křetínský, Jan and Lampert, Christoph and Toman, Viktor},
  booktitle    = {16th International Conference on Quantitative Evaluation of Systems},
  isbn         = {9783030302801},
  issn         = {0302-9743},
  location     = {Glasgow, United Kingdom},
  pages        = {109--128},
  publisher    = {Springer Nature},
  title        = {{Strategy representation by decision trees with linear classifiers}},
  doi          = {10.1007/978-3-030-30281-8_7},
  volume       = {11785},
  year         = {2019},
}

@article{6972,
  abstract     = {We give fault-tolerant algorithms for establishing synchrony in distributed systems in which each of thennodes has its own clock. Our algorithms operate in a very strong fault model: we require self-stabilisation, i.e.,the initial state of the system may be arbitrary, and there can be up to f<n/3 ongoing Byzantine faults, i.e.,nodes that deviate from the protocol in an arbitrary manner. Furthermore, we assume that the local clocks ofthe nodes may progress at different speeds (clock drift) and communication has bounded delay. In this model,we study the pulse synchronisation problem, where the task is to guarantee that eventually all correct nodesgenerate well-separated local pulse events (i.e., unlabelled logical clock ticks) in a synchronised manner.Compared to prior work, we achieveexponentialimprovements in stabilisation time and the number ofcommunicated bits, and give the first sublinear-time algorithm for the problem:•In the deterministic setting, the state-of-the-art solutions stabilise in timeΘ(f)and have each nodebroadcastΘ(flogf)bits per time unit. We exponentially reduce the number of bits broadcasted pertime unit toΘ(logf)while retaining the same stabilisation time.•In the randomised setting, the state-of-the-art solutions stabilise in timeΘ(f)and have each nodebroadcastO(1)bits per time unit. We exponentially reduce the stabilisation time to polylogfwhileeach node broadcasts polylogfbits per time unit.These results are obtained by means of a recursive approach reducing the above task ofself-stabilisingpulse synchronisation in thebounded-delaymodel tonon-self-stabilisingbinary consensus in thesynchro-nousmodel. In general, our approach introduces at most logarithmic overheads in terms of stabilisation timeand broadcasted bits over the underlying consensus routine.},
  author       = {Lenzen, Christoph and Rybicki, Joel},
  issn         = {0004-5411},
  journal      = {Journal of the ACM},
  number       = {5},
  publisher    = {ACM},
  title        = {{Self-stabilising Byzantine clock synchronisation is almost as easy as consensus}},
  doi          = {10.1145/3339471},
  volume       = {66},
  year         = {2019},
}

@inbook{6987,
  abstract     = {Cells are arranged into species-specific patterns during early embryogenesis. Such cell division patterns are important since they often reflect the distribution of localized cortical factors from eggs/fertilized eggs to specific cells as well as the emergence of organismal form. However, it has proven difficult to reveal the mechanisms that underlie the emergence of cell positioning patterns that underlie embryonic shape, likely because a systems-level approach is required that integrates cell biological, genetic, developmental, and mechanical parameters. The choice of organism to address such questions is also important. Because ascidians display the most extreme form of invariant cleavage pattern among the metazoans, we have been analyzing the cell biological mechanisms that underpin three aspects of cell division (unequal cell division (UCD), oriented cell division (OCD), and asynchronous cell cycles) which affect the overall shape of the blastula-stage ascidian embryo composed of 64 cells. In ascidians, UCD creates two small cells at the 16-cell stage that in turn undergo two further successive rounds of UCD. Starting at the 16-cell stage, the cell cycle becomes asynchronous, whereby the vegetal half divides before the animal half, thus creating 24-, 32-, 44-, and then 64-cell stages. Perturbing either UCD or the alternate cell division rhythm perturbs cell position. We propose that dynamic cell shape changes propagate throughout the embryo via cell-cell contacts to create the ascidian-specific invariant cleavage pattern.},
  author       = {McDougall, Alex and Chenevert, Janet and Godard, Benoit G and Dumollard, Remi},
  booktitle    = {Evo-Devo: Non-model species in cell and developmental biology},
  editor       = {Tworzydlo, Waclaw and Bilinski, Szczepan M.},
  isbn         = {9783030234584},
  issn         = {1861-0412},
  pages        = {127--154},
  publisher    = {Springer Nature},
  title        = {{Emergence of embryo shape during cleavage divisions}},
  doi          = {10.1007/978-3-030-23459-1_6},
  volume       = {68},
  year         = {2019},
}

@article{6999,
  abstract     = {Plasmodesmata (PD) are plant-specific membrane-lined channels that create cytoplasmic and membrane continuities between adjacent cells, thereby facilitating cell–cell communication and virus movement. Plant cells have evolved diverse mechanisms to regulate PD plasticity in response to numerous environmental stimuli. In particular, during defense against plant pathogens, the defense hormone, salicylic acid (SA), plays a crucial role in the regulation of PD permeability in a callose-dependent manner. Here, we uncover a mechanism by which plants restrict the spreading of virus and PD cargoes using SA signaling by increasing lipid order and closure of PD. We showed that exogenous SA application triggered the compartmentalization of lipid raft nanodomains through a modulation of the lipid raft-regulatory protein, Remorin (REM). Genetic studies, superresolution imaging, and transmission electron microscopy observation together demonstrated that Arabidopsis REM1.2 and REM1.3 are crucial for plasma membrane nanodomain assembly to control PD aperture and functionality. In addition, we also found that a 14-3-3 epsilon protein modulates REM clustering and membrane nanodomain compartmentalization through its direct interaction with REM proteins. This study unveils a molecular mechanism by which the key plant defense hormone, SA, triggers membrane lipid nanodomain reorganization, thereby regulating PD closure to impede virus spreading.},
  author       = {Huang, D and Sun, Y and Ma, Z and Ke, M and Cui, Y and Chen, Z and Chen, C and Ji, C and Tran, TM and Yang, L and Lam, SM and Han, Y and Shu, G and Friml, Jiří and Miao, Y and Jiang, L and Chen, X},
  issn         = {1091-6490},
  journal      = {Proceedings of the National Academy of Sciences of the United States of America},
  number       = {42},
  pages        = {21274--21284},
  publisher    = {National Academy of Sciences},
  title        = {{Salicylic acid-mediated plasmodesmal closure via Remorin-dependent lipid organization}},
  doi          = {10.1073/pnas.1911892116},
  volume       = {116},
  year         = {2019},
}

@article{7093,
  abstract     = {In graph theory, as well as in 3-manifold topology, there exist several width-type parameters to describe how "simple" or "thin" a given graph or 3-manifold is. These parameters, such as pathwidth or treewidth for graphs, or the concept of thin position for 3-manifolds, play an important role when studying algorithmic problems; in particular, there is a variety of problems in computational 3-manifold topology - some of them known to be computationally hard in general - that become solvable in polynomial time as soon as the dual graph of the input triangulation has bounded treewidth.
In view of these algorithmic results, it is natural to ask whether every 3-manifold admits a triangulation of bounded treewidth. We show that this is not the case, i.e., that there exists an infinite family of closed 3-manifolds not admitting triangulations of bounded pathwidth or treewidth (the latter implies the former, but we present two separate proofs).
We derive these results from work of Agol, of Scharlemann and Thompson, and of Scharlemann, Schultens and Saito by exhibiting explicit connections between the topology of a 3-manifold M on the one hand and width-type parameters of the dual graphs of triangulations of M on the other hand, answering a question that had been raised repeatedly by researchers in computational 3-manifold topology. In particular, we show that if a closed, orientable, irreducible, non-Haken 3-manifold M has a triangulation of treewidth (resp. pathwidth) k then the Heegaard genus of M is at most 18(k+1) (resp. 4(3k+1)).},
  author       = {Huszár, Kristóf and Spreer, Jonathan and Wagner, Uli},
  issn         = {1920-180X},
  journal      = {Journal of Computational Geometry},
  number       = {2},
  pages        = {70–98},
  publisher    = {Computational Geometry Laborartoy},
  title        = {{On the treewidth of triangulated 3-manifolds}},
  doi          = {10.20382/JOGC.V10I2A5},
  volume       = {10},
  year         = {2019},
}

@article{7108,
  abstract     = {We prove that for every d ≥ 2, deciding if a pure, d-dimensional, simplicial complex is shellable is NP-hard, hence NP-complete. This resolves a question raised, e.g., by Danaraj and Klee in 1978. Our reduction also yields that for every d ≥ 2 and k ≥ 0, deciding if a pure, d-dimensional, simplicial complex is k-decomposable is NP-hard. For d ≥ 3, both problems remain NP-hard when restricted to contractible pure d-dimensional complexes. Another simple corollary of our result is that it is NP-hard to decide whether a given poset is CL-shellable.},
  author       = {Goaoc, Xavier and Patak, Pavel and Patakova, Zuzana and Tancer, Martin and Wagner, Uli},
  issn         = {0004-5411},
  journal      = {Journal of the ACM},
  number       = {3},
  publisher    = {ACM},
  title        = {{Shellability is NP-complete}},
  doi          = {10.1145/3314024},
  volume       = {66},
  year         = {2019},
}

@inproceedings{7147,
  abstract     = {The expression of a gene is characterised by its transcription factors and the function processing them. If the transcription factors are not affected by gene products, the regulating function is often represented as a combinational logic circuit, where the outputs (product) are determined by current input values (transcription factors) only, and are hence independent on their relative arrival times. However, the simultaneous arrival of transcription factors (TFs) in genetic circuits is a strong assumption, given that the processes of transcription and translation of a gene into a protein introduce intrinsic time delays and that there is no global synchronisation among the arrival times of different molecular species at molecular targets.

In this paper, we construct an experimentally implementable genetic circuit with two inputs and a single output, such that, in presence of small delays in input arrival, the circuit exhibits qualitatively distinct observable phenotypes. In particular, these phenotypes are long lived transients: they all converge to a single value, but so slowly, that they seem stable for an extended time period, longer than typical experiment duration. We used rule-based language to prototype our circuit, and we implemented a search for finding the parameter combinations raising the phenotypes of interest.

The behaviour of our prototype circuit has wide implications. First, it suggests that GRNs can exploit event timing to create phenotypes. Second, it opens the possibility that GRNs are using event timing to react to stimuli and memorise events, without explicit feedback in regulation. From the modelling perspective, our prototype circuit demonstrates the critical importance of analysing the transient dynamics at the promoter binding sites of the DNA, before applying rapid equilibrium assumptions.},
  author       = {Guet, Calin C and Henzinger, Thomas A and Igler, Claudia and Petrov, Tatjana and Sezgin, Ali},
  booktitle    = {17th International Conference on Computational Methods in Systems Biology},
  isbn         = {9783030313036},
  issn         = {1611-3349},
  location     = {Trieste, Italy},
  pages        = {155--187},
  publisher    = {Springer Nature},
  title        = {{Transient memory in gene regulation}},
  doi          = {10.1007/978-3-030-31304-3_9},
  volume       = {11773},
  year         = {2019},
}

@article{7150,
  abstract     = {In this work, we use algebraic methods for studying distance computation and subgraph detection tasks in the congested clique model. Specifically, we adapt parallel matrix multiplication implementations to the congested clique, obtaining an O(n1−2/ω) round matrix multiplication algorithm, where ω<2.3728639 is the exponent of matrix multiplication. In conjunction with known techniques from centralised algorithmics, this gives significant improvements over previous best upper bounds in the congested clique model. The highlight results include:

1.    triangle and 4-cycle counting in O(n0.158) rounds, improving upon the O(n1/3) algorithm of Dolev et al. [DISC 2012],
2. a (1+o(1))-approximation of all-pairs shortest paths in O(n0.158) rounds, improving upon the O~(n1/2)-round (2+o(1))-approximation algorithm given by Nanongkai [STOC 2014], and
 3. computing the girth in O(n0.158) rounds, which is the first non-trivial solution in this model.
   
In addition, we present a novel constant-round combinatorial algorithm for detecting 4-cycles.},
  author       = {Censor-Hillel, Keren and Kaski, Petteri and Korhonen, Janne and Lenzen, Christoph and Paz, Ami and Suomela, Jukka},
  issn         = {0178-2770},
  journal      = {Distributed Computing},
  number       = {6},
  pages        = {461--478},
  publisher    = {Springer Nature},
  title        = {{Algebraic methods in the congested clique}},
  doi          = {10.1007/s00446-016-0270-2},
  volume       = {32},
  year         = {2019},
}

@inproceedings{7159,
  abstract     = {Cyber-physical systems (CPS) and the Internet-of-Things (IoT) result in a tremendous amount of generated, measured and recorded time-series data. Extracting temporal segments that encode patterns with useful information out of these huge amounts of data is an extremely difficult problem. We propose shape expressions as a declarative formalism for specifying, querying and extracting sophisticated temporal patterns from possibly noisy data. Shape expressions are regular expressions with arbitrary (linear, exponential, sinusoidal, etc.) shapes with parameters as atomic predicates and additional constraints on these parameters. We equip shape expressions with a novel noisy semantics that combines regular expression matching semantics with statistical regression. We characterize essential properties of the formalism and propose an efficient approximate shape expression matching procedure. We demonstrate the wide applicability of this technique on two case studies. },
  author       = {Ničković, Dejan and Qin, Xin and Ferrere, Thomas and Mateis, Cristinel and Deshmukh, Jyotirmoy},
  booktitle    = {19th International Conference on Runtime Verification},
  isbn         = {9783030320782},
  issn         = {0302-9743},
  location     = {Porto, Portugal},
  pages        = {292--309},
  publisher    = {Springer Nature},
  title        = {{Shape expressions for specifying and extracting signal features}},
  doi          = {10.1007/978-3-030-32079-9_17},
  volume       = {11757},
  year         = {2019},
}

@book{7171,
  abstract     = {Wissen Sie, was sich hinter künstlicher Intelligenz und maschinellem Lernen verbirgt? 
Dieses Sachbuch erklärt Ihnen leicht verständlich und ohne komplizierte Formeln die grundlegenden Methoden und Vorgehensweisen des maschinellen Lernens. Mathematisches Vorwissen ist dafür nicht nötig. Kurzweilig und informativ illustriert Lisa, die Protagonistin des Buches, diese anhand von Alltagssituationen. 
Ein Buch für alle, die in Diskussionen über Chancen und Risiken der aktuellen Entwicklung der künstlichen Intelligenz und des maschinellen Lernens mit Faktenwissen punkten möchten. Auch für Schülerinnen und Schüler geeignet!},
  editor       = {Kersting, Kristian and Lampert, Christoph and Rothkopf, Constantin},
  isbn         = {978-3-658-26762-9},
  pages        = {XIV, 245},
  publisher    = {Springer Nature},
  title        = {{Wie Maschinen Lernen: Künstliche Intelligenz Verständlich Erklärt}},
  doi          = {10.1007/978-3-658-26763-6},
  year         = {2019},
}

@article{7179,
  abstract     = {Glutamate is the major excitatory neurotransmitter in the CNS binding to a variety of glutamate receptors. Metabotropic glutamate receptors (mGluR1 to mGluR8) can act excitatory or inhibitory, depending on associated signal cascades. Expression and localization of inhibitory acting mGluRs at inner hair cells (IHCs) in the cochlea are largely unknown. Here, we analyzed expression of mGluR2, mGluR3, mGluR4, mGluR6, mGluR7, and mGluR8 and investigated their localization with respect to the presynaptic ribbon of IHC synapses. We detected transcripts for mGluR2, mGluR3, and mGluR4 as well as for mGluR7a, mGluR7b, mGluR8a, and mGluR8b splice variants. Using receptor-specific antibodies in cochlear wholemounts, we found expression of mGluR2, mGluR4, and mGluR8b close to presynaptic ribbons. Super resolution and confocal microscopy in combination with 3-dimensional reconstructions indicated a postsynaptic localization of mGluR2 that overlaps with postsynaptic density protein 95 on dendrites of afferent type I spiral ganglion neurons. In contrast, mGluR4 and mGluR8b were expressed at the presynapse close to IHC ribbons. In summary, we localized in detail 3 mGluR types at IHC ribbon synapses, providing a fundament for new therapeutical strategies that could protect the cochlea against noxious stimuli and excitotoxicity.},
  author       = {Klotz, Lisa and Wendler, Olaf and Frischknecht, Renato and Shigemoto, Ryuichi and Schulze, Holger and Enz, Ralf},
  issn         = {1530-6860},
  journal      = {FASEB Journal},
  number       = {12},
  pages        = {13734--13746},
  publisher    = {FASEB},
  title        = {{Localization of group II and III metabotropic glutamate receptors at pre- and postsynaptic sites of inner hair cell ribbon synapses}},
  doi          = {10.1096/fj.201901543R},
  volume       = {33},
  year         = {2019},
}

@inproceedings{7183,
  abstract     = {A probabilistic vector addition system with states (pVASS) is a finite state Markov process augmented with non-negative integer counters that can be incremented or decremented during each state transition, blocking any behaviour that would cause a counter to decrease below zero. The pVASS can be used as abstractions of probabilistic programs with many decidable properties. The use of pVASS as abstractions requires the presence of nondeterminism in the model. In this paper, we develop techniques for checking fast termination of pVASS with nondeterminism. That is, for every initial configuration of size n, we consider the worst expected number of transitions needed to reach a configuration with some counter negative (the expected termination time). We show that the problem whether the asymptotic expected termination time is linear is decidable in polynomial time for a certain natural class of pVASS with nondeterminism. Furthermore, we show the following dichotomy: if the asymptotic expected termination time is not linear, then it is at least quadratic, i.e., in Ω(n2).},
  author       = {Brázdil, Tomás and Chatterjee, Krishnendu and Kucera, Antonín and Novotný, Petr and Velan, Dominik},
  booktitle    = {International Symposium on Automated Technology for Verification and Analysis},
  isbn         = {9783030317836},
  issn         = {1611-3349},
  location     = {Taipei, Taiwan},
  pages        = {462--478},
  publisher    = {Springer Nature},
  title        = {{Deciding fast termination for probabilistic VASS with nondeterminism}},
  doi          = {10.1007/978-3-030-31784-3_27},
  volume       = {11781},
  year         = {2019},
}

@article{72,
  abstract     = {We consider the totally asymmetric simple exclusion process (TASEP) with non-random initial condition having density ρ on ℤ− and λ on ℤ+, and a second class particle initially at the origin. For ρ&lt;λ, there is a shock and the second class particle moves with speed 1−λ−ρ. For large time t, we show that the position of the second class particle fluctuates on a t1/3 scale and determine its limiting law. We also obtain the limiting distribution of the number of steps made by the second class particle until time t.},
  author       = {Ferrari, Patrick and Ghosal, Promit and Nejjar, Peter},
  issn         = {0246-0203},
  journal      = {Annales de l'institut Henri Poincare (B) Probability and Statistics},
  number       = {3},
  pages        = {1203--1225},
  publisher    = {Institute of Mathematical Statistics},
  title        = {{Limit law of a second class particle in TASEP with non-random initial condition}},
  doi          = {10.1214/18-AIHP916},
  volume       = {55},
  year         = {2019},
}

@inproceedings{7228,
  abstract     = {Traditional concurrent programming involves manipulating shared mutable state. Alternatives to this programming style are communicating sequential processes (CSP) and actor models, which share data via explicit communication. These models have been known for almost half a century, and have recently had started to gain significant traction among modern programming languages. The common abstraction for communication between several processes is the channel. Although channels are similar to producer-consumer data structures, they have different semantics and support additional operations, such as the select expression. Despite their growing popularity, most known implementations of channels use lock-based data structures and can be rather inefficient.

In this paper, we present the first efficient lock-free algorithm for implementing a communication channel for CSP programming. We provide implementations and experimental results in the Kotlin and Go programming languages. Our new algorithm outperforms existing implementations on many workloads, while providing non-blocking progress guarantee. Our design can serve as an example of how to construct general communication data structures for CSP and actor models. },
  author       = {Koval, Nikita and Alistarh, Dan-Adrian and Elizarov, Roman},
  booktitle    = {25th Anniversary of Euro-Par},
  isbn         = {978-3-0302-9399-4},
  issn         = {1611-3349},
  location     = {Göttingen, Germany},
  pages        = {317--333},
  publisher    = {Springer Nature},
  title        = {{Scalable FIFO channels for programming via communicating sequential processes}},
  doi          = {10.1007/978-3-030-29400-7_23},
  volume       = {11725},
  year         = {2019},
}

@inproceedings{7230,
  abstract     = {Simple drawings of graphs are those in which each pair of edges share at most one point, either a common endpoint or a proper crossing. In this paper we study the problem of extending a simple drawing D(G) of a graph G by inserting a set of edges from the complement of G into D(G) such that the result is a simple drawing. In the context of rectilinear drawings, the problem is trivial. For pseudolinear drawings, the existence of such an extension follows from Levi’s enlargement lemma. In contrast, we prove that deciding if a given set of edges can be inserted into a simple drawing is NP-complete. Moreover, we show that the maximization version of the problem is APX-hard. We also present a polynomial-time algorithm for deciding whether one edge uv can be inserted into D(G) when {u,v} is a dominating set for the graph G.},
  author       = {Arroyo Guevara, Alan M and Derka, Martin and Parada, Irene},
  booktitle    = {27th International Symposium on Graph Drawing and Network Visualization},
  isbn         = {978-3-0303-5801-3},
  issn         = {1611-3349},
  location     = {Prague, Czech Republic},
  pages        = {230--243},
  publisher    = {Springer Nature},
  title        = {{Extending simple drawings}},
  doi          = {10.1007/978-3-030-35802-0_18},
  volume       = {11904},
  year         = {2019},
}

@inproceedings{7231,
  abstract     = {Piecewise Barrier Tubes (PBT) is a new technique for flowpipe overapproximation for nonlinear systems with polynomial dynamics, which leverages a combination of barrier certificates. PBT has advantages over traditional time-step based methods in dealing with those nonlinear dynamical systems in which there is a large difference in speed between trajectories, producing an overapproximation that is time independent. However, the existing approach for PBT is not efficient due to the application of interval methods for enclosure-box computation, and it can only deal with continuous dynamical systems without uncertainty. In this paper, we extend the approach with the ability to handle both continuous and hybrid dynamical systems with uncertainty that can reside in parameters and/or noise. We also improve the efficiency of the method significantly, by avoiding the use of interval-based methods for the enclosure-box computation without loosing soundness. We have developed a C++ prototype implementing the proposed approach and we evaluate it on several benchmarks. The experiments show that our approach is more efficient and precise than other methods in the literature.},
  author       = {Kong, Hui and Bartocci, Ezio and Jiang, Yu and Henzinger, Thomas A},
  booktitle    = {17th International Conference on Formal Modeling and Analysis of Timed Systems},
  isbn         = {978-3-0302-9661-2},
  issn         = {1611-3349},
  location     = {Amsterdam, The Netherlands},
  pages        = {123--141},
  publisher    = {Springer Nature},
  title        = {{Piecewise robust barrier tubes for nonlinear hybrid systems with uncertainty}},
  doi          = {10.1007/978-3-030-29662-9_8},
  volume       = {11750},
  year         = {2019},
}