@article{1207, abstract = {The eigenvalue distribution of the sum of two large Hermitian matrices, when one of them is conjugated by a Haar distributed unitary matrix, is asymptotically given by the free convolution of their spectral distributions. We prove that this convergence also holds locally in the bulk of the spectrum, down to the optimal scales larger than the eigenvalue spacing. The corresponding eigenvectors are fully delocalized. Similar results hold for the sum of two real symmetric matrices, when one is conjugated by Haar orthogonal matrix.}, author = {Bao, Zhigang and Erdös, László and Schnelli, Kevin}, issn = {0010-3616}, journal = {Communications in Mathematical Physics}, number = {3}, pages = {947 -- 990}, publisher = {Springer}, title = {{Local law of addition of random matrices on optimal scale}}, doi = {10.1007/s00220-016-2805-6}, volume = {349}, year = {2017}, } @article{1208, abstract = {We study parameter estimation in linear Gaussian covariance models, which are p-dimensional Gaussian models with linear constraints on the covariance matrix. Maximum likelihood estimation for this class of models leads to a non-convex optimization problem which typically has many local maxima. Using recent results on the asymptotic distribution of extreme eigenvalues of the Wishart distribution, we provide sufficient conditions for any hill climbing method to converge to the global maximum. Although we are primarily interested in the case in which n≫p, the proofs of our results utilize large sample asymptotic theory under the scheme n/p→γ>1. Remarkably, our numerical simulations indicate that our results remain valid for p as small as 2. An important consequence of this analysis is that, for sample sizes n≃14p, maximum likelihood estimation for linear Gaussian covariance models behaves as if it were a convex optimization problem. © 2016 The Royal Statistical Society and Blackwell Publishing Ltd.}, author = {Zwiernik, Piotr and Uhler, Caroline and Richards, Donald}, issn = {1369-7412}, journal = {Journal of the Royal Statistical Society. Series B: Statistical Methodology}, number = {4}, pages = {1269 -- 1292}, publisher = {Wiley-Blackwell}, title = {{Maximum likelihood estimation for linear Gaussian covariance models}}, doi = {10.1111/rssb.12217}, volume = {79}, year = {2017}, } @article{1211, abstract = {Systems such as fluid flows in channels and pipes or the complex Ginzburg–Landau system, defined over periodic domains, exhibit both continuous symmetries, translational and rotational, as well as discrete symmetries under spatial reflections or complex conjugation. The simplest, and very common symmetry of this type is the equivariance of the defining equations under the orthogonal group O(2). We formulate a novel symmetry reduction scheme for such systems by combining the method of slices with invariant polynomial methods, and show how it works by applying it to the Kuramoto–Sivashinsky system in one spatial dimension. As an example, we track a relative periodic orbit through a sequence of bifurcations to the onset of chaos. Within the symmetry-reduced state space we are able to compute and visualize the unstable manifolds of relative periodic orbits, their torus bifurcations, a transition to chaos via torus breakdown, and heteroclinic connections between various relative periodic orbits. It would be very hard to carry through such analysis in the full state space, without a symmetry reduction such as the one we present here.}, author = {Budanur, Nazmi B and Cvitanović, Predrag}, journal = {Journal of Statistical Physics}, number = {3-4}, pages = {636--655}, publisher = {Springer}, title = {{Unstable manifolds of relative periodic orbits in the symmetry reduced state space of the Kuramoto–Sivashinsky system}}, doi = {10.1007/s10955-016-1672-z}, volume = {167}, year = {2017}, } @inbook{1213, abstract = {Bacterial cytokinesis is commonly initiated by the Z-ring, a dynamic cytoskeletal structure that assembles at the site of division. Its primary component is FtsZ, a tubulin-like GTPase, that like its eukaryotic relative forms protein filaments in the presence of GTP. Since the discovery of the Z-ring 25 years ago, various models for the role of FtsZ have been suggested. However, important information about the architecture and dynamics of FtsZ filaments during cytokinesis is still missing. One reason for this lack of knowledge has been the small size of bacteria, which has made it difficult to resolve the orientation and dynamics of individual FtsZ filaments in the Z-ring. While superresolution microscopy experiments have helped to gain more information about the organization of the Z-ring in the dividing cell, they were not yet able to elucidate a mechanism of how FtsZ filaments reorganize during assembly and disassembly of the Z-ring. In this chapter, we explain how to use an in vitro reconstitution approach to investigate the self-organization of FtsZ filaments recruited to a biomimetic lipid bilayer by its membrane anchor FtsA. We show how to perform single-molecule experiments to study the behavior of individual FtsZ monomers during the constant reorganization of the FtsZ-FtsA filament network. We describe how to analyze the dynamics of single molecules and explain why this information can help to shed light onto possible mechanism of Z-ring constriction. We believe that similar experimental approaches will be useful to study the mechanism of membrane-based polymerization of other cytoskeletal systems, not only from prokaryotic but also eukaryotic origin.}, author = {Baranova, Natalia and Loose, Martin}, booktitle = {Cytokinesis}, editor = {Echard, Arnaud }, issn = {0091-679X}, pages = {355 -- 370}, publisher = {Academic Press}, title = {{Single-molecule measurements to study polymerization dynamics of FtsZ-FtsA copolymers}}, doi = {10.1016/bs.mcb.2016.03.036}, volume = {137}, year = {2017}, } @article{12193, abstract = {DNA methylation regulates eukaryotic gene expression and is extensively reprogrammed during animal development. However, whether developmental methylation reprogramming during the sporophytic life cycle of flowering plants regulates genes is presently unknown. Here we report a distinctive gene-targeted RNA-directed DNA methylation (RdDM) activity in the Arabidopsis thaliana male sexual lineage that regulates gene expression in meiocytes. Loss of sexual-lineage-specific RdDM causes mis-splicing of the MPS1 gene (also known as PRD2), thereby disrupting meiosis. Our results establish a regulatory paradigm in which de novo methylation creates a cell-lineage-specific epigenetic signature that controls gene expression and contributes to cellular function in flowering plants.}, author = {Walker, James and Gao, Hongbo and Zhang, Jingyi and Aldridge, Billy and Vickers, Martin and Higgins, James D. and Feng, Xiaoqi}, issn = {1546-1718}, journal = {Nature Genetics}, keywords = {Genetics}, number = {1}, pages = {130--137}, publisher = {Nature Research}, title = {{Sexual-lineage-specific DNA methylation regulates meiosis in Arabidopsis}}, doi = {10.1038/s41588-017-0008-5}, volume = {50}, year = {2017}, } @article{1228, abstract = {Since 2006, reprogrammed cells have increasingly been used as a biomedical research technique in addition to neuro-psychiatric methods. These rapidly evolving techniques allow for the generation of neuronal sub-populations, and have sparked interest not only in monogenetic neuro-psychiatric diseases, but also in poly-genetic and poly-aetiological disorders such as schizophrenia (SCZ) and bipolar disorder (BPD). This review provides a summary of 19 publications on reprogrammed adult somatic cells derived from patients with SCZ, and five publications using this technique in patients with BPD. As both disorders are complex and heterogeneous, there is a plurality of hypotheses to be tested in vitro. In SCZ, data on alterations of dopaminergic transmission in vitro are sparse, despite the great explanatory power of the so-called DA hypothesis of SCZ. Some findings correspond to perturbations of cell energy metabolism, and observations in reprogrammed cells suggest neuro-developmental alterations. Some studies also report on the efficacy of medicinal compounds to revert alterations observed in cellular models. However, due to the paucity of replication studies, no comprehensive conclusions can be drawn from studies using reprogrammed cells at the present time. In the future, findings from cell culture methods need to be integrated with clinical, epidemiological, pharmacological and imaging data in order to generate a more comprehensive picture of SCZ and BPD.}, author = {Sauerzopf, Ulrich and Sacco, Roberto and Novarino, Gaia and Niello, Marco and Weidenauer, Ana and Praschak Rieder, Nicole and Sitte, Harald and Willeit, Matthaeus}, journal = {European Journal of Neuroscience}, number = {1}, pages = {45 -- 57}, publisher = {Wiley-Blackwell}, title = {{Are reprogrammed cells a useful tool for studying dopamine dysfunction in psychotic disorders? A review of the current evidence}}, doi = {10.1111/ejn.13418}, volume = {45}, year = {2017}, } @article{123, abstract = {The Leidenfrost effect occurs when an object near a hot surface vaporizes rapidly enough to lift itself up and hover. Although well understood for liquids and stiff sublimable solids, nothing is known about the effect with materials whose stiffness lies between these extremes. Here we introduce a new phenomenon that occurs with vaporizable soft solids - the elastic Leidenfrost effect. By dropping hydrogel spheres onto hot surfaces we find that, rather than hovering, they energetically bounce several times their diameter for minutes at a time. With high-speed video during a single impact, we uncover high-frequency microscopic gap dynamics at the sphere/substrate interface. We show how these otherwise-hidden agitations constitute work cycles that harvest mechanical energy from the vapour and sustain the bouncing. Our findings suggest a new strategy for injecting mechanical energy into a widely used class of soft materials, with potential relevance to fields such as active matter, soft robotics and microfluidics.}, author = {Waitukaitis, Scott R and Zuiderwijk, Antal and Souslov, Anton and Coulais, Corentin and Van Hecke, Martin}, journal = {Nature Physics}, number = {11}, pages = {1095 -- 1099}, publisher = {Nature Publishing Group}, title = {{Coupling the Leidenfrost effect and elastic deformations to power sustained bouncing}}, doi = {10.1038/nphys4194}, volume = {13}, year = {2017}, } @inproceedings{12571, abstract = {We consider the problems of maintaining approximate maximum matching and minimum vertex cover in a dynamic graph. Starting with the seminal work of Onak and Rubinfeld [STOC 2010], this problem has received significant attention in recent years. Very recently, extending the framework of Baswana, Gupta and Sen [FOCS 2011], Solomon [FOCS 2016] gave a randomized 2-approximation dynamic algorithm for this problem that has amortized update time of O(1) with high probability. We consider the natural open question of derandomizing this result. We present a new deterministic fully dynamic algorithm that maintains a O(1)-approximate minimum vertex cover and maximum fractional matching, with an amortized update time of O(1). Previously, the best deterministic algorithm for this problem was due to Bhattacharya, Henzinger and Italiano [SODA 2015]; it had an approximation ratio of (2+ϵ) and an amortized update time of O(logn/ϵ2). Our result can be generalized to give a fully dynamic O(f3)-approximation algorithm with O(f2) amortized update time for the hypergraph vertex cover and fractional matching problems, where every hyperedge has at most f vertices.}, author = {Bhattacharya, Sayan and Chakrabarty, Deeparnab and Henzinger, Monika H}, booktitle = {19th International Conference on Integer Programming and Combinatorial Optimization}, isbn = {9783319592497}, issn = {0302-9743}, location = {Waterloo, ON, Canada}, pages = {86--98}, publisher = {Springer Nature}, title = {{Deterministic fully dynamic approximate vertex cover and fractional matching in O(1) amortized update time}}, doi = {10.1007/978-3-319-59250-3_8}, volume = {10328}, year = {2017}, } @article{12608, abstract = {The spatio-temporal distribution of air temperature over mountain glaciers can demonstrate complex patterns, yet it is often represented simplistically using linear vertical temperature gradients (VTGs) extrapolated from off-glacier locations. We analyse a network of centreline and lateral air temperature observations at Tsanteleina Glacier, Italy, during summer 2015. On average, VTGs are steep (<−0.0065 °C m−1), but they are shallow under warm ambient conditions when the correlation between air temperature and elevation becomes weaker. Published along-flowline temperature distribution methods explain centreline observations well, including warming on the lower glacier tongue, but cannot estimate lateral temperature variability. Application of temperature distribution methods improves simulation of melt rates (RMSE) in an energy-balance model by up to 36% compared to the environmental lapse rate extrapolated from an off-glacier station. However, results suggest that model parameters are not easily transferable to glaciers with a small fetch without recalibration. Such methods have potential to improve estimates of temperature across a glacier, but their parameter transferability should be further linked to the glacier and atmospheric characteristics. Furthermore, ‘cold spots’, which can be >2°C cooler than expected for their elevation, whose occurrence is not predicted by the temperature distribution models, are identified at one-quarter of the measurement sites.}, author = {SHAW, THOMAS E. and BROCK, BEN W. and AYALA, ÁLVARO and RUTTER, NICK and Pellicciotti, Francesca}, issn = {1727-5652}, journal = {Journal of Glaciology}, keywords = {Earth-Surface Processes}, number = {242}, pages = {973--988}, publisher = {Cambridge University Press}, title = {{Centreline and cross-glacier air temperature variability on an Alpine glacier: Assessing temperature distribution methods and their influence on melt model calculations}}, doi = {10.1017/jog.2017.65}, volume = {63}, year = {2017}, } @article{12609, abstract = {Previous estimates of melt and surface sublimation on glaciers of the subtropical semiarid Andes (29–34°S) have been obtained at few specific locations, but it is not clear how ablation components vary across the entire extent of a glacier in this dry environment. Here, we simulate the distributed energy and mass balance of Juncal Norte Glacier (33°S) during a 2-month summer period. Forcing fields of near-surface air temperature and wind speed are generated using two methods accounting for the main physical processes that shape their spatial variations. Simulated meteorological variables and ablation agree well with observations on the glacier tongue and reveal complex patterns of energy and mass fluxes. Ablation decreases from 70 mm w.e. d−1 at the low-albedo glacier terminus (~3000 m), where almost 100% of total ablation corresponds to melt, to <5 mm w.e. d−1 at wind-exposed, strong-radiated sites above 5500 m, where surface sublimation represents >75% of total ablation. Our simulations provide the first glacier-scale estimates of ablation components on a glacier in the study region and better reproduce the observed and expected spatial variations of melt and surface sublimation, in comparison with more simple assumptions, such as linear gradients and uniform wind speeds.}, author = {AYALA, A. and Pellicciotti, Francesca and PELEG, N. and BURLANDO, P.}, issn = {1727-5652}, journal = {Journal of Glaciology}, keywords = {Earth-Surface Processes}, number = {241}, pages = {803--822}, publisher = {Cambridge University Press}, title = {{Melt and surface sublimation across a glacier in a dry environment: distributed energy-balance modelling of Juncal Norte Glacier, Chile}}, doi = {10.1017/jog.2017.46}, volume = {63}, year = {2017}, } @article{12610, abstract = {The hydrological systems of heavily-downwasted debris-covered glaciers differ from those of clean-ice glaciers due to the hummocky surface and debris mantle of such glaciers, leading to a relatively limited understanding of drainage pathways. Supraglacial ponds represent sinks within the discontinuous supraglacial drainage system, and occasionally drain englacially. To assess pond dynamics, we made pond water level measurements on Lirung Glacier, Nepal, during May and October of 2013 and 2014. Simultaneously, aerial, satellite, and terrestrial orthoimages and digital elevation models were obtained, providing snapshots of the ponds and their surroundings. We performed a DEM-based analysis of the glacier's closed surface catchments to identify surface drainage pathways and englacial drainage points, and compared this to field observations of surface and near-surface water flow. The total ponded area was higher in the pre-monsoon than post-monsoon, with individual ponds filling and draining seasonally associated with the surface exposure of englacial conduit segments. We recorded four pond drainage events, all of which occurred gradually (duration of weeks), observed diurnal fluctuations indicative of varying water supply and outflow discharge, and we documented instances of interaction between distant ponds. The DEM drainage analysis identified numerous sinks >3 m in depth across the glacier surface, few of which exhibited ponds (23%), while the field survey highlighted instances of surface water only explicable via englacial routes. Taken together, our observations provide evidence for widespread supraglacial-englacial connectivity of meltwater drainage paths. Results suggest that successive englacial conduit collapse events, themselves likely driven by supraglacial pond drainage, cause the glacier surface drainage system to evolve into a configuration following relict englacial conduit systems. Within this system, ponds form in depressions of reduced drainage efficiency and link the supraglacial and englacial drainage networks.}, author = {Miles, Evan S. and Steiner, Jakob and Willis, Ian and Buri, Pascal and Immerzeel, Walter W. and Chesnokova, Anna and Pellicciotti, Francesca}, issn = {2296-6463}, journal = {Frontiers in Earth Science}, keywords = {General Earth and Planetary Sciences}, publisher = {Frontiers Media}, title = {{Pond dynamics and supraglacial-englacial connectivity on debris-covered Lirung Glacier, Nepal}}, doi = {10.3389/feart.2017.00069}, volume = {5}, year = {2017}, } @article{12611, abstract = {We investigate the energy balance and ablation regimes of glaciers in high-elevation, dry environments using glaciometeorological data collected on six glaciers in the semiarid Andes of North-Central Chile (29–34°S, 3127–5324 m). We use a point-scale physically based energy balance (EB) model and an enhanced Temperature-Index (ETI) model that calculates melt rates only as a function of air temperature and net shortwave radiation. At all sites, the largest energy inputs are net shortwave and incoming longwave radiation, which are controlled by surface albedo and elevation, respectively. Turbulent fluxes cancel each other out at the lower sites, but as elevation increases, cold, dry and wind-exposed conditions increase the magnitude of negative latent heat fluxes, associated with large surface sublimation rates. In midsummer (January), ablation rates vary from 67.9 mm w.e. d−1 at the lowest site (∼100% corresponding to melt), to 2.3 mm w.e. d−1 at the highest site (>85% corresponding to surface sublimation). At low-elevation, low-albedo, melt-dominated sites, the ETI model correctly reproduces melt using a large range of possible parameters, but both the performance and parameter transferability decrease with elevation for two main reasons: (i) the air temperature threshold approach for melt onset does not capture the diurnal variability of melt in cold and strong irradiated environments and (ii) energy losses decrease the correlation between melt and net shortwave radiation. We summarize our results by means of an elevation profile of ablation components that can be used as reference in future studies of glacier ablation in the semiarid Andes.}, author = {Ayala, A. and Pellicciotti, Francesca and MacDonell, S. and McPhee, J. and Burlando, P.}, issn = {0043-1397}, journal = {Water Resources Research}, keywords = {Water Science and Technology}, number = {7}, pages = {5601--5625}, publisher = {American Geophysical Union}, title = {{Patterns of glacier ablation across North-Central Chile: Identifying the limits of empirical melt models under sublimation-favorable conditions}}, doi = {10.1002/2016wr020126}, volume = {53}, year = {2017}, } @article{12612, abstract = {Supraglacial ponds play a key role in absorbing atmospheric energy and directing it to the ice of debris-covered glaciers, but the spatial and temporal distribution of these features is not well documented. We analyse 172 Landsat TM/ETM+ scenes for the period 1999–2013 to identify thawed supraglacial ponds for the debris-covered tongues of five glaciers in the Langtang Valley of Nepal. We apply an advanced atmospheric correction routine (Landcor/6S) and use band ratio and image morphological techniques to identify ponds and validate our results with 2.5 m Cartosat-1 observations. We then characterize the spatial, seasonal and interannual patterns of ponds. We find high variability in pond incidence between glaciers (May–October means of 0.08–1.69% of debris area), with ponds most frequent in zones of low surface gradient and velocity. The ponds show pronounced seasonality, appearing in the pre-monsoon as snow melts, peaking at the monsoon onset at 2% of debris-covered area, then declining in the post-monsoon as ponds drain or freeze. Ponds are highly recurrent and persistent, with 40.5% of pond locations occurring for multiple years. Rather than a trend in pond cover over the study period, we find high interannual variability for each glacier after controlling for seasonality.}, author = {MILES, EVAN S. and WILLIS, IAN C. and ARNOLD, NEIL S. and STEINER, JAKOB and Pellicciotti, Francesca}, issn = {1727-5652}, journal = {Journal of Glaciology}, keywords = {Earth-Surface Processes}, number = {237}, pages = {88--105}, publisher = {Cambridge University Press}, title = {{Spatial, seasonal and interannual variability of supraglacial ponds in the Langtang Valley of Nepal, 1999–2013}}, doi = {10.1017/jog.2016.120}, volume = {63}, year = {2017}, } @inproceedings{12905, author = {Schlögl, Alois and Kiss, Janos}, booktitle = {AHPC17 – Austrian HPC Meeting 2017}, location = {Grundlsee, Austria}, pages = {28}, publisher = {FSP Scientific Computing}, title = {{Scientific Computing at IST Austria}}, year = {2017}, } @article{1294, abstract = {We study controller synthesis problems for finite-state Markov decision processes, where the objective is to optimize the expected mean-payoff performance and stability (also known as variability in the literature). We argue that the basic notion of expressing the stability using the statistical variance of the mean payoff is sometimes insufficient, and propose an alternative definition. We show that a strategy ensuring both the expected mean payoff and the variance below given bounds requires randomization and memory, under both the above definitions. We then show that the problem of finding such a strategy can be expressed as a set of constraints.}, author = {Brázdil, Tomáš and Chatterjee, Krishnendu and Forejt, Vojtěch and Kučera, Antonín}, journal = {Journal of Computer and System Sciences}, pages = {144 -- 170}, publisher = {Elsevier}, title = {{Trading performance for stability in Markov decision processes}}, doi = {10.1016/j.jcss.2016.09.009}, volume = {84}, year = {2017}, } @inproceedings{13160, abstract = {Transforming deterministic ω -automata into deterministic parity automata is traditionally done using variants of appearance records. We present a more efficient variant of this approach, tailored to Rabin automata, and several optimizations applicable to all appearance records. We compare the methods experimentally and find out that our method produces smaller automata than previous approaches. Moreover, the experiments demonstrate the potential of our method for LTL synthesis, using LTL-to-Rabin translators. It leads to significantly smaller parity automata when compared to state-of-the-art approaches on complex formulae.}, author = {Kretinsky, Jan and Meggendorfer, Tobias and Waldmann, Clara and Weininger, Maximilian}, booktitle = {Tools and Algorithms for the Construction and Analysis of Systems}, isbn = {9783662545768}, issn = {1611-3349}, location = {Uppsala, Sweden}, pages = {443--460}, publisher = {Springer}, title = {{Index appearance record for transforming Rabin automata into parity automata}}, doi = {10.1007/978-3-662-54577-5_26}, volume = {10205}, year = {2017}, } @article{1336, abstract = {Evolutionary algorithms (EAs) form a popular optimisation paradigm inspired by natural evolution. In recent years the field of evolutionary computation has developed a rigorous analytical theory to analyse the runtimes of EAs on many illustrative problems. Here we apply this theory to a simple model of natural evolution. In the Strong Selection Weak Mutation (SSWM) evolutionary regime the time between occurrences of new mutations is much longer than the time it takes for a mutated genotype to take over the population. In this situation, the population only contains copies of one genotype and evolution can be modelled as a stochastic process evolving one genotype by means of mutation and selection between the resident and the mutated genotype. The probability of accepting the mutated genotype then depends on the change in fitness. We study this process, SSWM, from an algorithmic perspective, quantifying its expected optimisation time for various parameters and investigating differences to a similar evolutionary algorithm, the well-known (1+1) EA. We show that SSWM can have a moderate advantage over the (1+1) EA at crossing fitness valleys and study an example where SSWM outperforms the (1+1) EA by taking advantage of information on the fitness gradient.}, author = {Paixao, Tiago and Pérez Heredia, Jorge and Sudholt, Dirk and Trubenova, Barbora}, issn = {0178-4617}, journal = {Algorithmica}, number = {2}, pages = {681 -- 713}, publisher = {Springer}, title = {{Towards a runtime comparison of natural and artificial evolution}}, doi = {10.1007/s00453-016-0212-1}, volume = {78}, year = {2017}, } @article{1337, abstract = {We consider the local eigenvalue distribution of large self-adjoint N×N random matrices H=H∗ with centered independent entries. In contrast to previous works the matrix of variances sij=\mathbbmE|hij|2 is not assumed to be stochastic. Hence the density of states is not the Wigner semicircle law. Its possible shapes are described in the companion paper (Ajanki et al. in Quadratic Vector Equations on the Complex Upper Half Plane. arXiv:1506.05095). We show that as N grows, the resolvent, G(z)=(H−z)−1, converges to a diagonal matrix, diag(m(z)), where m(z)=(m1(z),…,mN(z)) solves the vector equation −1/mi(z)=z+∑jsijmj(z) that has been analyzed in Ajanki et al. (Quadratic Vector Equations on the Complex Upper Half Plane. arXiv:1506.05095). We prove a local law down to the smallest spectral resolution scale, and bulk universality for both real symmetric and complex hermitian symmetry classes.}, author = {Ajanki, Oskari H and Erdös, László and Krüger, Torben H}, issn = {0178-8051}, journal = {Probability Theory and Related Fields}, number = {3-4}, pages = {667 -- 727}, publisher = {Springer}, title = {{Universality for general Wigner-type matrices}}, doi = {10.1007/s00440-016-0740-2}, volume = {169}, year = {2017}, } @article{1338, abstract = {We present a computer-aided programming approach to concurrency. The approach allows programmers to program assuming a friendly, non-preemptive scheduler, and our synthesis procedure inserts synchronization to ensure that the final program works even with a preemptive scheduler. The correctness specification is implicit, inferred from the non-preemptive behavior. Let us consider sequences of calls that the program makes to an external interface. The specification requires that any such sequence produced under a preemptive scheduler should be included in the set of sequences produced under a non-preemptive scheduler. We guarantee that our synthesis does not introduce deadlocks and that the synchronization inserted is optimal w.r.t. a given objective function. The solution is based on a finitary abstraction, an algorithm for bounded language inclusion modulo an independence relation, and generation of a set of global constraints over synchronization placements. Each model of the global constraints set corresponds to a correctness-ensuring synchronization placement. The placement that is optimal w.r.t. the given objective function is chosen as the synchronization solution. We apply the approach to device-driver programming, where the driver threads call the software interface of the device and the API provided by the operating system. Our experiments demonstrate that our synthesis method is precise and efficient. The implicit specification helped us find one concurrency bug previously missed when model-checking using an explicit, user-provided specification. We implemented objective functions for coarse-grained and fine-grained locking and observed that different synchronization placements are produced for our experiments, favoring a minimal number of synchronization operations or maximum concurrency, respectively.}, author = {Cerny, Pavol and Clarke, Edmund and Henzinger, Thomas A and Radhakrishna, Arjun and Ryzhyk, Leonid and Samanta, Roopsha and Tarrach, Thorsten}, journal = {Formal Methods in System Design}, number = {2-3}, pages = {97 -- 139}, publisher = {Springer}, title = {{From non-preemptive to preemptive scheduling using synchronization synthesis}}, doi = {10.1007/s10703-016-0256-5}, volume = {50}, year = {2017}, } @article{13380, abstract = {Although dissipative self-assembly is ubiquitous in nature, where it gives rise to structures and functions critical to life, examples of artificial systems featuring this mode of self-assembly are rare. Here, we identify the presence of ephemeral assemblies during seeded growth of gold nanoparticles. In this process, hydrazine reduces Au(III) ions, which attach to the existing nanoparticles “seeds”. The attachment is accompanied by a local increase in the concentration of a surfactant, which therefore forms a bilayer on nanoparticle surfaces, inducing their assembly. The resulting aggregates gradually disassemble as the surfactant concentration throughout the solution equilibrates. The lifetimes of the out-of-equilibrium aggregates depend on and can be controlled by the size of the constituent nanoparticles. We demonstrate the utility of our out-of-equilibrium aggregates to form transient reflective coatings on polar surfaces.}, author = {Sawczyk, Michał and Klajn, Rafal}, issn = {1520-5126}, journal = {Journal of the American Chemical Society}, keywords = {Colloid and Surface Chemistry, Biochemistry, General Chemistry, Catalysis}, number = {49}, pages = {17973--17978}, publisher = {American Chemical Society}, title = {{Out-of-equilibrium aggregates and coatings during seeded growth of metallic nanoparticles}}, doi = {10.1021/jacs.7b09111}, volume = {139}, year = {2017}, }