@article{12632,
  abstract     = {We investigate the performance of five glacier melt models over a multi-decadal period in order to assess their ability to model future glacier response. The models range from a simple degree-day model, based solely on air temperature, to more-sophisticated models, including the full shortwave radiation balance. In addition to the empirical models, the performance of a physically based energy-balance (EB) model is examined. The melt models are coupled to an accumulation and a surface evolution model and applied in a distributed manner to Rhonegletscher, Switzerland, over the period 1929–2012 at hourly resolution. For calibration, seasonal mass-balance measurements (2006–12) are used. Decadal ice volume changes for six periods in the years 1929–2012 serve for model validation. Over the period 2006–12, there are almost no differences in performance between the models, except for EB, which is less consistent with observations, likely due to lack of meteorological in situ data. However, simulations over the long term (1929–2012) reveal that models which include a separate term for shortwave radiation agree best with the observed ice volume changes, indicating that their melt relationships are robust in time and thus suitable for long-term modelling, in contrast to more empirical approaches that are oversensitive to temperature fluctuations.},
  author       = {Gabbi, Jeannette and Carenzo, Marco and Pellicciotti, Francesca and Bauder, Andreas and Funk, Martin},
  issn         = {1727-5652},
  journal      = {Journal of Glaciology},
  keywords     = {Earth-Surface Processes},
  number       = {224},
  pages        = {1140--1154},
  publisher    = {International Glaciological Society},
  title        = {{A comparison of empirical and physically based glacier surface melt models for long-term simulations of glacier response}},
  doi          = {10.3189/2014jog14j011},
  volume       = {60},
  year         = {2014},
}

@article{12637,
  abstract     = {The performance of glaciohydrological models which simulate catchment response to climate variability depends to a large degree on the data used to force the models. The forcing data become increasingly important in high-elevation, glacierized catchments where the interplay between extreme topography, climate, and the cryosphere is complex. It is challenging to generate a reliable forcing data set that captures this spatial heterogeneity. In this paper, we analyze the results of a 1 year field campaign focusing on air temperature and precipitation observations in the Langtang valley in the Nepalese Himalayas. We use the observed time series to characterize both temperature lapse rates (LRs) and precipitation gradients (PGs). We study their spatial and temporal variability, and we attempt to identify possible controlling factors. We show that very clear LRs exist in the valley and that there are strong seasonal differences related to the water vapor content in the atmosphere. Results also show that the LRs are generally shallower than the commonly used environmental lapse rates. The analysis of the precipitation observations reveals that there is great variability in precipitation over short horizontal distances. A uniform valley wide PG cannot be established, and several scale-dependent mechanisms may explain our observations. We complete our analysis by showing the impact of the observed LRs and PGs on the outputs of the TOPKAPI-ETH glaciohydrological model. We conclude that LRs and PGs have a very large impact on the water balance composition and that short-term monitoring campaigns have the potential to improve model quality considerably.},
  author       = {Immerzeel, W. W. and Petersen, L. and Ragettli, S. and Pellicciotti, Francesca},
  issn         = {1944-7973},
  journal      = {Water Resources Research},
  keywords     = {Water Science and Technology},
  number       = {3},
  pages        = {2212--2226},
  publisher    = {American Geophysical Union},
  title        = {{The importance of observed gradients of air temperature and precipitation for modeling runoff from a glacierized watershed in the Nepalese Himalayas}},
  doi          = {10.1002/2013wr014506},
  volume       = {50},
  year         = {2014},
}

@article{97,
  abstract     = {The distribution of Coulomb blockade peak heights as a function of magnetic field is investigated experimentally in a Ge-Si nanowire quantum dot. Strong spin-orbit coupling in this hole-gas system leads to antilocalization of Coulomb blockade peaks, consistent with theory. In particular, the peak height distribution has its maximum away from zero at zero magnetic field, with an average that decreases with increasing field. Magnetoconductance in the open-wire regime places a bound on the spin-orbit length (lso < 20 nm), consistent with values extracted in the Coulomb blockade regime (lso < 25 nm).},
  author       = {Higginbotham, Andrew P and Kuemmeth, Ferdinand and Larsen, Thorvald and Fitzpatrick, Mattias and Yao, Jun and Yan, Hao and Lieber, Charles and Marcus, Charles},
  journal      = {APS Physics, Physical Review Letters},
  number       = {21},
  publisher    = {American Physical Society},
  title        = {{Antilocalization of coulomb blockade in a Ge/Si nanowire}},
  doi          = {10.1103/PhysRevLett.112.216806},
  volume       = {112},
  year         = {2014},
}

