TY - CONF
AB - 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.
AU - Chatterjee, Krishnendu
AU - Henzinger, Thomas A
AU - Jobstmann, Barbara
AU - Radhakrishna, Arjun
ID - 4388
TI - GIST: A solver for probabilistic games
VL - 6174
ER -
TY - CONF
AB - 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.
AU - Doyen, Laurent
AU - Henzinger, Thomas A
AU - Legay, Axel
AU - Nickovic, Dejan
ID - 4389
TI - Robustness of sequential circuits
ER -
TY - CONF
AB - 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.
AU - Cerny, Pavol
AU - Radhakrishna, Arjun
AU - Zufferey, Damien
AU - Chaudhuri, Swarat
AU - Alur, Rajeev
ID - 4390
TI - Model checking of linearizability of concurrent list implementations
VL - 6174
ER -
TY - CONF
AB - 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.
AU - Cerny, Pavol
AU - Henzinger, Thomas A
AU - Radhakrishna, Arjun
ID - 4393
TI - Simulation distances
VL - 6269
ER -
TY - CONF
AB - 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.
AU - Beyer, Dirk
AU - Henzinger, Thomas A
AU - Théoduloz, Grégory
AU - Zufferey, Damien
ED - Rosenblum, David
ED - Taenzer, Gabriele
ID - 4396
TI - Shape refinement through explicit heap analysis
VL - 6013
ER -
TY - CONF
AB - 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.
AU - Bangerter, Endre
AU - Briner, Thomas
AU - Henecka, Wilko
AU - Stephan Krenn
AU - Sadeghi, Ahmad-Reza
AU - Schneider, Thomas
ED - Martinelli, Fabio
ED - Preneel, Bart
ID - 2980
TI - Automatic Generation of Sigma-Protocols
VL - 6391
ER -
TY - JOUR
AB - 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.
AU - Grunewald, Wim
AU - Friml, Jirí
ID - 3072
IS - 16
JF - EMBO Journal
TI - The march of the PINs: Developmental plasticity by dynamic polar targeting in plant cells
VL - 29
ER -
TY - JOUR
AU - Friml, Jirí
AU - Jones, Angharad
ID - 3077
IS - 2
JF - Plant Physiology
TI - Endoplasmic reticulum: The rising compartment in auxin biology
VL - 154
ER -
TY - JOUR
AB - 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.
AU - Weissman, Daniel
AU - Feldman, Marcus
AU - Fisher, Daniel
ID - 3303
IS - 4
JF - Genetics
TI - The rate of fitness-valley crossing in sexual populations
VL - 186
ER -
TY - JOUR
AB - 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.
AU - Evans, Steven N
AU - Sturmfels, Bernd
AU - Caroline Uhler
ID - 3306
JF - The Annals of Applied Probability
TI - Commuting birth and death processes
VL - 20
ER -
TY - JOUR
AB - 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.
AU - Sturmfels, Bernd
AU - Caroline Uhler
ID - 3308
IS - 4
JF - Annals of the Institute of Statistical Mathematics
TI - Multivariate Gaussians, semidefinite matrix completion, and convex algebraic geometry
VL - 62
ER -
TY - CONF
AB - 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.
AU - Gasper Tkacik
ID - 3430
TI - Lecture notes for 2010 summer school on Quantitative Evolutionary and Comparative Genomics
ER -
TY - JOUR
AB - 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.
AU - Jiruska, Premysl
AU - Csicsvari, Jozsef L
AU - Powell, Andrew
AU - Fox, John
AU - Chang, Wei
AU - Vreugdenhil, Martin
AU - Li, Xiaoli
AU - Palus, Milan
AU - Bujan, Alejandro
AU - Dearden, Richard
AU - Jefferys, John
ID - 3538
IS - 16
JF - Journal of Neuroscience
TI - High-frequency network activity, global increase in neuronal activity, and synchrony expansion precede epileptic seizures in vitro
VL - 30
ER -
TY - CONF
AB - 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.
AU - Wies, Thomas
AU - Zufferey, Damien
AU - Henzinger, Thomas A
ED - Ong, Luke
ID - 4361
TI - Forward analysis of depth-bounded processes
VL - 6014
ER -
TY - JOUR
AB - 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.
AU - Zemach, Assaf
AU - Kim, M. Yvonne
AU - Silva, Pedro
AU - Rodrigues, Jessica A.
AU - Dotson, Bradley
AU - Brooks, Matthew D.
AU - ZILBERMAN, Daniel
ID - 9485
IS - 43
JF - Proceedings of the National Academy of Sciences
SN - 0027-8424
TI - Local DNA hypomethylation activates genes in rice endosperm
VL - 107
ER -
TY - JOUR
AB - 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.
AU - Zemach, Assaf
AU - ZILBERMAN, Daniel
ID - 9489
IS - 17
JF - Current Biology
SN - 0960-9822
TI - Evolution of eukaryotic DNA methylation and the pursuit of safer sex
VL - 20
ER -
TY - JOUR
AB - 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.
AU - Timothy Browning
AU - Heath-Brown, Roger
ID - 228
IS - 629
JF - Journal fur die Reine und Angewandte Mathematik
TI - Rational points on quartic hypersurfaces
ER -
TY - JOUR
AB - 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 ℚ.
AU - Timothy Browning
ID - 229
IS - 1
JF - Mathematische Annalen
TI - Linear growth for Châtelet surfaces
VL - 346
ER -
TY - JOUR
AB - 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.
AU - Giuliani, Alessandro
AU - Robert Seiringer
ID - 2384
IS - 5-6
JF - Journal of Statistical Physics
TI - The ground state energy of the weakly interacting Bose gas at high density
VL - 135
ER -
TY - JOUR
AB - 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.
AU - Lieb, Élliott H
AU - Robert Seiringer
AU - Yngvason, Jakob
ID - 2385
IS - 6
JF - Physical Review A - Atomic, Molecular, and Optical Physics
TI - Yrast line of a rapidly rotating Bose gas: Gross-Pitaevskii regime
VL - 79
ER -