@inproceedings{4384,
abstract = {Model checking software transactional memories (STMs) is difficult because of the unbounded number, length, and delay of concurrent transactions and the unbounded size of the memory. We show that, under certain conditions, the verification problem can be reduced to a finite-state problem, and we illustrate the use of the method by proving the correctness of several STMs, including two-phase locking, DSTM, TL2, and optimistic concurrency control. The safety properties we consider include strict serializability and opacity; the liveness properties include obstruction freedom, livelock freedom, and wait freedom.
Our main contribution lies in the structure of the proofs, which are largely automated and not restricted to the STMs mentioned above. In a first step we show that every STM that enjoys certain structural properties either violates a safety or liveness requirement on some program with two threads and two shared variables, or satisfies the requirement on all programs. In the second step we use a model checker to prove the requirement for the STM applied to a most general program with two threads and two variables. In the safety case, the model checker constructs a simulation relation between two carefully constructed finite-state transition systems, one representing the given STM applied to a most general program, and the other representing a most liberal safe STM applied to the same program. In the liveness case, the model checker analyzes fairness conditions on the given STM transition system.},
author = {Guerraoui, Rachid and Thomas Henzinger and Jobstmann, Barbara and Vasu Singh},
pages = {372 -- 382},
publisher = {ACM},
title = {{Model checking transactional memories}},
doi = {10.1145/1375581.1375626},
year = {2008},
}
@article{3037,
author = {Feraru, Elena and Friml, Jirí},
journal = {Plant Physiology},
number = {4},
pages = {1553 -- 1559},
publisher = {American Society of Plant Biologists},
title = {{PIN polar targeting}},
doi = {10.1104/pp.108.121756},
volume = {147},
year = {2008},
}
@article{3307,
abstract = {A complete mitochondrial (mt) genome sequence was reconstructed from a 38,000 year-old Neandertal individual with 8341 mtDNA sequences identified among 4.8 Gb of DNA generated from ∼0.3 g of bone. Analysis of the assembled sequence unequivocally establishes that the Neandertal mtDNA falls outside the variation of extant human mtDNAs, and allows an estimate of the divergence date between the two mtDNA lineages of 660,000 ± 140,000 years. Of the 13 proteins encoded in the mtDNA, subunit 2 of cytochrome c oxidase of the mitochondrial electron transport chain has experienced the largest number of amino acid substitutions in human ancestors since the separation from Neandertals. There is evidence that purifying selection in the Neandertal mtDNA was reduced compared with other primate lineages, suggesting that the effective population size of Neandertals was small.},
author = {Green, Richard E and Malaspinas, Anna-Sapfo and Krause, Johannes and Briggs, Adrian W and Johnson, Philip L and Caroline Uhler and Meyer, Matthias and Good, Jeffrey M and Maricic, Tomislav and Stenzel, Udo and Prüfer, Kay and Siebauer, Michael F and Burbano, Hernän A and Ronan, Michael T and Rothberg, Jonathan M and Egholm, Michael and Rudan, Pavao and Brajković, Dejana and Kućan, Željko and Gušić, Ivan and Wikström, Mårten K and Laakkonen, Liisa J and Kelso, Janet F and Slatkin, Montgomery and Pääbo, Svante H},
journal = {Cell},
pages = {416 -- 426},
publisher = {Cell Press},
title = {{A complete neandertal mitochondrial genome sequence determined by highhhroughput sequencing}},
doi = {10.1016/j.cell.2008.06.021},
volume = {134},
year = {2008},
}
@article{3435,
abstract = {We develop a new method for estimating effective population sizes, Ne, and selection coefficients, s, from time-series data of allele frequencies sampled from a single diallelic locus. The method is based on calculating transition probabilities, using a numerical solution of the diffusion process, and assuming independent binomial sampling from this diffusion process at each time point. We apply the method in two example applications. First, we estimate selection coefficients acting on the CCR5-Δ32 mutation on the basis of published samples of contemporary and ancient human DNA. We show that the data are compatible with the assumption of s = 0, although moderate amounts of selection acting on this mutation cannot be excluded. In our second example, we estimate the selection coefficient acting on a mutation segregating in an experimental phage population. We show that the selection coefficient acting on this mutation is ~0.43.},
author = {Jonathan Bollback and York, Thomas L and Nielsen, Rasmus},
journal = {Genetics},
number = {1},
pages = {497 -- 502},
publisher = {Genetics Society of America},
title = {{Estimation of 2Nes From Temporal Allele Frequency Data}},
doi = {10.1534/genetics.107.085019},
volume = {179},
year = {2008},
}
@inproceedings{3504,
abstract = {Simulation and bisimulation metrics for stochastic systems provide a quantitative gen- eralization of the classical simulation and bisimulation relations. These metrics capture the similarity of states with respect to quantitative specifications written in the quantitative μ-calculus and related probabilistic logics.
We present algorithms for computing the metrics on Markov decision processes (MDPs), turn- based stochastic games, and concurrent games. For turn-based games and MDPs, we provide a polynomial-time algorithm based on linear programming for the computation of the one-step metric distance between states. The algorithm improves on the previously known exponential-time algo- rithm based on a reduction to the theory of reals. We then present PSPACE algorithms for both the decision problem and the problem of approximating the metric distance between two states, matching the best known bound for Markov chains. For the bisimulation kernel of the metric, which corresponds to probabilistic bisimulation, our algorithm works in time O(n4) for both turn-based games and MDPs; improving the previously best known O(n9 · log(n)) time algorithm for MDPs. For a concurrent game G, we show that computing the exact distance between states is at least as hard as computing the value of concurrent reachability games and the square-root-sum problem in computational geometry. We show that checking whether the metric distance is bounded by a rational r, can be accomplished via a reduction to the theory of real closed fields, involving a
formula with three quantifier alternations, yielding O(|G|O(|G|5)) time complexity, improving the previously known reduction with O(|G|O(|G|7)) time complexity. These algorithms can be iterated
to approximate the metrics using binary search.},
author = {Chatterjee, Krishnendu and De Alfaro, Luca and Majumdar, Ritankar and Raman, Vishwanath},
pages = {107 -- 118},
publisher = {Schloss Dagstuhl - Leibniz-Zentrum für Informatik},
title = {{Algorithms for game metrics}},
doi = {10.4230/LIPIcs.FSTTCS.2008.1745},
volume = {2},
year = {2008},
}
@article{9457,
abstract = {Eukaryotic chromatin is separated into functional domains differentiated by posttranslational histone modifications, histone variants, and DNA methylation1–6. Methylation is associated with repression of transcriptional initiation in plants and animals, and is frequently found in transposable elements. Proper methylation patterns are critical for eukaryotic development4,5, and aberrant methylation-induced silencing of tumor suppressor genes is a common feature of human cancer7. In contrast to methylation, the histone variant H2A.Z is preferentially deposited by the Swr1 ATPase complex near 5′ ends of genes where it promotes transcriptional competence8–20. How DNA methylation and H2A.Z influence transcription remains largely unknown. Here we show that in the plant Arabidopsis thaliana, regions of DNA methylation are quantitatively deficient in H2A.Z. Exclusion of H2A.Z is seen at sites of DNA methylation in the bodies of actively transcribed genes and in methylated transposons. Mutation of the MET1 DNA methyltransferase, which causes both losses and gains of DNA methylation4,5, engenders opposite changes in H2A.Z deposition, while mutation of the PIE1 subunit of the Swr1 complex that deposits H2A.Z17 leads to genome-wide hypermethylation. Our findings indicate that DNA methylation can influence chromatin structure and effect gene silencing by excluding H2A.Z, and that H2A.Z protects genes from DNA methylation.},
author = {ZILBERMAN, Daniel and Coleman-Derr, Devin and Ballinger, Tracy and Henikoff, Steven},
issn = {1476-4687},
journal = {Nature},
keywords = {Multidisciplinary},
number = {7218},
pages = {125--129},
publisher = {Springer Nature},
title = {{Histone H2A.Z and DNA methylation are mutually antagonistic chromatin marks}},
doi = {10.1038/nature07324},
volume = {456},
year = {2008},
}
@article{2367,
abstract = {It was recently shown by Hansen that the Wigner-Yanase entropy is, for general states of quantum systems, not subadditive with respect to decomposition into two subsystems, although this property is known to hold for pure states. We investigate the question whether the weaker property of subadditivity for pure states with respect to decomposition into more than two subsystems holds. This property would have interesting applications in quantum chemistry. We show, however, that it does not hold in general, and provide a counterexample.},
author = {Robert Seiringer},
journal = {Letters in Mathematical Physics},
number = {3},
pages = {285 -- 288},
publisher = {Springer},
title = {{On the failure of subadditivity of the Wigner-Yanase entropy}},
doi = {10.1007/s11005-007-0159-x},
volume = {80},
year = {2007},
}
@article{2370,
abstract = {After recalling briefly the connection between spontaneous symmetry breaking and off-diagonal long-range order for models of magnets a general proof of spontaneous breaking of gauge symmetry as a consequence of Bose-Einstein condensation is presented. The proof is based on a rigorous validation of Bogoliubov's c-number substitution for the k = 0 mode operator α0.},
author = {Lieb, Élliott H and Robert Seiringer and Yngvason, Jakob},
journal = {Reports on Mathematical Physics},
number = {3},
pages = {389 -- 399},
publisher = {Elsevier},
title = {{Bose-Einstein condensation and spontaneous symmetry breaking}},
doi = {10.1016/S0034-4877(07)80074-7},
volume = {59},
year = {2007},
}
@article{2371,
abstract = {We give a proof of stability of relativistic matter with magnetic fields all the way up to the critical value of the nuclear charge Zα = 2/π.},
author = {Frank, Rupert L and Lieb, Élliott H and Robert Seiringer},
journal = {Communications in Mathematical Physics},
number = {2},
pages = {479 -- 489},
publisher = {Springer},
title = {{Stability of relativistic matter with magnetic fields for nuclear charges up to the critical value}},
doi = {10.1007/s00220-007-0307-2},
volume = {275},
year = {2007},
}
@article{2372,
abstract = {The increasing interest in the Müller density-matrix-functional theory has led us to a systematic mathematical investigation of its properties. This functional is similar to the Hartree-Fock (HF) functional, but with a modified exchange term in which the square of the density matrix γ(x, x′) is replaced by the square of γ1 2 (x, x′). After an extensive introductory discussion of density-matrix-functional theory we show, among other things, that this functional is convex (unlike the HF functional) and that energy minimizing γ 's have unique densities ρ(r), which is a physically desirable property often absent in HF theory. We show that minimizers exist if N≤Z, and derive various properties of the minimal energy and the corresponding minimizers. We also give a precise statement about the equation for the orbitals of γ, which is more complex than for HF theory. We state some open mathematical questions about the theory together with conjectured solutions.},
author = {Frank, Rupert L and Lieb, Élliott H and Robert Seiringer and Siedentop, Heinz K},
journal = {Physical Review A - Atomic, Molecular, and Optical Physics},
number = {5},
publisher = {American Physical Society},
title = {{Müller's exchange-correlation energy in density-matrix-functional theory}},
doi = {10.1103/PhysRevA.76.052517},
volume = {76},
year = {2007},
}
@article{2373,
abstract = {For the BCS equation with local two-body interaction λV(x), we give a rigorous analysis of the asymptotic behavior of the critical temperature as γ"0. We derive necessary and sufficient conditions onV(x) for the existence of a nontrivial solution for all values of γ>0.},
author = {Frank, Rupert L and Hainzl, Christian and Naboko, Serguei N and Robert Seiringer},
journal = {Journal of Geometric Analysis},
number = {4},
pages = {559 -- 567},
publisher = {Springer},
title = {{The critical temperature for the BCS equation at weak coupling}},
doi = {10.1007/BF02937429},
volume = {17},
year = {2007},
}
@article{2375,
abstract = {We give a Cwikel-Lieb-Rozenblum type bound on the number of bound states of Schrödinger operators with matrix-valued potentials using the functional integral method of Lieb. This significantly improves the constant in this inequality obtained earlier by Hundertmark.},
author = {Frank, Rupert L and Lieb, Élliott H and Robert Seiringer},
journal = {Letters in Mathematical Physics},
number = {2-3},
pages = {107 -- 116},
publisher = {Springer},
title = {{Number of bound states of Schrödinger operators with matrix-valued potentials}},
doi = {10.1007/s11005-007-0211-x},
volume = {82},
year = {2007},
}
@inbook{2705,
author = {László Erdös},
booktitle = {Spectral Theory and Mathematical Physics: a Festschrift in Honor of Barry Simon's 60th Birthday },
editor = {Gesztesy, Fritz and Deift, Percy and Galvez, Percy and Perry, Peter and Schlag, Wilhelm},
pages = {401 -- 428},
publisher = {American Mathematical Society},
title = {{Recent developments in quantum mechanics with magnetic fields}},
volume = {76},
year = {2007},
}
@article{1762,
abstract = {In quantum information science, the phase of a wave function plays an important role in encoding information. Although most experiments in this field rely on dynamic effects to manipulate this information, an alternative approach is to use geometric phase, which has been argued to have potential fault tolerance. We demonstrated the controlled accumulation of a geometric phase, Berry's phase, in a superconducting qubit; we manipulated the qubit geometrically by means of microwave radiation and observed the accumulated phase in an interference experiment. We found excellent agreement with Berry's predictions and also observed a geometry-dependent contribution to dephasing.},
author = {Leek, Peter J and Johannes Fink and Blais, Alexandre and Bianchetti, R and Göppl, M and Gambetta, Jay M and Schuster, David I and Frunzio, Luigi and Schoelkopf, Robert J and Wallraff, Andreas},
journal = {Science},
number = {5858},
pages = {1889 -- 1892},
publisher = {American Association for the Advancement of Science},
title = {{Observation of Berry's phase in a solid-state qubit}},
doi = {10.1126/science.1149858},
volume = {318},
year = {2007},
}
@inproceedings{2091,
abstract = {We present a novel multi-scale representation and acquisition method for the animation of high-resolution facial geometry and wrinkles. We first acquire a static scan of the face including reflectance data at the highest possible quality. We then augment a traditional marker-based facial motion-capture system by two synchronized video cameras to track expression wrinkles. The resulting model consists of high-resolution geometry, motion-capture data, and expression wrinkles in 2D parametric form. This combination represents the facial shape and its salient features at multiple scales. During motion synthesis the motion-capture data deforms the high-resolution geometry using a linear shell-based mesh-deformation method. The wrinkle geometry is added to the facial base mesh using nonlinear energy optimization. We present the results of our approach for performance replay as well as for wrinkle editing. },
author = {Bernd Bickel and Botsch, Mario and Angst, Roland and Matusik, Wojciech and Otaduy, Miguel A and Pfister, Hanspeter and Groß, Markus S},
publisher = {ACM},
title = {{Multi scale capture of facial geometry and motion}},
doi = {doi:10.1145/1275808.1276419},
year = {2007},
}
@article{2093,
abstract = {We present a novel multi-scale representation and acquisition method for the animation of high-resolution facial geometry and wrinkles. We first acquire a static scan of the face including reflectance data at the highest possible quality. We then augment a traditional marker-based facial motion-capture system by two synchronized video cameras to track expression wrinkles. The resulting model consists of high-resolution geometry, motion-capture data, and expression wrinkles in 2D parametric form. This combination represents the facial shape and its salient features at multiple scales. During motion synthesis the motion-capture data deforms the high-resolution geometry using a linear shell-based mesh-deformation method. The wrinkle geometry is added to the facial base mesh using nonlinear energy optimization. We present the results of our approach for performance replay as well as for wrinkle editing. },
author = {Bernd Bickel and Botsch, Mario and Angst, Roland and Matusik, Wojciech and Otaduy, Miguel A and Pfister, Hanspeter and Groß, Markus S},
journal = {ACM Transactions on Graphics},
number = {3},
publisher = {ACM},
title = {{Multi scale capture of facial geometry and motion}},
doi = {10.1145/1276377.1276419},
volume = {26},
year = {2007},
}
@article{2118,
abstract = {We extend to infinite dimensions an explicit formula of Chill, Fašangová, Metafune, and Pallara for the optimal angle of analyticity of analytic Ornstein-Uhlenbeck semigroups. The main ingredient is an abstract representation of the Ornstein-Uhlenbeck operator in divergence form. },
author = {Jan Maas and van Neerven, Jan M},
journal = {Archiv der Mathematik},
number = {3},
pages = {226 -- 236},
publisher = {Birkhäuser},
title = {{On analytic Ornstein-Uhlenbeck semigroups in infinite dimensions}},
doi = {10.1007/s00013-007-2082-x},
volume = {89},
year = {2007},
}
@article{221,
author = {De La Bretèche, Régis and Browning, Timothy D},
journal = {Michigan Mathematical Journal},
number = {1},
pages = {51 -- 80},
publisher = {Project Euclid},
title = {{On Manin's conjecture for singular del Pezzo surfaces of degree four, I}},
doi = {10.1307/mmj/1177681985},
volume = {55},
year = {2007},
}
@article{222,
abstract = {Acknowledgements. The authors are grateful to Ulrich Derenthal and Brendan Hassett for several useful conversations relating to universal torsors for singular del Pezzo surfaces. Special thanks are due to Roger Heath–Brown whose ideas led us to the proof of Lemma 6. The paper was finalised while the first author was at the École Normale Supérieure, and the second author was at Oxford University supported by EPSRC grant number GR/R93155/01. The hospitality and financial support of these institutions is gratefully acknowledged. Finally, the authors would like to thank the anonymous referee for his careful reading of the manuscript and numerous useful suggestions.},
author = {de la Bretèche, Régis and Timothy Browning},
journal = {Mathematical Proceedings of the Cambridge Philosophical Society},
number = {3},
pages = {579 -- 605},
publisher = {Unknown},
title = {{On Manin's conjecture for singular del Pezzo surfaces of degree four, II}},
doi = {10.1017/S0305004107000205},
volume = {143},
year = {2007},
}
@article{223,
abstract = {Let Q be a non-singular diagonal quadratic form in at least four variables. We provide upper bounds for the number of integer solutions to the equation Q = 0, which lie in a box with sides of length 2B, as B → ∞. The estimates obtained are completely uniform in the coefficients of the form, and become sharper as they grow larger in modulus.},
author = {Timothy Browning},
journal = {Monatshefte fur Mathematik},
number = {1},
pages = {13 -- 38},
publisher = {Springer},
title = {{Density of integer solutions to diagonal quadratic forms}},
doi = {10.1007/s00605-007-0457-5},
volume = {152},
year = {2007},
}