@misc{9740,
  abstract     = {The fitness effects of symbionts on their hosts can be context-dependent, with usually benign symbionts causing detrimental effects when their hosts are stressed, or typically parasitic symbionts providing protection towards their hosts (e.g. against pathogen infection). Here, we studied the novel association between the invasive garden ant Lasius neglectus and its fungal ectosymbiont Laboulbenia formicarum for potential costs and benefits. We tested ants with different Laboulbenia levels for their survival and immunity under resource limitation and exposure to the obligate killing entomopathogen Metarhizium brunneum. While survival of L. neglectus workers under starvation was significantly decreased with increasing Laboulbenia levels, host survival under Metarhizium exposure increased with higher levels of the ectosymbiont, suggesting a symbiont-mediated anti-pathogen protection, which seems to be driven mechanistically by both improved sanitary behaviours and an upregulated immune system. Ants with high Laboulbenia levels showed significantly longer self-grooming and elevated expression of immune genes relevant for wound repair and antifungal responses (β-1,3-glucan binding protein, Prophenoloxidase), compared with ants carrying low Laboulbenia levels. This suggests that the ectosymbiont Laboulbenia formicarum weakens its ant host by either direct resource exploitation or the costs of an upregulated behavioural and immunological response, which, however, provides a prophylactic protection upon later exposure to pathogens.},
  author       = {Konrad, Matthias and Grasse, Anna V and Tragust, Simon and Cremer, Sylvia},
  publisher    = {Dryad},
  title        = {{Data from: Anti-pathogen protection versus survival costs mediated by an ectosymbiont in an ant host}},
  doi          = {10.5061/dryad.vm0vc},
  year         = {2014},
}

@misc{9741,
  abstract     = {In rapidly changing environments, selection history may impact the dynamics of adaptation. Mutations selected in one environment may result in pleiotropic fitness trade-offs in subsequent novel environments, slowing the rates of adaptation. Epistatic interactions between mutations selected in sequential stressful environments may slow or accelerate subsequent rates of adaptation, depending on the nature of that interaction. We explored the dynamics of adaptation during sequential exposure to herbicides with different modes of action in Chlamydomonas reinhardtii. Evolution of resistance to two of the herbicides was largely independent of selection history. For carbetamide, previous adaptation to other herbicide modes of action positively impacted the likelihood of adaptation to this herbicide. Furthermore, while adaptation to all individual herbicides was associated with pleiotropic fitness costs in stress-free environments, we observed that accumulation of resistance mechanisms was accompanied by a reduction in overall fitness costs. We suggest that antagonistic epistasis may be a driving mechanism that enables populations to more readily adapt in novel environments. These findings highlight the potential for sequences of xenobiotics to facilitate the rapid evolution of multiple-drug and -pesticide resistance, as well as the potential for epistatic interactions between adaptive mutations to facilitate evolutionary rescue in rapidly changing environments.},
  author       = {Lagator, Mato and Colegrave, Nick and Neve, Paul},
  publisher    = {Dryad},
  title        = {{Data from: Selection history and epistatic interactions impact dynamics of adaptation to novel environmental stresses}},
  doi          = {10.5061/dryad.85dn7},
  year         = {2014},
}

