TY - JOUR
AB - The Nef protein of human and simian immunodeficiency virus (HIV/SIV) is believed to interfere with T cell activation signals by forming a signaling complex at the plasma membrane. Composition and function of the complex are not fully understood. Here we report that Nef recruits the Polycomb Group (PcG) protein Eed, so far known as a nuclear factor and repressor of transcription, to the membrane of cells. The Nef-induced translocation of Eed led to a potent stimulation of Tat-dependent HIV transcription, implying that Eed removal from the nucleus is required for optimal Tat function. Similar to Nef action, activation of integrin receptors recruited Eed to the plasma membrane, also leading to enhanced Tat/Nef-mediated transcription. Our results suggest a link between membrane-associated activation processes and transcriptional derepression and demonstrate how HIV exploits this mechanism.
AU - Witte, Vanessa
AU - Laffert, Bernd
AU - Rosorius, Olaf
AU - Lischka, Peter
AU - Blume, Katja
AU - Galler, Gunther
AU - Stilper, Andrea
AU - Willbold, Dieter
AU - D'Aloja, Paola
AU - Michael Sixt
AU - Kolanus, Johanna
AU - Ott, Melanie
AU - Kolanus, Waldemar
AU - Schuler, Gerold
AU - Baur, Andreas S
ID - 3929
IS - 2
JF - Molecular Cell
TI - HIV-1 Nef mimics an integrin receptor signal that recruits the polycomb group protein Eed to the plasma membrane
VL - 13
ER -
TY - JOUR
AB - Hyaluronan is an unsulfated glycosaminoglycan (GAG) that is ubiquitously expressed in the extracellular matrix (ECM) of all vertebrates, where hyaluronan rich matrices constitute a particular permissive environment for the development of complex biological structures and also for tumor progression. Because of its conserved structure and ubiquitous expression, antibodies for its histochemical detection cannot be produced. We have engineered a fusion protein, neurocan-GFP, and expressed it as a secreted molecule in mammalian cells. Neurocan-GFP fusion protein specifically binds to hyaluronan and directly visualizes hyaluronan on tissue sections, revealing a very detailed picture of hyaluronan distribution. The fluorescent fusion protein can be used in combination with antibodies and nuclear markers for double or triple staining. In addition, it is suitable to visualize hyaluronan on living cells by time-lapse video microscopy. The successful production and application of the neurocan-GFP fusion protein opens up new perspectives for using GFP fusion proteins as detection tools in histological and cytological studies complementing conventional antibody and biotin/avidin techniques.
AU - Zhang, Hui
AU - Baader, Stephan L
AU - Michael Sixt
AU - Kappler, Joachim
AU - Rauch, Uwe
ID - 3931
IS - 7
JF - Journal of Histochemistry and Cytochemistry
TI - Neurocan-GFP fusion protein: a new approach to detect hyaluronan on tissue sections and living cells
VL - 52
ER -
TY - JOUR
AB - We combine topological and geometric methods to construct a multiresolution representation for a function over a two-dimensional domain. In a preprocessing stage, we create the Morse-Smale complex of the function and progressively simplify its topology by cancelling pairs of critical points. Based on a simple notion of dependency among these cancellations, we construct a hierarchical data structure supporting traversal and reconstruction operations similarly to traditional geometry-based representations. We use this data structure to extract topologically valid approximations that satisfy error bounds provided at runtime.
AU - Bremer, Peer-Timo
AU - Herbert Edelsbrunner
AU - Hamann, Bernd
AU - Pascucci, Valerio
ID - 3984
IS - 4
JF - IEEE Transactions on Visualization and Computer Graphics
TI - A topological hierarchy for functions on triangulated surfaces
VL - 10
ER -
TY - JOUR
AB - Given a Morse function f over a 2-manifold with or without boundary, the Reeb graph is obtained by contracting the connected components of the level sets to points. We prove tight upper and lower bounds on the number of loops in the Reeb graph that depend on the genus, the number of boundary components, and whether or not the 2-manifold is orientable. We also give an algorithm that constructs the Reeb graph in time O(n log n), where n is the number of edges in the triangulation used to represent the 2-manifold and the Morse function.
AU - Cole-McLaughlin, Kree
AU - Herbert Edelsbrunner
AU - Harer, John
AU - Natarajan, Vijay
AU - Pascucci, Valerio
ID - 3985
IS - 2
JF - Discrete & Computational Geometry
TI - Loops in Reeb graphs of 2-manifolds
VL - 32
ER -
TY - JOUR
AB - The motion of a biomolecule greatly depends on the engulfing solution, which is mostly water. Instead of representing individual water molecules, it is desirable to develop implicit solvent models that nevertheless accurately represent the contribution of the solvent interaction to the motion. In such models, hydrophobicity is expressed as a weighted sum of atomic surface areas. The derivatives of these weighted areas contribute to the force that drives the motion. In this paper we give formulas for the weighted and unweighted area derivatives of a molecule modeled as a space-filling diagram made up of balls in motion. Other than the radii and the centers of the balls, the formulas are given in terms of the sizes of circular arcs of the boundary and edges of the power diagram. We also give inclusion-exclusion formulas for these sizes.
AU - Bryant, Robert
AU - Herbert Edelsbrunner
AU - Koehl, Patrice
AU - Levitt, Michael
ID - 3986
IS - 3
JF - Discrete & Computational Geometry
TI - The area derivative of a space-filling diagram
VL - 32
ER -
TY - JOUR
AB - We consider scientific data sets that describe density functions over three-dimensional geometric domains. Such data sets are often large and coarsened representations are needed for visualization and analysis. Assuming a tetrahedral mesh representation, we construct such representations with a simplification algorithm that combines three goals: the approximation of the function, the preservation of the mesh topology, and the improvement of the mesh quality. The third goal is achieved with a novel extension of the well-known quadric error metric. We perform a number of computational experiments to understand the effect of mesh quality improvement on the density map approximation. In addition, we study the effect of geometric simplification on the topological features of the function by monitoring its critical points.
AU - Natarajan, Vijay
AU - Herbert Edelsbrunner
ID - 3987
IS - 5
JF - IEEE Transactions on Visualization and Computer Graphics
TI - Simplification of three-dimensional density maps
VL - 10
ER -
TY - CONF
AB - We give an algorithm that locally improves the fit between two proteins modeled as space-filling diagrams. The algorithm defines the fit in purely geometric terms and improves by applying a rigid motion to one of the two proteins. Our implementation of the algorithm takes between three and ten seconds and converges with high likelihood to the correct docked configuration, provided it starts at a position away from the correct one by at most 18 degrees of rotation and at most 3.0Angstrom of translation. The speed and convergence radius make this an attractive algorithm to use in combination with a coarse sampling of the six-dimensional space of rigid motions.
AU - Choi, Vicky
AU - Agarwal, Pankaj K
AU - Herbert Edelsbrunner
AU - Rudolph, Johannes
ID - 3988
TI - Local search heuristic for rigid protein docking
VL - 3240
ER -
TY - CONF
AB - We introduce local and global comparison measures for a collection of k less than or equal to d real-valued smooth functions on a common d-dimensional Riemannian manifold. For k = d = 2 we relate the measures to the set of critical points of one function restricted to the level sets of the other. The definition of the measures extends to piecewise linear functions for which they ace easy to compute. The computation of the measures forms the centerpiece of a software tool which we use to study scientific datasets.
AU - Herbert Edelsbrunner
AU - Harer, John
AU - Natarajan, Vijay
AU - Pascucci, Valerio
ID - 3989
TI - Local and global comparison of continuous functions
ER -
TY - JOUR
AB - The writhing number measures the global geometry of a closed space curve or knot. We show that this measure is related to the average winding number of its Gauss map. Using this relationship, we give an algorithm for computing the writhing number for a polygonal knot with n edges in time roughly proportional to n(1.6). We also implement a different, simple algorithm and provide experimental evidence for its practical efficiency.
AU - Agarwal, Pankaj K
AU - Herbert Edelsbrunner
AU - Wang, Yusu
ID - 3990
IS - 1
JF - Discrete & Computational Geometry
TI - Computing the writhing number of a polygonal knot
VL - 32
ER -
TY - CHAP
AU - Harold Vladar
AU - Cipriani, Roberto
AU - Scharifker, Benjamin
AU - Bubis, Jose
ED - Hanslmeier,A.
ED - Kempe,S.
ED - Seckbach,J.
ID - 4230
T2 - Life in the Universe From the Miller Experiment to the Search for Life on Other Worlds
TI - A mechanism for the prebiotic emergence of proteins
ER -
TY - CHAP
AU - Harold Vladar
AU - Cipriani, Roberto
AU - Scharifker, Benjamin
AU - Bubis, Jose
ED - Seckbach,J.
ED - Chela-Flores,J.
ED - Owen,T.
ED - Raulin,F.
ID - 4239
T2 - Life in the Universe From the Miller Experiment to the Search for Life on Other Worlds
TI - A Mechanism for the Prebiotic Emergence of Proteins
VL - 7
ER -
TY - JOUR
AB - We consider a single genetic locus which carries two alleles, labelled P and Q. This locus experiences selection and mutation. It is linked to a second neutral locus with recombination rate r. If r = 0, this reduces to the study of a single selected locus. Assuming a Moran model for the population dynamics, we pass to a diffusion approximation and, assuming that the allele frequencies at the selected locus have reached stationarity, establish the joint generating function for the genealogy of a sample from the population and the frequency of the P allele. In essence this is the joint generating function for a coalescent and the random background in which it evolves. We use this to characterize, for the diffusion approximation, the probability of identity in state at the neutral locus of a sample of two individuals (whose type at the selected locus is known) as solutions to a system of ordinary differential equations. The only subtlety is to find the boundary conditions for this system. Finally, numerical examples are presented that illustrate the accuracy and predictions of the diffusion approximation. In particular, a comparison is made between this approach and one in which the frequencies at the selected locus are estimated by their value in the absence of fluctuations and a classical structured coalescent model is used.
AU - Nicholas Barton
AU - Etheridge, Alison M
AU - Sturm, Anja K
ID - 4253
IS - 2
JF - Annals of Applied Probability
TI - Coalescence in a Random Background
VL - 14
ER -
TY - CONF
AU - Maler, Oded
AU - Dejan Nickovic
ID - 4372
TI - Monitoring Temporal Properties of Continuous Signals
ER -
TY - CONF
AB - We present a type system for E code, which is an assembly language that manages the release, interaction, and termination of real-time tasks. E code specifies a deadline for each task, and the type system ensures that the deadlines are path-insensitive. We show that typed E programs allow, for given worst-case execution times of tasks, a simple schedulability analysis. Moreover, the real-time programming language Giotto can be compiled into typed E~code. This shows that typed E~code identifies an easily schedulable yet expressive class of real-time programs. We have extended the Giotto compiler to generate typed E code, and enabled the run-time system for E code to perform a type and schedulability check before executing the code.
AU - Thomas Henzinger
AU - Kirsch, Christoph M
ID - 4445
TI - A typed assembly language for real-time programs
ER -
TY - CONF
AB - The success of model checking for large programs depends crucially on the ability to efficiently construct parsimonious abstractions. A predicate abstraction is parsimonious if at each control location, it specifies only relationships between current values of variables, and only those which are required for proving correctness. Previous methods for automatically refining predicate abstractions until sufficient precision is obtained do not systematically construct parsimonious abstractions: predicates usually contain symbolic variables, and are added heuristically and often uniformly to many or all control locations at once. We use Craig interpolation to efficiently construct, from a given abstract error trace which cannot be concretized, a parsominous abstraction that removes the trace. At each location of the trace, we infer the relevant predicates as an interpolant between the two formulas that define the past and the future segment of the trace. Each interpolant is a relationship between current values of program variables, and is relevant only at that particular program location. It can be found by a linear scan of the proof of infeasibility of the trace.We develop our method for programs with arithmetic and pointer expressions, and call-by-value function calls. For function calls, Craig interpolation offers a systematic way of generating relevant predicates that contain only the local variables of the function and the values of the formal parameters when the function was called. We have extended our model checker Blast with predicate discovery by Craig interpolation, and applied it successfully to C programs with more than 130,000 lines of code, which was not possible with approaches that build less parsimonious abstractions.
AU - Thomas Henzinger
AU - Jhala, Ranjit
AU - Majumdar, Ritankar S
AU - McMillan, Kenneth L
ID - 4458
TI - Abstractions from proofs
ER -
TY - CONF
AB - Software model checking has been successful for sequential programs, where predicate abstraction offers suitable models, and counterexample-guided abstraction refinement permits the automatic inference of models. When checking concurrent programs, we need to abstract threads as well as the contexts in which they execute. Stateless context models, such as predicates on global variables, prove insufficient for showing the absence of race conditions in many examples. We therefore use richer context models, which combine (1) predicates for abstracting data state, (2) control flow quotients for abstracting control state, and (3) counters for abstracting an unbounded number of threads. We infer suitable context models automatically by a combination of counterexample-guided abstraction refinement, bisimulation minimization, circular assume-guarantee reasoning, and parametric reasoning about an unbounded number of threads. This algorithm, called CIRC, has been implemented in BLAST and succeeds in checking many examples of NESC code for data races. In particular, BLAST proves the absence of races in several cases where previous race checkers give false positives.
AU - Thomas Henzinger
AU - Jhala, Ranjit
AU - Majumdar, Ritankar S
ID - 4459
TI - Race checking by context inference
ER -
TY - CHAP
AB - One of the central axioms of extreme programming is the disciplined use of regression testing during stepwise software development. Due to recent progress in software model checking, it has become possible to supplement this process with automatic checks for behavioral safety properties of programs, such as conformance with locking idioms and other programming protocols and patterns. For efficiency reasons, all checks must be incremental, i.e., they must reuse partial results from previous checks in order to avoid all unnecessary repetition of expensive verification tasks. We show that the lazy-abstraction algorithm, and its implementation in Blast, can be extended to support the fully automatic and incremental checking of temporal safety properties during software development.
AU - Thomas Henzinger
AU - Jhala, Ranjit
AU - Majumdar, Ritankar S
AU - Sanvido, Marco A
ID - 4461
T2 - Verification: Theory and Practice
TI - Extreme model checking
VL - 2772
ER -
TY - CONF
AB - We present a new high-level programming language, called xGiotto, for programming applications with hard real-time constraints. Like its predecessor, xGiotto is based on the LET (logical execution time) assumption: the programmer specifies when the outputs of a task become available, and the compiler checks if the specification can be implemented on a given platform. However, while the predecessor language xGiotto was purely time-triggered, xGiotto accommodates also asynchronous events. Indeed, through a mechanism called event scoping, events are the main structuring principle of the new language. The xGiotto compiler and run-time system implement event scoping through a tree-based event filter. The compiler also checks programs for determinism (absence of race conditions).
AU - Ghosal, Arkadeb
AU - Thomas Henzinger
AU - Kirsch, Christoph M
AU - Sanvido, Marco A
ID - 4525
TI - Event-driven programming with logical execution times
VL - 2993
ER -
TY - CONF
AB - Strategies in repeated games can be classified as to whether or not they use memory and/or randomization. We consider Markov decision processes and 2-player graph games, both of the deterministic and probabilistic varieties. We characterize when memory and/or randomization are required for winning with respect to various classes of w-regular objectives, noting particularly when the use of memory can be traded for the use of randomization. In particular, we show that Markov decision processes allow randomized memoryless optimal strategies for all M?ller objectives. Furthermore, we show that 2-player probabilistic graph games allow randomized memoryless strategies for winning with probability 1 those M?ller objectives which are upward-closed. Upward-closure means that if a set α of infinitely repeating vertices is winning, then all supersets of α are also winning.
AU - Krishnendu Chatterjee
AU - de Alfaro, Luca
AU - Thomas Henzinger
ID - 4555
TI - Trading memory for randomness
ER -
TY - JOUR
AB - We study the problem of determining stack boundedness and the exact maximum stack size for three classes of interrupt-driven programs. Interrupt-driven programs are used in many real-time applications that require responsive interrupt handling. In order to ensure responsiveness, programmers often enable interrupt processing in the body of lower-priority interrupt handlers. In such programs a programming error can allow interrupt handlers to be interrupted in a cyclic fashion to lead to an unbounded stack, causing the system to crash. For a restricted class of interrupt-driven programs, we show that there is a polynomial-time procedure to check stack boundedness, while determining the exact maximum stack size is PSPACE-complete. For a larger class of programs, the two problems are both PSPACE-complete, and for the largest class of programs we consider, the two problems are PSPACE-hard and can be solved in exponential time. While the complexities are high, our algorithms are exponential only in the number of handlers, and polynomial in the size of the program.
AU - Krishnendu Chatterjee
AU - Ma, Di
AU - Majumdar, Ritankar S
AU - Zhao, Tian
AU - Thomas Henzinger
AU - Palsberg, Jens
ID - 4556
IS - 2
JF - Information and Computation
TI - Stack size analysis for interrupt-driven programs
VL - 194
ER -