@misc{5455,
abstract = {A fundamental algorithmic problem at the heart of static analysis is Dyck reachability. The input is a graphwhere the edges are labeled with different types of opening and closing parentheses, and the reachabilityinformation is computed via paths whose parentheses are properly matched. We present new results for Dyckreachability problems with applications to alias analysis and data-dependence analysis. Our main contributions,that include improved upper bounds as well as lower bounds that establish optimality guarantees, are asfollows:First, we consider Dyck reachability on bidirected graphs, which is the standard way of performing field-sensitive points-to analysis. Given a bidirected graph withnnodes andmedges, we present: (i) an algorithmwith worst-case running timeO(m+n·α(n)), whereα(n)is the inverse Ackermann function, improving thepreviously knownO(n2)time bound; (ii) a matching lower bound that shows that our algorithm is optimalwrt to worst-case complexity; and (iii) an optimal average-case upper bound ofO(m)time, improving thepreviously knownO(m·logn)bound.Second, we consider the problem of context-sensitive data-dependence analysis, where the task is to obtainanalysis summaries of library code in the presence of callbacks. Our algorithm preprocesses libraries in almostlinear time, after which the contribution of the library in the complexity of the client analysis is only linear,and only wrt the number of call sites.Third, we prove that combinatorial algorithms for Dyck reachability on general graphs with truly sub-cubic bounds cannot be obtained without obtaining sub-cubic combinatorial algorithms for Boolean MatrixMultiplication, which is a long-standing open problem. Thus we establish that the existing combinatorialalgorithms for Dyck reachability are (conditionally) optimal for general graphs. We also show that the samehardness holds for graphs of constant treewidth.Finally, we provide a prototype implementation of our algorithms for both alias analysis and data-dependenceanalysis. Our experimental evaluation demonstrates that the new algorithms significantly outperform allexisting methods on the two problems, over real-world benchmarks.},
author = {Chatterjee, Krishnendu and Choudhary, Bhavya and Pavlogiannis, Andreas},
issn = {2664-1690},
pages = {37},
publisher = {IST Austria},
title = {{Optimal Dyck reachability for data-dependence and alias analysis}},
doi = {10.15479/AT:IST-2017-870-v1-1},
year = {2017},
}
@misc{5456,
abstract = {We present a new dynamic partial-order reduction method for stateless model checking of concurrent programs. A common approach for exploring program behaviors relies on enumerating the traces of the program, without storing the visited states (aka stateless exploration). As the number of distinct traces grows exponentially, dynamic partial-order reduction (DPOR) techniques have been successfully used to partition the space of traces into equivalence classes (Mazurkiewicz partitioning), with the goal of exploring only few representative traces from each class.
We introduce a new equivalence on traces under sequential consistency semantics, which we call the observation equivalence. Two traces are observationally equivalent if every read event observes the same write event in both traces. While the traditional Mazurkiewicz equivalence is control-centric, our new definition is data-centric. We show that our observation equivalence is coarser than the Mazurkiewicz equivalence, and in many cases even exponentially coarser. We devise a DPOR exploration of the trace space, called data-centric DPOR, based on the observation equivalence.
1. For acyclic architectures, our algorithm is guaranteed to explore exactly one representative trace from each observation class, while spending polynomial time per class. Hence, our algorithm is optimal wrt the observation equivalence, and in several cases explores exponentially fewer traces than any enumerative method based on the Mazurkiewicz equivalence.
2. For cyclic architectures, we consider an equivalence between traces which is finer than the observation equivalence; but coarser than the Mazurkiewicz equivalence, and in some cases is exponentially coarser. Our data-centric DPOR algorithm remains optimal under this trace equivalence.
Finally, we perform a basic experimental comparison between the existing Mazurkiewicz-based DPOR and our data-centric DPOR on a set of academic benchmarks. Our results show a significant reduction in both running time and the number of explored equivalence classes.},
author = {Chalupa, Marek and Chatterjee, Krishnendu and Pavlogiannis, Andreas and Sinha, Nishant and Vaidya, Kapil},
issn = {2664-1690},
pages = {36},
publisher = {IST Austria},
title = {{Data-centric dynamic partial order reduction}},
doi = {10.15479/AT:IST-2017-872-v1-1},
year = {2017},
}
@article{548,
abstract = {In this work maximum entropy distributions in the space of steady states of metabolic networks are considered upon constraining the first and second moments of the growth rate. Coexistence of fast and slow phenotypes, with bimodal flux distributions, emerges upon considering control on the average growth (optimization) and its fluctuations (heterogeneity). This is applied to the carbon catabolic core of Escherichia coli where it quantifies the metabolic activity of slow growing phenotypes and it provides a quantitative map with metabolic fluxes, opening the possibility to detect coexistence from flux data. A preliminary analysis on data for E. coli cultures in standard conditions shows degeneracy for the inferred parameters that extend in the coexistence region.},
author = {De Martino, Daniele},
issn = {24700045},
journal = {Physical Review E},
number = {6},
publisher = {American Physiological Society},
title = {{Maximum entropy modeling of metabolic networks by constraining growth-rate moments predicts coexistence of phenotypes}},
doi = {10.1103/PhysRevE.96.060401},
volume = {96},
year = {2017},
}
@inproceedings{549,
abstract = {Model checking is usually based on a comprehensive traversal of the state space. Causality-based model checking is a radically different approach that instead analyzes the cause-effect relationships in a program. We give an overview on a new class of model checking algorithms that capture the causal relationships in a special data structure called concurrent traces. Concurrent traces identify key events in an execution history and link them through their cause-effect relationships. The model checker builds a tableau of concurrent traces, where the case splits represent different causal explanations of a hypothetical error. Causality-based model checking has been implemented in the ARCTOR tool, and applied to previously intractable multi-threaded benchmarks.},
author = {Finkbeiner, Bernd and Kupriyanov, Andrey},
booktitle = {Electronic Proceedings in Theoretical Computer Science},
issn = {20752180},
location = {Uppsala, Sweden},
pages = {31 -- 38},
publisher = {Open Publishing Association},
title = {{Causality-based model checking}},
doi = {10.4204/EPTCS.259.3},
volume = {259},
year = {2017},
}
@article{550,
abstract = {For large random matrices X with independent, centered entries but not necessarily identical variances, the eigenvalue density of XX* is well-approximated by a deterministic measure on ℝ. We show that the density of this measure has only square and cubic-root singularities away from zero. We also extend the bulk local law in [5] to the vicinity of these singularities.},
author = {Alt, Johannes},
issn = {1083589X},
journal = {Electronic Communications in Probability},
publisher = {Institute of Mathematical Statistics},
title = {{Singularities of the density of states of random Gram matrices}},
doi = {10.1214/17-ECP97},
volume = {22},
year = {2017},
}
@inproceedings{551,
abstract = {Evolutionary graph theory studies the evolutionary dynamics in a population structure given as a connected graph. Each node of the graph represents an individual of the population, and edges determine how offspring are placed. We consider the classical birth-death Moran process where there are two types of individuals, namely, the residents with fitness 1 and mutants with fitness r. The fitness indicates the reproductive strength. The evolutionary dynamics happens as follows: in the initial step, in a population of all resident individuals a mutant is introduced, and then at each step, an individual is chosen proportional to the fitness of its type to reproduce, and the offspring replaces a neighbor uniformly at random. The process stops when all individuals are either residents or mutants. The probability that all individuals in the end are mutants is called the fixation probability, which is a key factor in the rate of evolution. We consider the problem of approximating the fixation probability. The class of algorithms that is extremely relevant for approximation of the fixation probabilities is the Monte-Carlo simulation of the process. Previous results present a polynomial-time Monte-Carlo algorithm for undirected graphs when r is given in unary. First, we present a simple modification: instead of simulating each step, we discard ineffective steps, where no node changes type (i.e., either residents replace residents, or mutants replace mutants). Using the above simple modification and our result that the number of effective steps is concentrated around the expected number of effective steps, we present faster polynomial-time Monte-Carlo algorithms for undirected graphs. Our algorithms are always at least a factor O(n2/ log n) faster as compared to the previous algorithms, where n is the number of nodes, and is polynomial even if r is given in binary. We also present lower bounds showing that the upper bound on the expected number of effective steps we present is asymptotically tight for undirected graphs. },
author = {Chatterjee, Krishnendu and Ibsen-Jensen, Rasmus and Nowak, Martin},
booktitle = {Leibniz International Proceedings in Informatics},
isbn = {978-395977046-0},
location = {Aalborg, Denmark},
publisher = {Schloss Dagstuhl - Leibniz-Zentrum für Informatik},
title = {{Faster Monte Carlo algorithms for fixation probability of the Moran process on undirected graphs}},
doi = {10.4230/LIPIcs.MFCS.2017.61},
volume = {83},
year = {2017},
}
@inproceedings{552,
abstract = {Graph games provide the foundation for modeling and synthesis of reactive processes. Such games are played over graphs where the vertices are controlled by two adversarial players. We consider graph games where the objective of the first player is the conjunction of a qualitative objective (specified as a parity condition) and a quantitative objective (specified as a meanpayoff condition). There are two variants of the problem, namely, the threshold problem where the quantitative goal is to ensure that the mean-payoff value is above a threshold, and the value problem where the quantitative goal is to ensure the optimal mean-payoff value; in both cases ensuring the qualitative parity objective. The previous best-known algorithms for game graphs with n vertices, m edges, parity objectives with d priorities, and maximal absolute reward value W for mean-payoff objectives, are as follows: O(nd+1 . m . w) for the threshold problem, and O(nd+2 · m · W) for the value problem. Our main contributions are faster algorithms, and the running times of our algorithms are as follows: O(nd-1 · m ·W) for the threshold problem, and O(nd · m · W · log(n · W)) for the value problem. For mean-payoff parity objectives with two priorities, our algorithms match the best-known bounds of the algorithms for mean-payoff games (without conjunction with parity objectives). Our results are relevant in synthesis of reactive systems with both functional requirement (given as a qualitative objective) and performance requirement (given as a quantitative objective).},
author = {Chatterjee, Krishnendu and Henzinger, Monika and Svozil, Alexander},
booktitle = {Leibniz International Proceedings in Informatics},
isbn = {978-395977046-0},
location = {Aalborg, Denmark},
publisher = {Schloss Dagstuhl - Leibniz-Zentrum für Informatik},
title = {{Faster algorithms for mean payoff parity games}},
doi = {10.4230/LIPIcs.MFCS.2017.39},
volume = {83},
year = {2017},
}
@inproceedings{553,
abstract = {We consider two player, zero-sum, finite-state concurrent reachability games, played for an infinite number of rounds, where in every round, each player simultaneously and independently of the other players chooses an action, whereafter the successor state is determined by a probability distribution given by the current state and the chosen actions. Player 1 wins iff a designated goal state is eventually visited. We are interested in the complexity of stationary strategies measured by their patience, which is defined as the inverse of the smallest non-zero probability employed. Our main results are as follows: We show that: (i) the optimal bound on the patience of optimal and -optimal strategies, for both players is doubly exponential; and (ii) even in games with a single non-absorbing state exponential (in the number of actions) patience is necessary. },
author = {Chatterjee, Krishnendu and Hansen, Kristofer and Ibsen-Jensen, Rasmus},
booktitle = {Leibniz International Proceedings in Informatics},
isbn = {978-395977046-0},
location = {Aalborg, Denmark},
publisher = {Schloss Dagstuhl - Leibniz-Zentrum für Informatik},
title = {{Strategy complexity of concurrent safety games}},
doi = {10.4230/LIPIcs.MFCS.2017.55},
volume = {83},
year = {2017},
}
@misc{5559,
abstract = {Strong amplifiers of natural selection},
author = {Pavlogiannis, Andreas and Tkadlec, Josef and Chatterjee, Krishnendu and Nowak , Martin},
keywords = {natural selection},
publisher = {IST Austria},
title = {{Strong amplifiers of natural selection}},
doi = {10.15479/AT:ISTA:51},
year = {2017},
}
@misc{5560,
abstract = {This repository contains the data collected for the manuscript "Biased partitioning of the multi-drug efflux pump AcrAB-TolC underlies long-lived phenotypic heterogeneity".
The data is compressed into a single archive. Within the archive, different folders correspond to figures of the main text and the SI of the related publication.
Data is saved as plain text, with each folder containing a separate readme file describing the format. Typically, the data is from fluorescence microscopy measurements of single cells growing in a microfluidic "mother machine" device, and consists of relevant values (primarily arbitrary unit or normalized fluorescence measurements, and division times / growth rates) after raw microscopy images have been processed, segmented, and their features extracted, as described in the methods section of the related publication.},
author = {Bergmiller, Tobias and Andersson, Anna M and Tomasek, Kathrin and Balleza, Enrique and Kiviet, Daniel and Hauschild, Robert and Tkacik, Gasper and Guet, Calin C},
keywords = {single cell microscopy, mother machine microfluidic device, AcrAB-TolC pump, multi-drug efflux, Escherichia coli},
publisher = {IST Austria},
title = {{Biased partitioning of the multi-drug efflux pump AcrAB-TolC underlies long-lived phenotypic heterogeneity}},
doi = {doi:10.15479/AT:ISTA:53},
year = {2017},
}
@misc{5561,
abstract = {Graph matching problems as described in "Active Graph Matching for Automatic Joint Segmentation and Annotation of C. Elegans." by Kainmueller, Dagmar and Jug, Florian and Rother, Carsten and Myers, Gene, MICCAI 2014. Problems are in OpenGM2 hdf5 format (see http://hciweb2.iwr.uni-heidelberg.de/opengm/) and a custom text format used by the feature matching solver described in "Feature Correspondence via Graph Matching: Models and Global Optimization." by Lorenzo Torresani, Vladimir Kolmogorov and Carsten Rother, ECCV 2008, code at http://pub.ist.ac.at/~vnk/software/GraphMatching-v1.02.src.zip. },
author = {Kainmueller, Dagmar and Jug, Florian and Rother, Carsten and Meyers, Gene},
keywords = {graph matching, feature matching, QAP, MAP-inference},
publisher = {IST Austria},
title = {{Graph matching problems for annotating C. Elegans}},
doi = {10.15479/AT:ISTA:57},
year = {2017},
}
@misc{5562,
abstract = {This data was collected as part of the study [1]. It consists of preprocessed multi-electrode array recording from 160 salamander retinal ganglion cells responding to 297 repeats of a 19 s natural movie. The data is available in two formats: (1) a .mat file containing an array with dimensions “number of repeats” x “number of neurons” x “time in a repeat”; (2) a zipped .txt file containing the same data represented as an array with dimensions “number of neurons” x “number of samples”, where the number of samples is equal to the product of the number of repeats and timebins within a repeat. The time dimension is divided into 20 ms time windows, and the array is binary indicating whether a given cell elicited at least one spike in a given time window during a particular repeat. See the reference below for details regarding collection and preprocessing:
[1] Tkačik G, Marre O, Amodei D, Schneidman E, Bialek W, Berry MJ II. Searching for Collective Behavior in a Large Network of Sensory Neurons. PLoS Comput Biol. 2014;10(1):e1003408.},
author = {Marre, Olivier and Tkacik, Gasper and Amodei, Dario and Schneidman, Elad and Bialek, William and Berry, Michael},
keywords = {multi-electrode recording, retinal ganglion cells},
publisher = {IST Austria},
title = {{Multi-electrode array recording from salamander retinal ganglion cells}},
doi = {10.15479/AT:ISTA:61},
year = {2017},
}
@misc{5563,
abstract = {MATLAB code and processed datasets available for reproducing the results in:
Lukačišin, M.*, Landon, M.*, Jajoo, R*. (2016) Sequence-Specific Thermodynamic Properties of Nucleic Acids Influence Both Transcriptional Pausing and Backtracking in Yeast.
*equal contributions},
author = {Lukacisin, Martin},
publisher = {IST Austria},
title = {{MATLAB analysis code for 'Sequence-Specific Thermodynamic Properties of Nucleic Acids Influence Both Transcriptional Pausing and Backtracking in Yeast'}},
doi = {10.15479/AT:ISTA:64},
year = {2017},
}
@misc{5564,
abstract = {Compressed Fastq files with whole-genome sequencing data of IS-wt strain D and clones from four evolved populations (A11, C08, C10, D08). Information on this data collection is available in the Methods Section of the primary publication.},
author = {Steinrück, Magdalena and Guet, Calin C},
publisher = {IST Austria},
title = {{Fastq files for "Complex chromosomal neighborhood effects determine the adaptive potential of a gene under selection"}},
doi = {10.15479/AT:ISTA:65},
year = {2017},
}
@misc{5565,
abstract = {One of the key questions in understanding plant development is how single cells behave in a larger context of the tissue. Therefore, it requires the observation of the whole organ with a high spatial- as well as temporal resolution over prolonged periods of time, which may cause photo-toxic effects. This protocol shows a plant sample preparation method for light-sheet microscopy, which is characterized by mounting the plant vertically on the surface of a gel. The plant is mounted in such a way that the roots are submerged in a liquid medium while the leaves remain in the air. In order to ensure photosynthetic activity of the plant, a custom-made lighting system illuminates the leaves. To keep the roots in darkness the water surface is covered with sheets of black plastic foil. This method allows long-term imaging of plant organ development in standardized conditions.
The Video is licensed under a CC BY NC ND license. },
author = {Von Wangenheim, Daniel and Hauschild, Robert and Friml, Jirí},
publisher = {IST Austria},
title = {{Light Sheet Fluorescence microscopy of plant roots growing on the surface of a gel}},
doi = {10.15479/AT:ISTA:66},
year = {2017},
}
@misc{5566,
abstract = {Current minimal version of TipTracker},
author = {Hauschild, Robert},
keywords = {tool, tracking, confocal microscopy},
publisher = {IST Austria},
title = {{Live tracking of moving samples in confocal microscopy for vertically grown roots}},
doi = {10.15479/AT:ISTA:69},
year = {2017},
}
@misc{5567,
abstract = {Immunological synapse DC-Tcells},
author = {Leithner, Alexander F},
keywords = {Immunological synapse},
publisher = {IST Austria},
title = {{Immunological synapse DC-Tcells}},
doi = {10.15479/AT:ISTA:71},
year = {2017},
}
@misc{5568,
abstract = {Includes source codes, test cases, and example data used in the thesis Brittle Fracture Simulation with Boundary Elements for Computer Graphics. Also includes pre-built binaries of the HyENA library, but not sources - please contact the HyENA authors to obtain these sources if required (https://mech.tugraz.at/hyena)},
author = {Hahn, David},
keywords = {Boundary elements, brittle fracture, computer graphics, fracture simulation},
publisher = {IST Austria},
title = {{Source codes: Brittle fracture simulation with boundary elements for computer graphics}},
doi = {10.15479/AT:ISTA:73},
year = {2017},
}
@article{557,
abstract = {PURPOSE. Gene therapy of retinal ganglion cells (RGCs) has promise as a powerful therapeutic for the rescue and regeneration of these cells after optic nerve damage. However, early after damage, RGCs undergo atrophic changes, including gene silencing. It is not known if these changes will deleteriously affect transduction and transgene expression, or if the therapeutic protein can influence reactivation of the endogenous genome. METHODS. Double-transgenic mice carrying a Rosa26-(LoxP)-tdTomato reporter, and a mutant allele for the proapoptotic Bax gene were reared. The Bax mutant blocks apoptosis, but RGCs still exhibit nuclear atrophy and gene silencing. At times ranging from 1 hour to 4 weeks after optic nerve crush (ONC), eyes received an intravitreal injection of AAV2 virus carrying the Cre recombinase. Successful transduction was monitored by expression of the tdTomato reporter. Immunostaining was used to localize tdTomato expression in select cell types. RESULTS. Successful transduction of RGCs was achieved at all time points after ONC using AAV2 expressing Cre from the phosphoglycerate kinase (Pgk) promoter, but not the CMV promoter. ONC promoted an increase in the transduction of cell types in the inner nuclear layer, including Müller cells and rod bipolar neurons. There was minimal evidence of transduction of amacrine cells and astrocytes in the inner retina or optic nerve. CONCLUSIONS. Damaged RGCs can be transduced and at least some endogenous genes can be subsequently activated. Optic nerve damage may change retinal architecture to allow greater penetration of an AAV2 virus to transduce several additional cell types in the inner nuclear layer.},
author = {Nickells, Robert and Schmitt, Heather and Maes, Margaret E and Schlamp, Cassandra},
issn = {01460404},
journal = {Investigative Ophthalmology and Visual Science},
number = {14},
pages = {6091 -- 6104},
publisher = {Association for Research in Vision and Ophthalmology Inc.},
title = {{AAV2 mediated transduction of the mouse retina after optic nerve injury}},
doi = {10.1167/iovs.17-22634},
volume = {58},
year = {2017},
}
@misc{5570,
abstract = {Matlab script to calculate the forward migration indexes (/) from TrackMate spot-statistics files.},
author = {Hauschild, Robert},
keywords = {Cell migration, tracking, forward migration index, FMI},
publisher = {IST Austria},
title = {{Forward migration indexes}},
doi = {10.15479/AT:ISTA:75},
year = {2017},
}