@misc{9747,
  abstract     = {Understanding the effects of sex and migration on adaptation to novel environments remains a key problem in evolutionary biology. Using a single-cell alga Chlamydomonas reinhardtii, we investigated how sex and migration affected rates of evolutionary rescue in a sink environment, and subsequent changes in fitness following evolutionary rescue. We show that sex and migration affect both the rate of evolutionary rescue and subsequent adaptation. However, their combined effects change as the populations adapt to a sink habitat. Both sex and migration independently increased rates of evolutionary rescue, but the effect of sex on subsequent fitness improvements, following initial rescue, changed with migration, as sex was beneficial in the absence of migration but constraining adaptation when combined with migration. These results suggest that sex and migration are beneficial during the initial stages of adaptation, but can become detrimental as the population adapts to its environment.},
  author       = {Lagator, Mato and Morgan, Andrew and Neve, Paul and Colegrave, Nick},
  publisher    = {Dryad},
  title        = {{Data from: Role of sex and migration in adaptation to sink environments}},
  doi          = {10.5061/dryad.s42n1},
  year         = {2014},
}

@misc{9752,
  abstract     = {Redundancies and correlations in the responses of sensory neurons may seem to waste neural resources, but they can also carry cues about structured stimuli and may help the brain to correct for response errors. To investigate the effect of stimulus structure on redundancy in retina, we measured simultaneous responses from populations of retinal ganglion cells presented with natural and artificial stimuli that varied greatly in correlation structure; these stimuli and recordings are publicly available online. Responding to spatio-temporally structured stimuli such as natural movies, pairs of ganglion cells were modestly more correlated than in response to white noise checkerboards, but they were much less correlated than predicted by a non-adapting functional model of retinal response. Meanwhile, responding to stimuli with purely spatial correlations, pairs of ganglion cells showed increased correlations consistent with a static, non-adapting receptive field and nonlinearity. We found that in response to spatio-temporally correlated stimuli, ganglion cells had faster temporal kernels and tended to have stronger surrounds. These properties of individual cells, along with gain changes that opposed changes in effective contrast at the ganglion cell input, largely explained the pattern of pairwise correlations across stimuli where receptive field measurements were possible.},
  author       = {Simmons, Kristina and Prentice, Jason and Tkačik, Gašper and Homann, Jan and Yee, Heather and Palmer, Stephanie and Nelson, Philip and Balasubramanian, Vijay},
  publisher    = {Dryad},
  title        = {{Data from: Transformation of stimulus correlations by the retina}},
  doi          = {10.5061/dryad.246qg},
  year         = {2014},
}

@misc{9753,
  abstract     = {Background: The brood of ants and other social insects is highly susceptible to pathogens, particularly those that penetrate the soft larval and pupal cuticle. We here test whether the presence of a pupal cocoon, which occurs in some ant species but not in others, affects the sanitary brood care and fungal infection patterns after exposure to the entomopathogenic fungus Metarhizium brunneum. We use a) a comparative approach analysing four species with either naked or cocooned pupae and b) a within-species analysis of a single ant species, in which both pupal types co-exist in the same colony. Results: We found that the presence of a cocoon did not compromise fungal pathogen detection by the ants and that species with cocooned pupae increased brood grooming after pathogen exposure. All tested ant species further removed brood from their nests, which was predominantly expressed towards larvae and naked pupae treated with the live fungal pathogen. In contrast, cocooned pupae exposed to live fungus were not removed at higher rates than cocooned pupae exposed to dead fungus or a sham control. Consistent with this, exposure to the live fungus caused high numbers of infections and fungal outgrowth in larvae and naked pupae, but not in cocooned pupae. Moreover, the ants consistently removed the brood prior to fungal outgrowth, ensuring a clean brood chamber. Conclusion: Our study suggests that the pupal cocoon has a protective effect against fungal infection, causing an adaptive change in sanitary behaviours by the ants. It further demonstrates that brood removal - originally described for honeybees as “hygienic behaviour” – is a widespread sanitary behaviour in ants, which likely has important implications on disease dynamics in social insect colonies.},
  author       = {Tragust, Simon and Ugelvig, Line V and Chapuisat, Michel and Heinze, Jürgen and Cremer, Sylvia},
  publisher    = {Dryad},
  title        = {{Data from: Pupal cocoons affect sanitary brood care and limit fungal infections in ant colonies}},
  doi          = {10.5061/dryad.nc0gc},
  year         = {2014},
}

