@inproceedings{4388,
abstract = {GIST is a tool that (a) solves the qualitative analysis problem of turn-based probabilistic games with ω-regular objectives; and (b) synthesizes reasonable environment assumptions for synthesis of unrealizable specifications. Our tool provides the first and efficient implementations of several reduction-based techniques to solve turn-based probabilistic games, and uses the analysis of turn-based probabilistic games for synthesizing environment assumptions for unrealizable specifications.},
author = {Chatterjee, Krishnendu and Henzinger, Thomas A and Jobstmann, Barbara and Radhakrishna, Arjun},
location = {Edinburgh, UK},
pages = {665 -- 669},
publisher = {Springer},
title = {{GIST: A solver for probabilistic games}},
doi = {10.1007/978-3-642-14295-6_57},
volume = {6174},
year = {2010},
}
@inproceedings{4389,
abstract = {Digital components play a central role in the design of complex embedded systems. These components are interconnected with other, possibly analog, devices and the physical environment. This environment cannot be entirely captured and can provide inaccurate input data to the component. It is thus important for digital components to have a robust behavior, i.e. the presence of a small change in the input sequences should not result in a drastic change in the output sequences. In this paper, we study a notion of robustness for sequential circuits. However, since sequential circuits may have parts that are naturally discontinuous (e.g., digital controllers with switching behavior), we need a flexible framework that accommodates this fact and leaves discontinuous parts of the circuit out from the robustness analysis. As a consequence, we consider sequential circuits that have their input variables partitioned into two disjoint sets: control and disturbance variables. Our contributions are (1) a definition of robustness for sequential circuits as a form of continuity with respect to disturbance variables, (2) the characterization of the exact class of sequential circuits that are robust according to our definition, (3) an algorithm to decide whether a sequential circuit is robust or not.},
author = {Doyen, Laurent and Henzinger, Thomas A and Legay, Axel and Nickovic, Dejan},
pages = {77 -- 84},
publisher = {IEEE},
title = {{Robustness of sequential circuits}},
doi = {10.1109/ACSD.2010.26},
year = {2010},
}
@inproceedings{4390,
abstract = {Concurrent data structures with fine-grained synchronization are notoriously difficult to implement correctly. The difficulty of reasoning about these implementations does not stem from the number of variables or the program size, but rather from the large number of possible interleavings. These implementations are therefore prime candidates for model checking. We introduce an algorithm for verifying linearizability of singly-linked heap-based concurrent data structures. We consider a model consisting of an unbounded heap where each vertex stores an element from an unbounded data domain, with a restricted set of operations for testing and updating pointers and data elements. Our main result is that linearizability is decidable for programs that invoke a fixed number of methods, possibly in parallel. This decidable fragment covers many of the common implementation techniques — fine-grained locking, lazy synchronization, and lock-free synchronization. We also show how the technique can be used to verify optimistic implementations with the help of programmer annotations. We developed a verification tool CoLT and evaluated it on a representative sample of Java implementations of the concurrent set data structure. The tool verified linearizability of a number of implementations, found a known error in a lock-free implementation and proved that the corrected version is linearizable.},
author = {Cerny, Pavol and Radhakrishna, Arjun and Zufferey, Damien and Chaudhuri, Swarat and Alur, Rajeev},
location = {Edinburgh, UK},
pages = {465 -- 479},
publisher = {Springer},
title = {{Model checking of linearizability of concurrent list implementations}},
doi = {10.1007/978-3-642-14295-6_41},
volume = {6174},
year = {2010},
}
@inproceedings{4393,
abstract = {Boolean notions of correctness are formalized by preorders on systems. Quantitative measures of correctness can be formalized by real-valued distance functions between systems, where the distance between implementation and specification provides a measure of “fit” or “desirability.” We extend the simulation preorder to the quantitative setting, by making each player of a simulation game pay a certain price for her choices. We use the resulting games with quantitative objectives to define three different simulation distances. The correctness distance measures how much the specification must be changed in order to be satisfied by the implementation. The coverage distance measures how much the implementation restricts the degrees of freedom offered by the specification. The robustness distance measures how much a system can deviate from the implementation description without violating the specification. We consider these distances for safety as well as liveness specifications. The distances can be computed in polynomial time for safety specifications, and for liveness specifications given by weak fairness constraints. We show that the distance functions satisfy the triangle inequality, that the distance between two systems does not increase under parallel composition with a third system, and that the distance between two systems can be bounded from above and below by distances between abstractions of the two systems. These properties suggest that our simulation distances provide an appropriate basis for a quantitative theory of discrete systems. We also demonstrate how the robustness distance can be used to measure how many transmission errors are tolerated by error correcting codes.},
author = {Cerny, Pavol and Henzinger, Thomas A and Radhakrishna, Arjun},
location = {Paris, France},
pages = {235 -- 268},
publisher = {Schloss Dagstuhl - Leibniz-Zentrum für Informatik},
title = {{Simulation distances}},
doi = {10.1007/978-3-642-15375-4_18},
volume = {6269},
year = {2010},
}
@inproceedings{4396,
abstract = {Shape analysis is a promising technique to prove program properties about recursive data structures. The challenge is to automatically determine the data-structure type, and to supply the shape analysis with the necessary information about the data structure. We present a stepwise approach to the selection of instrumentation predicates for a TVLA-based shape analysis, which takes us a step closer towards the fully automatic verification of data structures. The approach uses two techniques to guide the refinement of shape abstractions: (1) during program exploration, an explicit heap analysis collects sample instances of the heap structures, which are used to identify the data structures that are manipulated by the program; and (2) during abstraction refinement along an infeasible error path, we consider different possible heap abstractions and choose the coarsest one that eliminates the infeasible path. We have implemented this combined approach for automatic shape refinement as an extension of the software model checker BLAST. Example programs from a data-structure library that manipulate doubly-linked lists and trees were successfully verified by our tool.},
author = {Beyer, Dirk and Henzinger, Thomas A and Théoduloz, Grégory and Zufferey, Damien},
editor = {Rosenblum, David and Taenzer, Gabriele},
location = {Paphos, Cyprus},
pages = {263 -- 277},
publisher = {Springer},
title = {{Shape refinement through explicit heap analysis}},
doi = {10.1007/978-3-642-12029-9_19},
volume = {6013},
year = {2010},
}
@inproceedings{2980,
abstract = {Efficient zero-knowledge proofs of knowledge (ZK-PoK) are basic
building blocks of many practical cryptographic applications such as
identification schemes, group signatures, and secure multi-party
computation (SMPC). Currently, first applications that essentially
rely on ZK-PoKs are being deployed in the real world. The most
prominent example is the Direct Anonymous Attestation (DAA)
protocol, which was adopted by the Trusted Computing Group (TCG)
and implemented as one of the functionalities of the cryptographic
chip Trusted Platform Module (TPM).
Implementing systems using ZK-PoK turns out to be challenging,
since ZK-PoK are significantly more complex than standard crypto
primitives (e.g., encryption and signature schemes). As a result,
the design-implementation cycles of ZK-PoK are time-consuming
and error-prone.
To overcome this, we present a compiler with corresponding languages
for the automatic generation of sound and efficient ZK-PoK based on
Σ-protocols. The protocol designer using our compiler formulates
the goal of a ZK-PoK proof in a high-level protocol specification language,
which abstracts away unnecessary technicalities from the designer. The
compiler then automatically generates the protocol implementation in
Java code; alternatively, the compiler can output a description of the
protocol in LaTeX which can be used for documentation or verification.},
author = {Bangerter, Endre and Briner, Thomas and Henecka, Wilko and Stephan Krenn and Sadeghi, Ahmad-Reza and Schneider, Thomas},
editor = {Martinelli, Fabio and Preneel, Bart},
pages = {67 -- 82},
publisher = {Springer},
title = {{Automatic Generation of Sigma-Protocols}},
doi = {10.1007/978-3-642-16441-5},
volume = {6391},
year = {2010},
}
@article{3072,
abstract = {Development of plants and their adaptive capacity towards ever‐changing environmental conditions largely depend on the spatial distribution of the plant hormone auxin. At the cellular level, various internal and external signals are translated into specific changes in the polar, subcellular localization of auxin transporters from the PIN family thereby directing and redirecting the intercellular fluxes of auxin. The current model of polar targeting of PIN proteins towards different plasma membrane domains encompasses apolar secretion of newly synthesized PINs followed by endocytosis and recycling back to the plasma membrane in a polarized manner. In this review, we follow the subcellular march of the PINs and highlight the cellular and molecular mechanisms behind polar foraging and subcellular trafficking pathways. Also, the entry points for different signals and regulations including by auxin itself will be discussed within the context of morphological and developmental consequences of polar targeting and subcellular trafficking.},
author = {Grunewald, Wim and Friml, Jirí},
journal = {EMBO Journal},
number = {16},
pages = {2700 -- 2714},
publisher = {Wiley-Blackwell},
title = {{The march of the PINs: Developmental plasticity by dynamic polar targeting in plant cells}},
doi = {10.1038/emboj.2010.181},
volume = {29},
year = {2010},
}
@article{3077,
author = {Friml, Jirí and Jones, Angharad},
journal = {Plant Physiology},
number = {2},
pages = {458 -- 462},
publisher = {American Society of Plant Biologists},
title = {{Endoplasmic reticulum: The rising compartment in auxin biology}},
doi = {10.1104/pp.110.161380},
volume = {154},
year = {2010},
}
@article{3303,
abstract = {Biological traits result in part from interactions between different genetic loci. This can lead to sign epistasis, in which a beneficial adaptation involves a combination of individually deleterious or neutral mutations; in this case, a population must cross a “fitness valley” to adapt. Recombination can assist this process by combining mutations from different individuals or retard it by breaking up the adaptive combination. Here, we analyze the simplest fitness valley, in which an adaptation requires one mutation at each of two loci to provide a fitness benefit. We present a theoretical analysis of the effect of recombination on the valley-crossing process across the full spectrum of possible parameter regimes. We find that low recombination rates can speed up valley crossing relative to the asexual case, while higher recombination rates slow down valley crossing, with the transition between the two regimes occurring when the recombination rate between the loci is approximately equal to the selective advantage provided by the adaptation. In large populations, if the recombination rate is high and selection against single mutants is substantial, the time to cross the valley grows exponentially with population size, effectively meaning that the population cannot acquire the adaptation. Recombination at the optimal (low) rate can reduce the valley-crossing time by up to several orders of magnitude relative to that in an asexual population. },
author = {Weissman, Daniel and Feldman, Marcus and Fisher, Daniel},
journal = {Genetics},
number = {4},
pages = {1389 -- 1410},
publisher = {Genetics Society of America},
title = {{The rate of fitness-valley crossing in sexual populations}},
doi = {10.1534/genetics.110.123240},
volume = {186},
year = {2010},
}
@article{3306,
abstract = {We use methods from combinatorics and algebraic statistics to study analogues of birth-and-death processes that have as their state space a finite subset of the m-dimensional lattice and for which the m matrices that record the transition probabilities in each of the lattice directions commute pairwise. One reason such processes are of interest is that the transition matrix is straightforward to diagonalize, and hence it is easy to compute n step transition probabilities. The set of commuting birth-and-death processes decomposes as a union of toric varieties, with the main component being the closure of all processes whose nearest neighbor transition probabilities are positive. We exhibit an explicit monomial parametrization for this main component, and we explore the boundary components using primary decomposition.},
author = {Evans, Steven N and Sturmfels, Bernd and Caroline Uhler},
journal = {The Annals of Applied Probability},
pages = {238 -- 266},
publisher = {Institute of Mathematical Statistics},
title = {{Commuting birth and death processes}},
doi = {10.1214/09-AAP615},
volume = {20},
year = {2010},
}
@article{3308,
abstract = {We study multivariate normal models that are described by linear constraints on the inverse of the covariance matrix. Maximum likelihood estimation for such models leads to the problem of maximizing the determinant function over a spectrahedron, and to the problem of characterizing the image of the positive definite cone under an arbitrary linear projection. These problems at the interface of statistics and optimization are here examined from the perspective of convex algebraic geometry.},
author = {Sturmfels, Bernd and Caroline Uhler},
journal = {Annals of the Institute of Statistical Mathematics},
number = {4},
pages = {603 -- 638},
publisher = {Springer},
title = {{Multivariate Gaussians, semidefinite matrix completion, and convex algebraic geometry}},
doi = {10.1007/s10463-010-0295-4},
volume = {62},
year = {2010},
}
@inproceedings{3430,
abstract = {These are notes for a set of 7 two-hour lectures given at the 2010 Summer School on Quantitative Evolutionary and Comparative Genomics at OIST, Okinawa, Japan. The emphasis is on understanding how biological systems process information. We take a physicist's approach of looking for simple phenomenological descriptions that can address the questions of biological function without necessarily modeling all (mostly unknown) microscopic details; the example that is developed throughout the notes is transcriptional regulation in genetic regulatory networks. We present tools from information theory and statistical physics that can be used to analyze noisy nonlinear biological networks, and build generative and predictive models of regulatory processes.},
author = {Gasper Tkacik},
publisher = {Elsevier},
title = {{Lecture notes for 2010 summer school on Quantitative Evolutionary and Comparative Genomics}},
year = {2010},
}
@article{3538,
abstract = {How seizures start is a major question in epilepsy research. Preictal EEG changes occur in both human patients and animal models, but their underlying mechanisms and relationship with seizure initiation remain unknown. Here we demonstrate the existence, in the hippocampal CA1 region, of a preictal state characterized by the progressive and global increase in neuronal activity associated with a widespread buildup of low-amplitude high-frequency activity (HFA) (> 100 Hz) and reduction in system complexity. HFA is generated by the firing of neurons, mainly pyramidal cells, at much lower frequencies. Individual cycles of HFA are generated by the near-synchronous (within similar to 5 ms) firing of small numbers of pyramidal cells. The presence of HFA in the low-calcium model implicates nonsynaptic synchronization; the presence of very similar HFA in the high-potassium model shows that it does not depend on an absence of synaptic transmission. Immediately before seizure onset, CA1 is in a state of high sensitivity in which weak depolarizing or synchronizing perturbations can trigger seizures. Transition to seizure is characterized by a rapid expansion and fusion of the neuronal populations responsible for HFA, associated with a progressive slowing of HFA, leading to a single, massive, hypersynchronous cluster generating the high-amplitude low-frequency activity of the seizure.},
author = {Jiruska, Premysl and Csicsvari, Jozsef L and Powell, Andrew and Fox, John and Chang, Wei and Vreugdenhil, Martin and Li, Xiaoli and Palus, Milan and Bujan, Alejandro and Dearden, Richard and Jefferys, John},
journal = {Journal of Neuroscience},
number = {16},
pages = {5690 -- 5701},
publisher = {Society for Neuroscience},
title = {{High-frequency network activity, global increase in neuronal activity, and synchrony expansion precede epileptic seizures in vitro}},
doi = {10.1523/JNEUROSCI.0535-10.2010},
volume = {30},
year = {2010},
}
@inproceedings{4361,
abstract = {Depth-bounded processes form the most expressive known fragment of the π-calculus for which interesting verification problems are still decidable. In this paper we develop an adequate domain of limits for the well-structured transition systems that are induced by depth-bounded processes. An immediate consequence of our result is that there exists a forward algorithm that decides the covering problem for this class. Unlike backward algorithms, the forward algorithm terminates even if the depth of the process is not known a priori. More importantly, our result suggests a whole spectrum of forward algorithms that enable the effective verification of a large class of mobile systems.},
author = {Wies, Thomas and Zufferey, Damien and Henzinger, Thomas A},
editor = {Ong, Luke},
location = {Paphos, Cyprus},
pages = {94 -- 108},
publisher = {Springer},
title = {{Forward analysis of depth-bounded processes}},
doi = {10.1007/978-3-642-12032-9_8},
volume = {6014},
year = {2010},
}
@article{9485,
abstract = {Cytosine methylation silences transposable elements in plants, vertebrates, and fungi but also regulates gene expression. Plant methylation is catalyzed by three families of enzymes, each with a preferred sequence context: CG, CHG (H = A, C, or T), and CHH, with CHH methylation targeted by the RNAi pathway. Arabidopsis thaliana endosperm, a placenta-like tissue that nourishes the embryo, is globally hypomethylated in the CG context while retaining high non-CG methylation. Global methylation dynamics in seeds of cereal crops that provide the bulk of human nutrition remain unknown. Here, we show that rice endosperm DNA is hypomethylated in all sequence contexts. Non-CG methylation is reduced evenly across the genome, whereas CG hypomethylation is localized. CHH methylation of small transposable elements is increased in embryos, suggesting that endosperm demethylation enhances transposon silencing. Genes preferentially expressed in endosperm, including those coding for major storage proteins and starch synthesizing enzymes, are frequently hypomethylated in endosperm, indicating that DNA methylation is a crucial regulator of rice endosperm biogenesis. Our data show that genome-wide reshaping of seed DNA methylation is conserved among angiosperms and has a profound effect on gene expression in cereal crops.},
author = {Zemach, Assaf and Kim, M. Yvonne and Silva, Pedro and Rodrigues, Jessica A. and Dotson, Bradley and Brooks, Matthew D. and ZILBERMAN, Daniel},
issn = {1091-6490},
journal = {Proceedings of the National Academy of Sciences},
number = {43},
pages = {18729--18734},
publisher = {National Academy of Sciences},
title = {{Local DNA hypomethylation activates genes in rice endosperm}},
doi = {10.1073/pnas.1009695107},
volume = {107},
year = {2010},
}
@article{9489,
abstract = {Cytosine methylation is an ancient process with conserved enzymology but diverse biological functions that include defense against transposable elements and regulation of gene expression. Here we will discuss the evolution and biological significance of eukaryotic DNA methylation, the likely drivers of that evolution, and major remaining mysteries.},
author = {Zemach, Assaf and ZILBERMAN, Daniel},
issn = {1879-0445},
journal = {Current Biology},
number = {17},
pages = {R780--R785},
publisher = {Elsevier},
title = {{Evolution of eukaryotic DNA methylation and the pursuit of safer sex}},
doi = {10.1016/j.cub.2010.07.007},
volume = {20},
year = {2010},
}
@article{228,
abstract = {Let X be a projective non-singular quartic hypersurface of dimension 39 or more, which is defined over . We show that X() is non-empty provided that X() is non-empty and X has p-adic points for every prime p.},
author = {Timothy Browning and Heath-Brown, Roger},
journal = {Journal fur die Reine und Angewandte Mathematik},
number = {629},
pages = {37 -- 88},
publisher = {Walter de Gruyter},
title = {{Rational points on quartic hypersurfaces}},
doi = {10.1515/CRELLE.2009.026},
year = {2009},
}
@article{229,
abstract = {An upper bound of the expected order of magnitude is established for the number of ℚ-rational points of bounded height on Châtelet surfaces defined over ℚ.},
author = {Timothy Browning},
journal = {Mathematische Annalen},
number = {1},
pages = {41 -- 50},
publisher = {Springer Nature},
title = {{Linear growth for Châtelet surfaces}},
doi = {10.1007/s00208-009-0383-z},
volume = {346},
year = {2009},
}
@article{2384,
abstract = {We prove the Lee-Huang-Yang formula for the ground state energy of the 3D Bose gas with repulsive interactions described by the exponential function, in a simultaneous limit of weak coupling and high density. In particular, we show that the Bogoliubov approximation is exact in an appropriate parameter regime, as far as the ground state energy is concerned.},
author = {Giuliani, Alessandro and Robert Seiringer},
journal = {Journal of Statistical Physics},
number = {5-6},
pages = {915 -- 934},
publisher = {Springer},
title = {{The ground state energy of the weakly interacting Bose gas at high density}},
doi = {10.1007/s10955-009-9718-0},
volume = {135},
year = {2009},
}
@article{2385,
abstract = {We consider an ultracold rotating Bose gas in a harmonic trap close to the critical angular velocity, so that the system can be considered to be confined to the lowest Landau level. With this assumption we prove that the Gross-Pitaevskii energy functional accurately describes the ground-state energy of the corresponding N -body Hamiltonian with contact interaction provided the total angular momentum L is much less than N2. While the Gross-Pitaevskii energy is always an obvious variational upper bound to the ground-state energy, a more refined analysis is needed to establish it as an exact lower bound. We also discuss the question of Bose-Einstein condensation in the parameter range considered. Coherent states together with inequalities in spaces of analytic functions are the main technical tools.},
author = {Lieb, Élliott H and Robert Seiringer and Yngvason, Jakob},
journal = {Physical Review A - Atomic, Molecular, and Optical Physics},
number = {6},
publisher = {American Physical Society},
title = {{Yrast line of a rapidly rotating Bose gas: Gross-Pitaevskii regime}},
doi = {10.1103/PhysRevA.79.063626},
volume = {79},
year = {2009},
}