@article{977,
  abstract     = {We propose a method for detecting many-body localization (MBL) in disordered spin systems. The method involves pulsed coherent spin manipulations that probe the dephasing of a given spin due to its entanglement with a set of distant spins. It allows one to distinguish the MBL phase from a noninteracting localized phase and a delocalized phase. In particular, we show that for a properly chosen pulse sequence the MBL phase exhibits a characteristic power-law decay reflecting its slow growth of entanglement. We find that this power-law decay is robust with respect to thermal and disorder averaging, provide numerical simulations supporting our results, and discuss possible experimental realizations in solid-state and cold-atom systems.},
  author       = {Maksym Serbyn and Knap, Michael J and Gopalakrishnan, Sarang and Papić, Zlatko and Yao, Norman Y and Laumann, Chris R and Abanin, Dmitry A and Lukin, Mikhail D and Demler, Eugene A},
  journal      = {Physical Review Letters},
  number       = {14},
  publisher    = {American Physical Society},
  title        = {{Interferometric probes of many-body localization}},
  doi          = {10.1103/PhysRevLett.113.147204},
  volume       = {113},
  year         = {2014},
}

@article{978,
  abstract     = {The newly discovered topological crystalline insulators feature a complex band structure involving multiple Dirac cones, and are potentially highly tunable by external electric field, temperature or strain. Theoretically, it has been predicted that the various Dirac cones, which are offset in energy and momentum, might harbour vastly different orbital character. However, their orbital texture, which is of immense importance in determining a variety of a materialâ €™ s properties remains elusive. Here, we unveil the orbital texture of Pb 1â ̂'x Sn x Se, a prototypical topological crystalline insulator. By using Fourier-transform scanning tunnelling spectroscopy we measure the interference patterns produced by the scattering of surface-state electrons. We discover that the intensity and energy dependences of the Fourier transforms show distinct characteristics, which can be directly attributed to orbital effects. Our experiments reveal a complex band topology involving two Lifshitz transitions and establish the orbital nature of the Dirac bands, which could provide an alternative pathway towards future quantum applications.},
  author       = {Zeljkovic, Ilija and Okada, Yoshinori and Huang, Chengyi and Sankar, Raman and Walkup, Daniel and Zhou, Wenwen and Maksym Serbyn and Chou, Fangcheng and Tsai, Wei-Feng and Lin, Hsin and Bansil, Arun and Fu, Liang and Hasan, Md Z and Madhavan, Vidya},
  journal      = {Nature Physics},
  number       = {8},
  pages        = {572 -- 577},
  publisher    = {Nature Publishing Group},
  title        = {{Mapping the unconventional orbital texture in topological crystalline insulators}},
  doi          = {10.1038/nphys3012},
  volume       = {10},
  year         = {2014},
}

@article{979,
  abstract     = {In the recently discovered topological crystalline insulators SnTe and Pb1-xSnx(Te, Se), crystal symmetry and electronic topology intertwine to create topological surface states with many interesting features including Lifshitz transition, Van-Hove singularity, and fermion mass generation. These surface states are protected by mirror symmetry with respect to the (110) plane. In this work we present a comprehensive study of the effects of different mirror-symmetry-breaking perturbations on the (001) surface band structure. Pristine (001) surface states have four branches of Dirac fermions at low energy. We show that ferroelectric-type structural distortion generates a mass and gaps out some or all of these Dirac points, while strain shifts Dirac points in the Brillouin zone. An in-plane magnetic field leaves the surface state gapless, but introduces asymmetry between Dirac points. Finally, an out-of-plane magnetic field leads to discrete Landau levels. We show that the Landau level spectrum has an unusual pattern of degeneracy and interesting features due to the unique underlying band structure. This suggests that Landau level spectroscopy can detect and distinguish between different mechanisms of symmetry breaking in topological crystalline insulators.},
  author       = {Maksym Serbyn and Fu, Liang},
  journal      = {Physical Review B - Condensed Matter and Materials Physics},
  number       = {3},
  publisher    = {American Physical Society},
  title        = {{Symmetry breaking and Landau quantization in topological crystalline insulators}},
  doi          = {10.1103/PhysRevB.90.035402},
  volume       = {90},
  year         = {2014},
}

@article{98,
  abstract     = {Relaxation and dephasing of hole spins are measured in a gate-defined Ge/Si nanowire double quantum dot using a fast pulsed-gate method and dispersive readout. An inhomogeneous dephasing time T2* ∼ 0.18 μs exceeds corresponding measurements in III-V semiconductors by more than an order of magnitude, as expected for predominately nuclear-spin-free materials. Dephasing is observed to be exponential in time, indicating the presence of a broadband noise source, rather than Gaussian, previously seen in systems with nuclear-spin-dominated dephasing.},
  author       = {Higginbotham, Andrew P and Larsen, Thorvald and Yao, Jun and Yan, Hao and Lieber, Charles and Marcus, Charles and Kuemmeth, Ferdinand},
  journal      = {Nano Letters},
  number       = {6},
  pages        = {3582 -- 3586},
  publisher    = {American Chemical Society},
  title        = {{Hole spin coherence in a Ge/Si heterostructure nanowire}},
  doi          = {10.1021/nl501242b},
  volume       = {14},
  year         = {2014},
}

@article{980,
  abstract     = {Many-body localized (MBL) systems are characterized by the absence of transport and thermalization and, therefore, cannot be described by conventional statistical mechanics. In this paper, using analytic arguments and numerical simulations, we study the behavior of local observables in an isolated MBL system following a quantum quench. For the case of a global quench, we find that the local observables reach stationary, highly nonthermal values at long times as a result of slow dephasing characteristic of the MBL phase. These stationary values retain the local memory of the initial state due to the existence of local integrals of motion in the MBL phase. The temporal fluctuations around stationary values exhibit universal power-law decay in time, with an exponent set by the localization length and the diagonal entropy of the initial state. Such a power-law decay holds for any local observable and is related to the logarithmic in time growth of entanglement in the MBL phase. This behavior distinguishes the MBL phase from both the Anderson insulator (where no stationary state is reached) and from the ergodic phase (where relaxation is expected to be exponential). For the case of a local quench, we also find a power-law approach of local observables to their stationary values when the system is prepared in a mixed state. Quench protocols considered in this paper can be naturally implemented in systems of ultracold atoms in disordered optical lattices, and the behavior of local observables provides a direct experimental signature of many-body localization.},
  author       = {Maksym Serbyn and Papić, Zlatko and Abanin, Dmitry A},
  journal      = {Physical Review B - Condensed Matter and Materials Physics},
  number       = {17},
  publisher    = {American Physical Society},
  title        = {{Quantum quenches in the many-body localized phase}},
  doi          = {10.1103/PhysRevB.90.174302},
  volume       = {90},
  year         = {2014},
}

@misc{9932,
  abstract     = {Gene duplication is important in evolution, because it provides new raw material for evolutionary adaptations. Several existing hypotheses about the causes of duplicate retention and diversification differ in their emphasis on gene dosage, sub-functionalization, and neo-functionalization. Little experimental data exists on the relative importance of gene expression changes and changes in coding regions for the evolution of duplicate genes. Furthermore, we do not know how strongly the environment could affect this importance. To address these questions, we performed evolution experiments with the TEM-1 beta lactamase gene in E. coli to study the initial stages of duplicate gene evolution in the laboratory. We mimicked tandem duplication by inserting two copies of the TEM-1 gene on the same plasmid. We then subjected these copies to repeated cycles of mutagenesis and selection in various environments that contained antibiotics in different combinations and concentrations. Our experiments showed that gene dosage is the most important factor in the initial stages of duplicate gene evolution, and overshadows the importance of point mutations in the coding region.},
  author       = {Dhar, Riddhiman and Bergmiller, Tobias and Wagner, Andreas},
  publisher    = {Dryad},
  title        = {{Data from: Increased gene dosage plays a predominant role in the initial stages of evolution of duplicate TEM-1 beta lactamase genes}},
  doi          = {10.5061/dryad.jc402},
  year         = {2014},
}

@article{350,
  abstract     = {Herein, a colloidal synthetic route to produce highly monodisperse Cu2HgGeSe4 (CHGSe) nanoparticles (NPs) is presented in detail. The high yield of the developed procedure allowed the production of CHGSe NPs at the gram scale. A thorough analysis of their structural and optical properties is shown. CHGSe NPs displayed poly-tetrahedral morphology and narrow size distributions with average size in the range of 10–40 nm and size dispersions below 10 %. A 1.6 eV optical band gap was measured by mean of UV–Vis. By adjusting the cation ratio, an effective control of their electrical conductivity is achieved. The prepared NPs are used as building blocks for the production of CHGSe bulk nanostructured materials. The thermoelectric properties of CHGSe nanomaterials are studied in the temperature range from 300 to 730 K. CHGSe nanomaterials reached electrical conductivities up to 5 × 104 S m−1, Seebeck coefficients above 100 μV K−1, and thermal conductivities below 1.0 W m−1 K−1 which translated into thermoelectric figures of merit up to 0.34 at 730 K.},
  author       = {Li, Wenhua and Ibáñez, Maria and Cadavid, Doris and Zamani, Reza and Rubio Garcia, Javier and Gorsse, Stéphane and Morante, Joan and Arbiol, Jordi and Cabot, Andreu},
  journal      = {Journal of Nanoparticle Research},
  number       = {3},
  publisher    = {Kluwer},
  title        = {{Colloidal synthesis and functional properties of quaternary Cu based semiconductors: Cu2HgGeSe4}},
  doi          = {10.1007/s11051-014-2297-2},
  volume       = {16},
  year         = {2014},
}

@article{451,
  abstract     = {We introduce algorithms for the computation of homology, cohomology, and related operations on cubical cell complexes, using the technique based on a chain contraction from the original chain complex to a reduced one that represents its homology. This work is based on previous results for simplicial complexes, and uses Serre’s diagonalization for cubical cells. An implementation in C++ of the introduced algorithms is available at http://www.pawelpilarczyk.com/chaincon/ together with some examples. The paper is self-contained as much as possible, and is written at a very elementary level, so that basic knowledge of algebraic topology should be sufficient to follow it.},
  author       = {Pawel Pilarczyk and Real, Pedro},
  journal      = {Advances in Computational Mathematics},
  number       = {1},
  pages        = {253 -- 275},
  publisher    = {Kluwer},
  title        = {{Computation of cubical homology, cohomology, and (co)homological operations via chain contraction}},
  doi          = {10.1007/s10444-014-9356-1},
  volume       = {41},
  year         = {2014},
}

@article{2443,
  abstract     = {The mode of action of auxin is based on its non-uniform distribution within tissues and organs. Despite the wide use of several auxin analogues in research and agriculture, little is known about the specificity of different auxin-related transport and signalling processes towards these compounds. Using seedlings of Arabidopsis thaliana and suspension-cultured cells of Nicotiana tabacum (BY-2), the physiological activity of several auxin analogues was investigated, together with their capacity to induce auxin-dependent gene expression, to inhibit endocytosis and to be transported across the plasma membrane. This study shows that the specificity criteria for different auxin-related processes vary widely. Notably, the special behaviour of some synthetic auxin analogues suggests that they might be useful tools in investigations of the molecular mechanism of auxin action. Thus, due to their differential stimulatory effects on DR5 expression, indole-3-propionic (IPA) and 2,4,5-trichlorophenoxy acetic (2,4,5-T) acids can serve in studies of TRANSPORT INHIBITOR RESPONSE 1/AUXIN SIGNALLING F-BOX (TIR1/AFB)-mediated auxin signalling, and 5-fluoroindole-3-acetic acid (5-F-IAA) can help to discriminate between transcriptional and non-transcriptional pathways of auxin signalling. The results demonstrate that the major determinants for the auxin-like physiological potential of a particular compound are very complex and involve its chemical and metabolic stability, its ability to distribute in tissues in a polar manner and its activity towards auxin signalling machinery.},
  author       = {Simon, Sibu and Kubeš, Martin and Baster, Pawel and Robert, Stéphanie and Dobrev, Petre and Friml, Jirí and Petrášek, Jan and Zažímalová, Eva},
  journal      = {New Phytologist},
  number       = {4},
  pages        = {1034 -- 1048},
  publisher    = {Wiley},
  title        = {{Defining the selectivity of processes along the auxin response chain: A study using auxin analogues}},
  doi          = {10.1111/nph.12437},
  volume       = {200},
  year         = {2013},
}

@inproceedings{2444,
  abstract     = {We consider two core algorithmic problems for probabilistic verification: the maximal end-component decomposition and the almost-sure reachability set computation for Markov decision processes (MDPs). For MDPs with treewidth k, we present two improved static algorithms for both the problems that run in time O(n·k 2.38·2k ) and O(m·logn· k), respectively, where n is the number of states and m is the number of edges, significantly improving the previous known O(n·k·√n· k) bound for low treewidth. We also present decremental algorithms for both problems for MDPs with constant treewidth that run in amortized logarithmic time, which is a huge improvement over the previously known algorithms that require amortized linear time.},
  author       = {Chatterjee, Krishnendu and Ła̧Cki, Jakub},
  location     = {St. Petersburg, Russia},
  pages        = {543 -- 558},
  publisher    = {Springer},
  title        = {{Faster algorithms for Markov decision processes with low treewidth}},
  doi          = {10.1007/978-3-642-39799-8_36},
  volume       = {8044},
  year         = {2013},
}

@inproceedings{2445,
  abstract     = {We develop program synthesis techniques that can help programmers fix concurrency-related bugs. We make two new contributions to synthesis for concurrency, the first improving the efficiency of the synthesized code, and the second improving the efficiency of the synthesis procedure itself. The first contribution is to have the synthesis procedure explore a variety of (sequential) semantics-preserving program transformations. Classically, only one such transformation has been considered, namely, the insertion of synchronization primitives (such as locks). Based on common manual bug-fixing techniques used by Linux device-driver developers, we explore additional, more efficient transformations, such as the reordering of independent instructions. The second contribution is to speed up the counterexample-guided removal of concurrency bugs within the synthesis procedure by considering partial-order traces (instead of linear traces) as counterexamples. A partial-order error trace represents a set of linear (interleaved) traces of a concurrent program all of which lead to the same error. By eliminating a partial-order error trace, we eliminate in a single iteration of the synthesis procedure all linearizations of the partial-order trace. We evaluated our techniques on several simplified examples of real concurrency bugs that occurred in Linux device drivers.},
  author       = {Cerny, Pavol and Henzinger, Thomas A and Radhakrishna, Arjun and Ryzhyk, Leonid and Tarrach, Thorsten},
  location     = {St. Petersburg, Russia},
  pages        = {951 -- 967},
  publisher    = {Springer},
  title        = {{Efficient synthesis for concurrency by semantics-preserving transformations}},
  doi          = {10.1007/978-3-642-39799-8_68},
  volume       = {8044},
  year         = {2013},
}

@inproceedings{2446,
  abstract     = {The model-checking problem for probabilistic systems crucially relies on the translation of LTL to deterministic Rabin automata (DRW). Our recent Safraless translation [KE12, GKE12] for the LTL(F,G) fragment produces smaller automata as compared to the traditional approach. In this work, instead of DRW we consider deterministic automata with acceptance condition given as disjunction of generalized Rabin pairs (DGRW). The Safraless translation of LTL(F,G) formulas to DGRW results in smaller automata as compared to DRW. We present algorithms for probabilistic model-checking as well as game solving for DGRW conditions. Our new algorithms lead to improvement both in terms of theoretical bounds as well as practical evaluation. We compare PRISM with and without our new translation, and show that the new translation leads to significant improvements.},
  author       = {Chatterjee, Krishnendu and Gaiser, Andreas and Kretinsky, Jan},
  location     = {St. Petersburg, Russia},
  pages        = {559 -- 575},
  publisher    = {Springer},
  title        = {{Automata with generalized Rabin pairs for probabilistic model checking and LTL synthesis}},
  doi          = {10.1007/978-3-642-39799-8_37},
  volume       = {8044},
  year         = {2013},
}