@inproceedings{3885,
abstract = {The theory of graph games with ω-regular winning conditions is the foundation for modeling and synthesizing reactive processes. In the case of stochastic reactive processes, the corresponding stochastic graph games have three players, two of them (System and Environment) behaving adversarially, and the third (Uncertainty) behaving probabilistically. We consider two problems for stochastic graph games: the qualitative problem asks for the set of states from which a player can win with probability 1 (almost-sure winning); and the quantitative problem asks for the maximal probability of winning (optimal winning) from each state. We consider ω-regular winning conditions formalized as Müller winning conditions. We present optimal memory bounds for pure almost-sure winning and optimal winning strategies in stochastic graph games with Müller winning conditions. We also present improved memory bounds for randomized almost-sure winning and optimal strategies.},
author = {Krishnendu Chatterjee},
pages = {138 -- 152},
publisher = {Springer},
title = {{Optimal strategy synthesis in stochastic Müller games}},
doi = {10.1007/978-3-540-71389-0_11},
volume = {4423},
year = {2007},
}
@inproceedings{3886,
abstract = {The theory of graph games with ω-regular winning conditions is the foundation for modeling and synthesizing reactive processes. In the case of stochastic reactive processes, the corresponding stochastic graph games have three players, two of them (System and Environment) behaving adversarially, and the third (Uncertainty) behaving probabilistically. We consider two problems for stochastic graph games: the qualitative problem asks for the set of states from which a player can win with probability 1 (almost-sure winning); and the quantitative problem asks for the maximal probability of winning (optimal winning) from each state. We consider ω-regular winning conditions formalized as Müller winning conditions. We show that both the qualitative and quantitative problem for stochastic Müller games are PSPACE-complete. We also consider two well-known sub-classes of Müller objectives, namely, upward-closed and union-closed objectives, and show that both the qualitative and quantitative problem for these sub-classes are coNP-complete.},
author = {Krishnendu Chatterjee},
pages = {436 -- 448},
publisher = {Schloss Dagstuhl - Leibniz-Zentrum für Informatik},
title = {{Stochastic Müller games are PSPACE-complete}},
doi = {10.1007/978-3-540-77050-3_36},
volume = {4855},
year = {2007},
}
@inproceedings{3887,
abstract = {We consider Markov decision processes (MDPs) with multiple long-run average objectives. Such MDPs occur in design problems where one wishes to simultaneously optimize several criteria, for example, latency and power. The possible trade-offs between the different objectives are characterized by the Pareto curve. We show that every Pareto optimal point can be epsilon-approximated by a memoryless strategy, for all epsilon > 0. In contrast to the single-objective case, the memoryless strategy may require randomization. We show that the Pareto curve can be approximated (a) in polynomial time in the size of the MDP for irreducible MDPs; and (b) in polynomial space in the size of the MDP for all MDPs. Additionally, we study the problem if a given value vector is realizable by any strategy, and show that it can be decided in polynomial time for irreducible MDPs and in NP for all MDPs. These results provide algorithms for design exploration in MDP models with multiple long-run average objectives.},
author = {Krishnendu Chatterjee},
pages = {473 -- 484},
publisher = {Schloss Dagstuhl - Leibniz-Zentrum für Informatik},
title = {{Markov decision processes with multiple long-run average objectives}},
doi = {10.1007/978-3-540-77050-3_39},
volume = {4855},
year = {2007},
}
@article{3909,
abstract = {Social insect colonies have evolved collective immune defences against parasites. These ‘social immune systems’ result from the cooperation of the individual group members to combat the increased risk of disease transmission that arises from sociality and group living. In this review we illustrate the pathways that parasites can take to infect a social insect colony and use these pathways as a framework to predict colony defence mechanisms and present the existing evidence. We find that the collective defences can be both prophylactic and activated on demand and consist of behavioural, physiological and organisational adaptations of the colony that prevent parasite entrance, establishment and spread. We discuss the regulation of collective immunity, which requires complex integration of information about both the parasites and the internal status of the insect colony. Our review concludes with an examination of the evolution of social immunity, which is based on the consequences of selection at both the individual and the colony level.},
author = {Cremer, Sylvia and Armitage, Sophie and Schmid Hempel, Paul},
journal = {Current Biology},
number = {16},
pages = {R693 -- R702},
publisher = {Cell Press},
title = {{Social immunity}},
doi = {10.1016/j.cub.2007.06.008},
volume = {17},
year = {2007},
}
@article{3910,
author = {Hughes, David and Cremer, Sylvia},
journal = {Animal Behaviour},
number = {5},
pages = {1593 -- 1599},
publisher = {Elsevier},
title = {{Plasticity in anti-parasite behaviours and its suggested role in invasion biology}},
doi = {10.1016/j.anbehav.2006.12.025},
volume = {74},
year = {2007},
}
@article{3911,
abstract = {Life in a social group increases the risk of disease transmission. To counteract this threat, social insects have evolved manifold antiparasite defenses, ranging from social exclusion of infected group members to intensive care. It is generally assumed that individuals performing hygienic behaviors risk infecting themselves, suggesting a high direct cost of helping. Our work instead indicates the opposite for garden ants. Social contact with individual workers, which were experimentally exposed to a fungal parasite, provided a clear survival benefit to nontreated, naive group members upon later challenge with the same parasite. This first demonstration of contact immunity in Social Hymenoptera and complementary results from other animal groups and plants suggest its general importance in both antiparasite and antiherbivore defense. In addition to this physiological prophylaxis of adult ants, infection of the brood was prevented in our experiment by behavioral changes of treated and naive workers. Parasite-treated ants stayed away from the brood chamber, whereas their naive nestmates increased brood-care activities. Our findings reveal a direct benefit for individuals to perform hygienic behaviors toward others, and this might explain the widely observed maintenance of social cohesion under parasite attack in insect societies.},
author = {Ugelvig, Line V and Cremer, Sylvia},
journal = {Current Biology},
number = {22},
pages = {1967 -- 1971},
publisher = {Cell Press},
title = {{Social prophylaxis: group interaction promotes collective immunity in ant colonies}},
doi = {10.1016/j.cub.2007.10.029},
volume = {17},
year = {2007},
}
@article{3937,
abstract = {Lymphocyte motility in lymph nodes is regulated by chemokines, but the contribution of integrins to this motility remains obscure. Here we examined lymphocyte migration over CCR7-binding chemokines that 'decorate' lymph node stroma. In a shear-free environment, surface-bound lymph node chemokines but not their soluble counterparts promoted robust and sustained T lymphocyte motility. The chemokine CCL21 induced compartmentalized clustering of the integrins LFA-1 and VLA-4 in motile lymphocytes, but both integrins remained nonadhesive to ligands on lymphocytes, dendritic cells and stroma. The application of shear stress to lymphocytes interacting with CCL21 and integrin ligands promoted robust integrin-mediated adhesion. Thus, lymph node chemokines that promote motility and strongly activate lymphocyte integrins under shear forces fail to stimulate stable integrin adhesiveness in extravascular shear-free environments.},
author = {Woolf, Eilon and Grigorova, Irina and Sagiv, Adi and Grabovsky, Valentin and Feigelson, Sara W and Shulman, Ziv and Hartmann, Tanja and Michael Sixt and Cyster, Jason G and Alon, Ronen},
journal = {Nature Immunology},
number = {10},
pages = {1076 -- 1085},
publisher = {Nature Publishing Group},
title = {{Lymph node chemokines promote sustained T lymphocyte motility without triggering stable integrin adhesiveness in the absence of shear forces}},
doi = {10.1038/ni1499},
volume = {8},
year = {2007},
}
@article{3938,
abstract = {RhoH is a small GTPase expressed only in the hematopoietic system. With the use of mice with targeted disruption of the RhoH gene, we demonstrated that RhoH is crucial for thymocyte maturation during DN3 to DN4 transition and during positive selection. Furthermore, the differentiation and expansion of DN3 and DN4 thymocytes in vitro were severely impaired. These defects corresponded to defective TCR signaling. Although RhoH is not required for TCR-induced activation of ZAP70 and ZAP70-mediated activation of p38, it is crucial for the tyrosine phosphorylation of LAT, PLCgamma1, and Vav1 and for the activation of Erk and calcium influx. These data suggest that RhoH is important for pre-TCR and TCR signaling because it allows the efficient interaction of ZAP70 with the LAT signalosome, thus regulating thymocyte development.},
author = {Dorn, Tatjana and Kuhn, Ursula and Bungartz, Gerd and Stiller, Sebastian and Bauer, Martina and Ellwart, Joachim and Peters, Thorsten and Scharffetter-Kochanek, Karin and Semmrich, Monika and Laschinger, Melanie and Holzmann, Bernhard and Klinkert, Wolfgang E and Straten, Per Thor and Køllgaard, Tania and Michael Sixt and Brakebusch, Cord},
journal = {Blood},
number = {6},
pages = {2346 -- 2355},
publisher = {American Society of Hematology},
title = {{RhoH is important for positive thymocyte selection and T-cell receptor signaling}},
doi = {10.1182/blood-2006-04-019034},
volume = {109},
year = {2007},
}
@article{3972,
abstract = {The persistence diagram of a real-valued function on a topological space is a multiset of points in the extended plane. We prove that under mild assumptions on the function, the persistence diagram is stable: small changes in the function imply only small changes in the diagram. We apply this result to estimating the homology of sets in a metric space and to comparing and classifying geometric shapes.},
author = {Cohen-Steiner, David and Herbert Edelsbrunner and Harer, John},
journal = {Discrete & Computational Geometry},
number = {1},
pages = {103 -- 120},
publisher = {Springer},
title = {{Stability of persistence diagrams}},
doi = {10.1007/s00454-006-1276-5},
volume = {37},
year = {2007},
}
@article{3973,
abstract = {In this paper we bound the difference between the total mean curvatures of two closed surfaces in R-3 in terms of their total absolute curvatures and the Frechet distance between the volumes they enclose. The proof relies on a combination of methods from algebraic topology and integral geometry. We also bound the difference between the lengths of two curves using the same methods.},
author = {Cohen-Steiner, David and Herbert Edelsbrunner},
journal = {Foundations of Computational Mathematics},
number = {4},
pages = {391 -- 404},
publisher = {Springer},
title = {{Inequalities for the curvature of curves and surfaces}},
doi = {10.1007/s10208-005-0200-3},
volume = {7},
year = {2007},
}
@inproceedings{3975,
abstract = {We study the reconstruction of a stratified space from a possibly noisy point sample. Specifically, we use the vineyard of the distance function restricted to a I-parameter family of neighborhoods of a point to assess the local homology of the stratified space at that point. We prove the correctness of this assessment under the assumption of a sufficiently dense sample. We also give an algorithm that constructs the vineyard and makes the local assessment in time at most cubic in the size of the Delaunay triangulation of the point sample.},
author = {Paul Bendich and Cohen-Steiner, David and Herbert Edelsbrunner and Harer, John and Morozov, Dmitriy},
pages = {536 -- 546},
publisher = {IEEE},
title = {{Inferring local homology from sampled stratified spaces}},
doi = {10.1109/FOCS.2007.33},
year = {2007},
}
@article{3976,
abstract = {Herein, we study the interfaces of a set of 146 transient protein-protein interfaces in order to better understand the principles of their interactions. We define and generate the protein interface using tools from computational geometry and topology and then apply statistical analysis to its residue composition. In addition to counting individual occurrences, we evaluate pairing preferences, both across and as neighbors on one side of an interface. Likelihood correction emphasizes novel and unexpected pairs, such as the His-Cys pair found in most complexes of serine proteases with their diverse inhibitors and the Met-Met neighbor pair found in unrelated protein interfaces. We also present a visualization of the protein interface that allows for facile identification of residue-residue contacts and other biochemical properties.},
author = {Headd, Jeffrey J and Ban, Y E Andrew and Brown, Paul and Herbert Edelsbrunner and Vaidya, Madhuwanti and Rudolph, Johannes},
journal = {Journal of Proteome Research},
number = {7},
pages = {2576 -- 2586},
publisher = {American Chemical Society},
title = {{Protein-protein interfaces: Properties, preferences, and projections}},
doi = {10.1021/pr070018+},
volume = {6},
year = {2007},
}
@article{3977,
abstract = {Using inclusion-exclusion, we can write the indicator function of a union of finitely many balls as an alternating sum of indicator functions of common intersections of balls. We exhibit abstract simplicial complexes that correspond to minimal inclusion-exclusion formulas. They include the dual complex, as defined in [3], and are characterized by the independence of their simplices and by geometric realizations with the same underlying space as the dual complex.},
author = {Attali, Dominique and Herbert Edelsbrunner},
journal = {Discrete & Computational Geometry},
number = {1},
pages = {59 -- 77},
publisher = {Springer},
title = {{Inclusion-exclusion formulas from independent complexes}},
doi = {10.1007/s00454-006-1274-7},
volume = {37},
year = {2007},
}
@inproceedings{3981,
abstract = {Building on the work of Martinetz, Schulten and de Silva, Carlsson, we introduce a 2-parameter family of witness complexes and algorithms for constructing them. This family can be used to determine the gross topology of point cloud data in R-d or other metric spaces. The 2-parameter family is sensitive to differences in sampling density and thus amenable to detecting patterns within the data set. It also lends itself to theoretical analysis. For example, we can prove that in the limit, when the witnesses cover the entire domain, witness complexes in the family that share the first, scale parameter have the same homotopy type.},
author = {Attali, Dominique and Herbert Edelsbrunner and Harer, John and Mileyko, Yuriy},
pages = {386 -- 397},
publisher = {Springer},
title = {{Alpha-beta witness complexes}},
doi = {10.1007/978-3-540-73951-7_34},
volume = {4619},
year = {2007},
}
@article{4152,
abstract = {Gastrulation is a morphogenetic process that results in the formation of the embryonic germ layers. Here we detail the major cell movements that occur during zebrafish gastrulation: epiboly, internalization, and convergent extension. Although gastrulation is known to be regulated by signaling pathways such as the Wnt/planar cell polarity pathway, many questions remain about the underlying molecular and cellular mechanisms. Key factors that may play a role in gastrulation cell movements are cell adhesion and cytoskeletal rearrangement. In addition, some of the driving force for gastrulation may derive from tissue interactions such as those described between the enveloping layer and the yolk syncytial layer. Future exploration of gastrulation mechanisms relies on the development of sensitive and quantitative techniques to characterize embryonic germ-layer properties.},
author = {Rohde, Laurel and Heisenberg, Carl-Philipp J},
journal = {International Review of Cytology - A Survey of Cell Biology},
pages = {159 -- 192},
publisher = {Academic Press},
title = {{Zebrafish gastrulation: Cell movements, signals, and mechanisms}},
doi = {10.1016/S0074-7696(07)61004-3},
volume = {261},
year = {2007},
}
@article{4182,
abstract = {We are interested in the cellular and molecular mechanisms underlying tissue morphogenesis during zebrafish gastrulation. Both differential cell adhesion and contractility have been proposed to be key mechanisms by which tissues form and rearrange in development. To obtain insight into the potential roles of differential cell adhesion and contraction for germ layer morphogenesis during gastrulation, we are analyzing cell adhesion and contraction of germ layer progenitor cells using atomic force microscopy, primary tissue culture and transplantation assays. I will present and discuss data about the differential adhesiveness and contractility of germ layer progenitor cells in the context of germ layer formation during vertebrate gastrulation.},
author = {Krieg, Michael and Arboleda, Yohanna and Müller, Daniel and Heisenberg, Carl-Philipp J},
journal = {European Journal of Cell Biology},
number = {Supplement 1},
pages = {39 -- 39},
publisher = {Elsevier},
title = {{The role of cell adhesion and contractility for germ layer morphogenesis during zebrafish gastrulation}},
doi = {10.1016/j.ejcb.2007.02.002},
volume = {86},
year = {2007},
}
@article{4205,
abstract = {Background: Bone morphogenetic proteins (Bmps) are required for the specification of ventrolateral cell fates during embryonic dorsoventral patterning and for proper convergence and extension gastrulation movements, but the mechanisms underlying the latter role remained elusive. Results: Via bead implantations, we show that the Bmp gradient determines the direction of lateral mesodermal cell migration during dorsal convergence in the zebrafish gastrula. This effect is independent of its role during dorsoventral patterning and of noncanonical Wnt signaling. However, it requires Bmp signal transduction through AIk8 and Smad5 to negatively regulate Ca2+/Cadherin-dependent cell-cell adhesiveness. In vivo, converging mesodermal cells form lamellipodia that attach to adjacent cells. Bmp signaling diminishes the Cadherin-dependent stability of such contact points, thereby abrogating subsequent cell displacement during lamellipodial retraction. Conclusions: We propose that the ventral-to-dorsal Bmp gradient has an instructive role to establish a reverse gradient of cell-cell adhesiveness, thereby defining different migratory zones and directing lamellipodia-driven cell migrations during dorsal convergence in lateral regions of the zebrafish gastrula.},
author = {Von Der Hardt, Sophia and Bakkers, Jeroen and Inbal, Adi and Carvalho, Lara and Solnica Krezel, Lilianna and Heisenberg, Carl-Philipp J and Hammerschmidt, Matthias},
journal = {Current Biology},
number = {6},
pages = {475 -- 487},
publisher = {Cell Press},
title = {{The Bmp gradient of the zebrafish gastrula guides migrating lateral cells by regulating cell-cell adhesion}},
doi = {10.1016/j.cub.2007.02.013},
volume = {17},
year = {2007},
}
@article{4225,
abstract = {The discovery of the genetic code was one of the most important advances of modern biology. But there is more to a DNA code than protein sequence; DNA carries signals for splicing, localization, folding, and regulation that are often embedded within the protein-coding sequence. In this issue, Itzkovitz and Alon show that the specific 64-to-20 mapping found in the genetic code may have been optimized for permitting protein-coding regions to carry this extra information and suggest that this property may have evolved as a side benefit of selection to minimize the negative effects of frameshift errors.},
author = {Bollenbach, Mark Tobias and Vetsigian, Kalin and Kishony, Roy},
journal = {Genome Research},
number = {4},
pages = {401 -- 404},
publisher = {Cold Spring Harbor Laboratory Press},
title = {{Evolution and multilevel optimization of the genetic code}},
doi = {10.1101/gr.6144007},
volume = {17},
year = {2007},
}
@article{4226,
abstract = {In the developing fly wing, secreted morphogens such as Decapentaplegic (Dpp) and Wingless (Wg) form gradients of concentration providing positional information. Dpp forms a longer-range gradient than Wg. To understand how the range is controlled, we measured the four key kinetic parameters governing morphogen spreading: the production rate, the effective diffusion coefficient, the degradation rate, and the immobile fraction. The four parameters had different values for Dpp versus Wg. In addition, Dynamin-dependent endocytosis was required for spreading of Dpp, but not Wg. Thus, the cellular mechanisms of Dpp and Wingless spreading are different: Dpp spreading requires endocytic, intracellular trafficking.},
author = {Anna Kicheva and Pantazis, Periklis and Bollenbach, Tobias and Kalaidzidis, Yannis and Bittig, Thomas and Julicher, Frank and Gonzalez-Gaitan, Marcos},
journal = {Science},
number = {5811},
pages = {521 -- 525},
publisher = {American Association for the Advancement of Science},
title = {{Kinetics of morphogen gradient formation}},
doi = {10.1126/science.1135774},
volume = {315},
year = {2007},
}
@inproceedings{4233,
author = {Harold Vladar},
editor = {Falcón,N. and Loyo de Sardi,Y.},
pages = {91 -- 109},
publisher = {Consejo de Desarrollo Cientifico y Tecnologico},
title = {{Alternativas prebióticas para la síntesis de amino- ácidos y otras moléculas relacionadas}},
doi = {3808},
year = {2007},
}
@article{4234,
abstract = {We study a generalised model of population growth in which the state variable is population growth rate instead of population size. Stochastic parametric perturbations, modelling phenotypic variability, lead to a Langevin system with two sources of multiplicative noise. The stationary probability distributions have two characteristic power-law scales. Numerical simulations show that noise suppresses the explosion of the growth rate which occurs in the deterministic counterpart. Instead, in different parameter regimes populations will grow with "anomalous" stochastic rates and (i) stabilise at "random carrying capacities", or (ii) go extinct in random times. Using logistic fits to reconstruct the simulated data, we find that even highly significant estimations do not recover or reflect information about the deterministic part of the process. Therefore, the logistic interpretation is not biologically meaningful. These results have implications for distinct model-aided calculations in biological situations because these kinds of estimations could lead to spurious conclusions. (c) 2006 Elsevier B.V. All rights reserved.},
author = {de Vladar, Harold and Pen, I.},
journal = {Physica A},
pages = {477 -- 485},
publisher = {Elsevier},
title = {{Determinism, noise, and spurious estimations in a generalised model of population growth}},
doi = {10.1016/j.physa.2006.06.025},
volume = {373},
year = {2007},
}
@article{4246,
abstract = {Gaia theory, which describes the life–environment system of the Earth as stable and self-regulating, has remained at the fringes of mainstream biological science owing to its historically inadequate definition and apparent incompatibility with individual-level natural selection. The key issue is whether and why the biosphere might tend towards stability and self-regulation. We review the various ways in which these issues have been addressed by evolutionary and ecological theory, and relate these to ‘Gaia theory’. We then ask how this theory extends the perspectives offered by these disciplines, and how it might be tested by novel modelling approaches and laboratory experiments using emergent technologies.},
author = {Free, Andrew and Nicholas Barton},
journal = {Trends in Ecology and Evolution},
number = {11},
pages = {611 -- 619},
publisher = {Cell Press},
title = {{Do evolution and ecology need the Gaia hypothesis?}},
doi = {10.1016/j.tree.2007.07.007},
volume = {22},
year = {2007},
}
@article{4247,
abstract = {Evolution at multiple gene positions is complicated. Direct selection on one gene disturbs the evolutionary dynamics of associated genes. Recent years have seen the development of a multilocus methodology for modeling evolution at arbitrary numbers of gene positions with arbitrary dominance and epistatic relations, mode of inheritance, genetic linkage, and recombination. We show that the approach is conceptually analogous to social evolutionary methodology, which focuses on selection acting on associated individuals. In doing so, we (1) make explicit the links between the multilocus methodology and the foundations of social evolution theory, namely, Price’s theorem and Hamilton’s rule; (2) relate the multilocus approach to levels‐of‐selection and neighbor‐modulated‐fitness approaches in social evolution; (3) highlight the equivalence between genetical hitchhiking and kin selection; (4) demonstrate that the multilocus methodology allows for social evolutionary analyses involving coevolution of multiple traits and genetical associations between nonrelatives, including individuals of different species; (5) show that this methodology helps solve problems of dynamic sufficiency in social evolution theory; (6) form links between invasion criteria in multilocus systems and Hamilton’s rule of kin selection; (7) illustrate the generality and exactness of Hamilton’s rule, which has previously been described as an approximate, heuristic result.},
author = {Gardner, Andy and West, Stuart A and Nicholas Barton},
journal = {American Naturalist},
number = {2},
pages = {207 -- 226},
publisher = {University of Chicago Press},
title = {{The relation between multilocus population genetics and social evolution theory}},
doi = {10.1086/510602},
volume = {169},
year = {2007},
}
@inproceedings{4342,
abstract = {Library 2.0 and user-generated content are two terms, which are closely connected. In the
presentation, I will briefly define both terms. Two example projects where user- generated content and libraries interact will be presented. The cooperation of Wikipedia and the Personennamendatei, the German cooperative name authority files is the first. The second will be Wikisource where users provide transcribed source material. Another important area of user-generated content is social tagging where users index different resources. And if the users will do so much in the future, is there still a place for librarians? But in the future user
and librarians become partners and the library will provide the platform: the library 2.0.},
author = {Danowski, Patrick},
location = {Durban, South Africa},
publisher = {IFLA},
title = {{Library 2.0 and User-Generated Content - What can the users do for us?}},
doi = {601},
year = {2007},
}
@article{4343,
author = {Patrick Danowski and Pfeifer,Barbara},
journal = {Bibliothek - Forschung Und Praxis},
number = {2},
pages = {149 -- 155},
publisher = {De Gruyter},
title = {{Wikipedia und Normdateien: Wege der Vernetzung am Beispiel der Kooperation mit der Personennamendatei}},
doi = {485},
volume = {31},
year = {2007},
}
@article{4344,
author = {Patrick Danowski and Heller,Lambert},
journal = {Bibliothek - Forschung Und Praxis},
number = {2007},
pages = {130 -- 136},
publisher = {De Gruyter},
title = {{Bibliothek 2.0 ? Wird alles anders?}},
doi = {45},
volume = {31},
year = {2007},
}
@article{4353,
abstract = {BACKGROUND: The invention of the Genome Sequence 20 DNA Sequencing System (454 parallel sequencing platform) has enabled the rapid and high-volume production of sequence data. Until now, however, individual emulsion PCR (emPCR) reactions and subsequent sequencing runs have been unable to combine template DNA from multiple individuals, as homologous sequences cannot be subsequently assigned to their original sources. METHODOLOGY: We use conventional PCR with 5'-nucleotide tagged primers to generate homologous DNA amplification products from multiple specimens, followed by sequencing through the high-throughput Genome Sequence 20 DNA Sequencing System (GS20, Roche/454 Life Sciences). Each DNA sequence is subsequently traced back to its individual source through 5'tag-analysis. CONCLUSIONS: We demonstrate that this new approach enables the assignment of virtually all the generated DNA sequences to the correct source once sequencing anomalies are accounted for (miss-assignment rate<0.4%). Therefore, the method enables accurate sequencing and assignment of homologous DNA sequences from multiple sources in single high-throughput GS20 run. We observe a bias in the distribution of the differently tagged primers that is dependent on the 5' nucleotide of the tag. In particular, primers 5' labelled with a cytosine are heavily overrepresented among the final sequences, while those 5' labelled with a thymine are strongly underrepresented. A weaker bias also exists with regards to the distribution of the sequences as sorted by the second nucleotide of the dinucleotide tags. As the results are based on a single GS20 run, the general applicability of the approach requires confirmation. However, our experiments demonstrate that 5'primer tagging is a useful method in which the sequencing power of the GS20 can be applied to PCR-based assays of multiple homologous PCR products. The new approach will be of value to a broad range of research areas, such as those of comparative genomics, complete mitochondrial analyses, population genetics, and phylogenetics.},
author = {Binladen, Jonas and Gilbert, M Thomas and Jonathan Bollback and Panitz, Frank and Bendixen, Christian and Nielsen, Rasmus and Willerslev, Eske},
journal = {PLoS One},
number = {2},
publisher = {Public Library of Science},
title = {{The use of coded PCR primers enables high-throughput sequencing of multiple homolog amplification products by 454 parallel sequencing}},
doi = {10.1371/journal.pone.0000197},
volume = {2},
year = {2007},
}
@article{4354,
abstract = {Homology search is one of the most ubiquitous bioinformatic tasks, yet it is unknown how effective the currently available tools are for identifying noncoding RNAs (ncRNAs). In this work, we use reliable ncRNA data sets to assess the effectiveness of methods such as BLAST, FASTA, HMMer, and Infernal. Surprisingly, the most popular homology search methods are often the least accurate. As a result, many studies have used inappropriate tools for their analyses. On the basis of our results, we suggest homology search strategies using the currently available tools and some directions for future development.},
author = {Freyhult, Eva K and Jonathan Bollback and Gardner, Paul P},
journal = {Genome Research},
number = {1},
pages = {117 -- 25},
publisher = {Cold Spring Harbor Laboratory Press},
title = {{Exploring genomic dark matter: a critical assessment of the performance of homology search methods on noncoding RNA}},
doi = {10.1101/gr.5890907},
volume = {17},
year = {2007},
}
@article{4355,
abstract = {When a beneficial mutation is fixed in a population that lacks recombination, the genetic background linked to that mutation is fixed. As a result, beneficial mutations on different backgrounds experience competition, or "clonal interference," that can cause asexual populations to evolve more slowly than their sexual counterparts. Factors such as a large population size (N) and high mutation rates (mu) increase the number of competing beneficial mutations, and hence are expected to increase the intensity of clonal interference. However, recent theory suggests that, with very large values of Nmu, the severity of clonal interference may instead decline. The reason is that, with large Nmu, genomes including both beneficial mutations are rapidly created by recurrent mutation, obviating the need for recombination. Here, we analyze data from experimentally evolved asexual populations of a bacteriophage and find that, in these nonrecombining populations with very large Nmu, recurrent mutation does appear to ameliorate this cost of asexuality.},
author = {Jonathan Bollback and Huelsenbeck, John P},
journal = {Molecular Biology and Evolution},
number = {6},
pages = {1397 -- 1406},
publisher = {Oxford University Press},
title = {{Clonal interference is alleviated by high mutation rates in large populations}},
doi = {10.1093/molbev/msm056},
volume = {24},
year = {2007},
}
@article{4356,
abstract = {We used a comparative genomics approach to identify genes that are under positive selection in six strains of Escherichia coli and Shigella flexneri, including five strains that are human pathogens. We find that positive selection targets a wide range of different functions in the E. coli genome, including cell surface proteins such as beta barrel porins, presumably because of the involvement of these genes in evolutionary arms races with other bacteria, phages, and/or the host immune system. Structural mapping of positively selected sites on trans-membrane beta barrel porins reveals that the residues under positive selection occur almost exclusively in the extracellular region of the proteins that are enriched with sites known to be targets of phages, colicins, or the host immune system. More surprisingly, we also find a number of other categories of genes that show very strong evidence for positive selection, such as the enigmatic rhs elements and transposases. Based on structural evidence, we hypothesize that the selection acting on transposases is related to the genomic conflict between transposable elements and the host genome.},
author = {Petersen, Lise and Jonathan Bollback and Dimmic, Matt and Hubisz, Melissa and Nielsen, Rasmus},
journal = {Genome Research},
number = {9},
pages = {1336 -- 1343},
publisher = {Cold Spring Harbor Laboratory Press},
title = {{Genes under positive selection in Escherichia coli}},
doi = {10.1101/gr.6254707},
volume = {17},
year = {2007},
}
@inproceedings{4368,
author = {Dejan Nickovic and Maler, Oded},
pages = {304 -- 319},
publisher = {Springer},
title = {{AMT: a property-based monitoring tool for analog systems}},
doi = {1567},
year = {2007},
}
@inproceedings{4370,
author = {Maler, Oded and Dejan Nickovic and Pnueli,Amir},
pages = {95 -- 107},
publisher = {Springer},
title = {{On synthesizing controllers from bounded-response properties}},
doi = {1568},
year = {2007},
}
@inproceedings{4394,
author = {Bouillaguet,Charles and Kuncak, Viktor and Thomas Wies and Zee,Karen and Rinard,Martin C.},
pages = {74 -- 88},
publisher = {Springer},
title = {{Using First-Order Theorem Provers in the Jahob Data Structure Verification System}},
doi = {1552},
year = {2007},
}
@inproceedings{4398,
author = {Berdine,Josh and Calcagno,Cristiano and Cook,Byron and Distefano,Dino and O'Hearn,Peter W. and Thomas Wies and Yang,Hongseok},
pages = {178 -- 192},
publisher = {Springer},
title = {{Shape Analysis for Composite Data Structures}},
doi = {1553},
year = {2007},
}
@inproceedings{4399,
abstract = {A temporal interface for a software component is a finite automaton that specifies the legal sequences of calls to functions that are provided by the component. We compare and evaluate three different algorithms for automatically extracting temporal interfaces from program code: (1) a game algorithm that computes the interface as a representation of the most general environment strategy to avoid a safety violation; (2) a learning algorithm that repeatedly queries the program to construct the minimal interface automaton; and (3) a CEGAR algorithm that iteratively refines an abstract interface hypothesis by adding relevant program variables. For comparison purposes, we present and implement the three algorithms in a unifying formal setting. While the three algorithms compute the same output and have similar worst-case complexities, their actual running times may differ considerably for a given input program. On the theoretical side, we provide for each of the three algorithms a family of input programs on which that algorithm outperforms the two alternatives. On the practical side, we evaluate the three algorithms experimentally on a variety of Java libraries. },
author = {Beyer, Dirk and Thomas Henzinger and Vasu Singh},
pages = {4 -- 19},
publisher = {Springer},
title = {{Algorithms for interface synthesis}},
doi = {10.1007/978-3-540-73368-3_4},
volume = {4590},
year = {2007},
}
@inproceedings{4402,
author = {Alur, Rajeev and Pavol Cerny and Chaudhuri,Swarat},
pages = {664 -- 678},
publisher = {Springer},
title = {{Model Checking on Trees with Path Equivalences}},
doi = {1544},
year = {2007},
}
@article{4405,
abstract = {Background
A central goal of Systems Biology is to model and analyze biological signaling pathways that interact with one another to form complex networks. Here we introduce Qualitative networks, an extension of Boolean networks. With this framework, we use formal verification methods to check whether a model is consistent with the laboratory experimental observations on which it is based. If the model does not conform to the data, we suggest a revised model and the new hypotheses are tested in-silico.
Results
We consider networks in which elements range over a small finite domain allowing more flexibility than Boolean values, and add target functions that allow to model a rich set of behaviors. We propose a symbolic algorithm for analyzing the steady state of these networks, allowing us to scale up to a system consisting of 144 elements and state spaces of approximately 1086 states. We illustrate the usefulness of this approach through a model of the interaction between the Notch and the Wnt signaling pathways in mammalian skin, and its extensive analysis.
Conclusion
We introduce an approach for constructing computational models of biological systems that extends the framework of Boolean networks and uses formal verification methods for the analysis of the model. This approach can scale to multicellular models of complex pathways, and is therefore a useful tool for the analysis of complex biological systems. The hypotheses formulated during in-silico testing suggest new avenues to explore experimentally. Hence, this approach has the potential to efficiently complement experimental studies in biology.},
author = {Schaub, Marc A and Thomas Henzinger and Fisher, Jasmin},
journal = {BMC Systems Biology},
number = {4},
publisher = {BioMed Central},
title = {{Qualitative networks: A symbolic approach to analyze biological signaling networks}},
doi = {10.1186/1752-0509-1-4},
volume = {1},
year = {2007},
}
@inbook{4417,
abstract = {Counterexample-guided abstraction refinement (CEGAR) is a powerful technique to scale automatic program analysis techniques to large programs. However, so far it has been used primarily for model checking in the context of predicate abstraction. We formalize CEGAR for general powerset domains. If a spurious abstract counterexample needs to be removed through abstraction refinement, there are often several choices, such as which program location(s) to refine, which abstract domain(s) to use at different locations, and which abstract values to compute. We define several plausible preference orderings on abstraction refinements, such as refining as “late” as possible and as “coarse” as possible. We present generic algorithms for finding refinements that are optimal with respect to the different preference orderings. We also compare the different orderings with respect to desirable properties, including the property if locally optimal refinements compose to a global optimum. Finally, we point out some difficulties with CEGAR for non-powerset domains.},
author = {Manevich, Roman and Field, John and Thomas Henzinger and Ramalingam, Ganesan and Sagiv, Mooly},
booktitle = {Program Analysis and Compilation, Theory and Practice: Essays Dedicated to Reinhard Wilhelm on the Occasion of His 60th Birthday},
pages = {273 -- 292},
publisher = {Springer},
title = {{Abstract counterexample-based refinement for powerset domains}},
doi = {10.1007/978-3-540-71322-7_13},
volume = {4444},
year = {2007},
}
@article{4446,
abstract = {The Embedded Machine is a virtual machine that mediates in real time the interaction between software processes and physical processes. It separates the compilation of embedded programs into two phases. The first phase, the platform-independent compiler phase, generates E code (code executed by the Embedded Machine), which supervises the timing, not the scheduling of, application tasks relative to external events such as clock ticks and sensor interrupts. E code is portable and, given an input behavior, exhibits predictable (i.e., deterministic) timing and output behavior. The second phase, the platform-dependent compiler phase, checks the time safety of the E code, that is, whether platform performance (determined by the hardware) and platform utilization (determined by the scheduler of the operating system) enable its timely execution. We have used the Embedded Machine to compile and execute high-performance control applications written in Giotto, such as the flight control system of an autonomous model helicopter.},
author = {Thomas Henzinger and Kirsch, Christoph M},
journal = {ACM Transactions on Programming Languages and Systems (TOPLAS)},
number = {393},
publisher = {ACM},
title = {{The embedded machine: Predictable, portable real-time code}},
doi = {10.1145/1286821.1286824},
volume = {29},
year = {2007},
}
@inproceedings{4511,
abstract = {In the traditional view, a language is a set of words, i.e., a function from words to boolean values. We call this view “qualitative,” because each word either belongs to or does not belong to a language. Let Σ be an alphabet, and let us consider infinite words over Σ. Formally, a qualitative language over Σ is a function A: B . There are many applications of qualitative languages. For example, qualitative languages are used to specify the legal behaviors of systems, and zero-sum objectives of games played on graphs. In the former case, each behavior of a system is either legal or illegal; in the latter case, each outcome of a game is either winning or losing. For defining languages, it is convenient to use finite acceptors (or generators). In particular, qualitative languages are often defined using finite-state machines (so-called ω-automata) whose transitions are labeled by letters from Σ. For example, the states of an ω-automaton may represent states of a system, and the transition labels may represent atomic observables of a behavior. There is a rich and well-studied theory of finite-state acceptors of qualitative languages, namely, the theory of theω-regular languages.},
author = {Thomas Henzinger},
pages = {20 -- 22},
publisher = {Springer},
title = {{Quantitative generalizations of languages}},
doi = {10.1007/978-3-540-73208-2_2},
volume = {4588},
year = {2007},
}
@inproceedings{4514,
abstract = {Digital technology is increasingly deployed in safety-critical situations. This calls for systematic design and verification methodologies that can cope with three major sources of system complexity: concurrency, real time, and uncertainty. We advocate a two-step process: formal modeling followed by algorithmic analysis (or, “model building” followed by “model checking”). We model the concurrent components of a reactive system as potential collaborators or adversaries in a multi-player game with temporal objectives, such as system safety. The real-time aspect of embedded systems requires models that combine discrete state transitions and continuous state evolutions. Uncertainty in the environment is naturally modeled by probabilistic state changes. As a result, we obtain three orthogonal extensions of the basic state-transition graph model for reactive systems —game graphs, timed graphs, and stochastic graphs— as well as combinations thereof. In this short text, we provide a uniform exposition of the underlying definitions. For verification algorithms, we refer the reader to the literature.},
author = {Thomas Henzinger},
pages = {103 -- 110},
publisher = {Springer},
title = {{Games, time, and probability: Graph models for system design and analysis}},
doi = {10.1007/978-3-540-69507-3_7},
volume = {4362},
year = {2007},
}
@article{4529,
abstract = {Computational modeling of biological systems is becoming increasingly important in efforts to better understand complex biological behaviors. In this review, we distinguish between two types of biological models—mathematical and computational—which differ in their representations of biological phenomena. We call the approach of constructing computational models of biological systems 'executable biology', as it focuses on the design of executable computer algorithms that mimic biological phenomena. We survey the main modeling efforts in this direction, emphasize the applicability and benefits of executable models in biological research and highlight some of the challenges that executable biology poses for biology and computer science. We claim that for executable biology to reach its full potential as a mainstream biological technique, formal and algorithmic approaches must be integrated into biological research. This will drive biology toward a more precise engineering discipline.},
author = {Fisher, Jasmin and Thomas Henzinger},
journal = {Nature Biotechnology},
pages = {1239 -- 1249},
publisher = {Nature Publishing Group},
title = {{Executable cell biology}},
doi = {10.1038/nbt1356},
volume = {25},
year = {2007},
}
@proceedings{4530,
abstract = {This book constitutes the refereed proceedings of the 21st International Workshop on Computer Science Logic, CSL 2007, held as the 16th Annual Conference of the EACSL in Lausanne, Switzerland. The 36 revised full papers presented together with the abstracts of six invited lectures are organized in topical sections on logic and games, expressiveness, games and trees, logic and deduction, lambda calculus, finite model theory, linear logic, proof theory, and game semantics.},
author = {Duparc, Jacques and Thomas Henzinger},
booktitle = {CSL: Computer Science Logic},
publisher = {Springer},
title = {{CSL: Computer Science Logic }},
doi = {10.1007/978-3-540-74915-8},
volume = {4646},
year = {2007},
}
@article{4531,
abstract = {Caenorhabditis elegans vulval development provides an important paradigm for studying the process of cell fate determination and pattern formation during animal development. Although many genes controlling vulval cell fate specification have been identified, how they orchestrate themselves to generate a robust and invariant pattern of cell fates is not yet completely understood. Here, we have developed a dynamic computational model incorporating the current mechanistic understanding of gene interactions during this patterning process. A key feature of our model is the inclusion of multiple modes of crosstalk between the epidermal growth factor receptor (EGFR) and LIN-12/Notch signaling pathways, which together determine the fates of the six vulval precursor cells (VPCs). Computational analysis, using the model-checking technique, provides new biological insights into the regulatory network governing VPC fate specification and predicts novel negative feedback loops. In addition, our analysis shows that most mutations affecting vulval development lead to stable fate patterns in spite of variations in synchronicity between VPCs. Computational searches for the basis of this robustness show that a sequential activation of the EGFR-mediated inductive signaling and LIN-12 / Notch-mediated lateral signaling pathways is key to achieve a stable cell fate pattern. We demonstrate experimentally a time-delay between the activation of the inductive and lateral signaling pathways in wild-type animals and the loss of sequential signaling in mutants showing unstable fate patterns; thus, validating two key predictions provided by our modeling work. The insights gained by our modeling study further substantiate the usefulness of executing and analyzing mechanistic models to investigate complex biological behaviors.},
author = {Fisher, Jasmin and Piterman, Nir and Hajnal, Alex and Thomas Henzinger},
journal = {PLoS Computational Biology},
publisher = {Public Library of Science},
title = {{Predictive modeling of signaling crosstalk during C. elegans vulval development}},
doi = {10.1371/journal.pcbi.0030092},
volume = {3(5):e92},
year = {2007},
}
@inproceedings{4537,
abstract = {The classical synthesis problem for reactive systems asks, given a proponent process A and an opponent process B, to refine A so that the closed-loop system A parallel to B satisfies a given specification Phi. The solution of this problem requires the computation of a winning strategy for proponent A in a game against opponent B. We define and study the co-synthesis problem, where the proponent A consists itself of two independent processes, A = A(1)parallel to A(2), with specifications Phi(1) and Phi(2), and the goal is to refine both A(1) and A(2) so that A(1)parallel to A(2)parallel to B satisfies Phi(1) boolean AND Phi(2). For example, if the opponent B is a fair scheduler for the two processes A(1) and A(2), and Phi(i) specifies the requirements of mutual exclusion for A(i) (e.g., starvation freedom), then the co-synthesis problem asks for the automatic synthesis of a mutual-exclusion protocol. We show that co-synthesis defined classically, with the processes A(1) and A(2) either collaborating or competing, does not capture desirable solutions. Instead, the proper formulation of co-synthesis is the one where process A, competes with A(2) but not at the price of violating Phi(1), and vice versa. We call this assume-guarantee synthesis and show that it can be solved by computing secure-equilibrium strategies. In particular, from mutual-exclusion requirements the assume-guarantee synthesis algorithm automatically computes Peterson's protocol.},
author = {Krishnendu Chatterjee and Thomas Henzinger},
pages = {261 -- 275},
publisher = {Springer},
title = {{Assume-guarantee synthesis}},
doi = {10.1007/978-3-540-71209-1_21},
volume = {4424},
year = {2007},
}
@article{4547,
abstract = {We study observation-based strategies for two-player turn-based games on graphs with omega-regular objectives. An observation-based strategy relies on imperfect information about the history of a play, namely, on the past sequence of observations. Such games occur in the synthesis of a controller that does not see the private state of the plant. Our main results are twofold. First, we give a fixed-point algorithm for computing the set of states from which a player can win with a deterministic observation-based strategy for any omega-regular objective. The fixed point is computed in the lattice of antichains of state sets. This algorithm has the advantages of being directed by the objective and of avoiding an explicit subset construction on the game graph. Second, we give an algorithm for computing the set of states from which a player can win with probability 1 with a randomized observation-based strategy for a Buechi objective. This set is of interest because in the absence of perfect information, randomized strategies are more powerful than deterministic ones. We show that our algorithms are optimal by proving matching lower bounds.},
author = {Krishnendu Chatterjee and Doyen, Laurent and Thomas Henzinger and Raskin, Jean-François},
journal = {Logical Methods in Computer Science},
number = {184},
pages = {1 -- 23},
publisher = {International Federation of Computational Logic},
title = {{Algorithms for omega-regular games with imperfect information}},
doi = {10.2168/LMCS-3(3:4)2007},
volume = {3},
year = {2007},
}
@phdthesis{4559,
abstract = {We study games played on graphs with omega-regular conditions specified as parity, Rabin, Streett or Muller conditions. These games have applications in the verification, synthesis, modeling, testing, and compatibility checking of reactive systems. Important distinctions between graph games are as follows: (a) turn-based vs. concurrent games, depending on whether at a state of the game only a single player makes a move, or players make moves simultaneously; (b) deterministic vs. stochastic, depending on whether the transition function is a deterministic or a probabilistic function over successor states; and (c) zero-sum vs. non-zero-sum, depending on whether the objectives of the players are strictly conflicting or not.
We establish that the decision problem for turn-based stochastic zero-sum games with Rabin, Streett, and Muller objectives are NP-complete, coNP-complete, and PSPACE-complete, respectively, substantially improving the previously known 3EXPTIME bound. We also present strategy improvement style algorithms for turn-based stochastic Rabin and Streett games. In the case of concurrent stochastic zero-sum games with parity objectives we obtain a PSPACE bound, again improving the previously known 3EXPTIME bound. As a consequence, concurrent stochastic zero-sum games with Rabin, Streett, and Muller objectives can be solved in EXPSPACE, improving the previously known 4EXPTIME bound. We also present an elementary and combinatorial proof of the existence of memoryless \epsilon-optimal strategies in concurrent stochastic games with reachability objectives, for all real \epsilon>0, where an \epsilon-optimal strategy achieves the value of the game with in \epsilon against all strategies of the opponent. We also use the proof techniques to present a strategy improvement style algorithm for concurrent stochastic reachability games.
We then go beyond \omega-regular objectives and study the complexity of an important class of quantitative objectives, namely, limit-average objectives. In the case of limit-average games, the states of the graph is labeled with rewards and the goal is to maximize the long-run average of the rewards. We show that concurrent stochastic zero-sum games with limit-average objectives can be solved in EXPTIME.
Finally, we introduce a new notion of equilibrium, called secure equilibrium, in non-zero-sum games which captures the notion of conditional competitiveness. We prove the existence of unique maximal secure equilibrium payoff profiles in turn-based deterministic games, and present algorithms to compute such payoff profiles. We also show how the notion of secure equilibrium extends the assume-guarantee style of reasoning in the game theoretic framework.},
author = {Krishnendu Chatterjee},
pages = {1 -- 247},
publisher = {University of California, Berkeley},
title = {{Stochastic ω-Regular Games}},
year = {2007},
}
@phdthesis{4566,
abstract = {Complex system design today calls for compositional design and implementation. However each component is designed with certain assumptions about the environment it is meant to operate in, and delivering certain guarantees if those assumptions are satisfied; numerous inter-component interaction errors are introduced in the manual and error-prone integration process as there is little support in design environments for machine-readably representing these assumptions and guarantees and automatically checking consistency during integration.
Based on Interface Automata we propose a framework for compositional design and analysis of systems: a set of domain-specific automata-theoretic type systems for compositional system specification and analysis by behavioral specification of open systems. We focus on three different domains: component-based hardware systems communicating on bidirectional wires. concurrent distributed recursive message-passing software systems, and embedded software system components operating in resource-constrained environments. For these domains we present approaches to formally represent the assumptions and conditional guarantees between interacting open system components. Composition of such components produces new components with the appropriate assumptions and guarantees. We check satisfaction of temporal logic specifications by such components, and the substitutability of one component with another in an arbitrary context. Using this framework one can analyze large systems incrementally without needing extensive summary information to close the system at each stage. Furthermore, we focus only on the inter-component interaction behavior without dealing with the full implementation details of each component. Many of the merits of automata-theoretic model-checking are combined with the compositionality afforded by type-system based techniques. We also present an integer-based extension of the conventional boolean verification framework motivated by our interface formalism for embedded software components.
Our algorithms for checking the behavioral compatibility of component interfaces are available in our tool Chic, which can be used as a plug-in for the Java IDE JBuilder and the heterogenous modeling and design environment Ptolemy II.
Finally, we address the complementary problem of partitioning a large system into meaningful coherent components by analyzing the interaction patterns between its basic elements. We demonstrate the usefulness of our partitioning approach by evaluating its efficacy in improving unit-test branch coverage for a large software system implemented in C.},
author = {Chakrabarti, Arindam},
pages = {1 -- 244},
publisher = {University of California, Berkeley},
title = {{A framework for compositional design and analysis of systems}},
year = {2007},
}
@article{4567,
abstract = {BLAST is an automatic verification tool for checking temporal safety properties of C programs. Given a C program and a temporal safety property, BLAST either statically proves that the program satisfies the safety property, or provides an execution path that exhibits a violation of the property (or, since the problem is undecidable, does not terminate). BLAST constructs, explores, and refines abstractions of the program state space based on lazy predicate abstraction and interpolation-based predicate discovery. This paper gives an introduction to BLAST and demonstrates, through two case studies, how it can be applied to program verification and test-case generation. In the first case study, we use BLAST to statically prove memory safety for C programs. We use CCured, a type-based memory-safety analyzer, to annotate a program with run-time assertions that check for safe memory operations. Then, we use BLAST to remove as many of the run-time checks as possible (by proving that these checks never fail), and to generate execution scenarios that violate the assertions for the remaining run-time checks. In our second case study, we use BLAST to automatically generate test suites that guarantee full coverage with respect to a given predicate. Given a C program and a target predicate p, BLAST determines the program locations q for which there exists a program execution that reaches q with p true, and automatically generates a set of test vectors that cause such executions. Our experiments show that BLAST can provide automated, precise, and scalable analysis for C programs.},
author = {Beyer, Dirk and Thomas Henzinger and Jhala, Ranjit and Majumdar, Ritankar S},
journal = {International Journal on Software Tools for Technology Transfer},
number = {5},
pages = {505 -- 525},
publisher = {Springer},
title = {{The software model checker BLAST: Applications to software engineering}},
doi = {10.1007/s10009-007-0044-z},
volume = {9},
year = {2007},
}
@inproceedings{4570,
abstract = {We consider the minimum-time reachability problem in concurrent two-player timed automaton game structures. We show how to compute the minimum time needed by a player to reach a target location against all possible choices of the opponent. We do not put any syntactic restriction on the game structure, nor do we require any player to guarantee time divergence. We only require players to use receptive strategies which do not block time. The minimal time is computed in part using a fixpoint expression, which we show can be evaluated on equivalence classes of a non-trivial extension of the clock-region equivalence relation for timed automata.},
author = {Brihaye, Thomas and Thomas Henzinger and Prabhu, Vinayak S and Raskin, Jean-François},
pages = {825 -- 837},
publisher = {Springer},
title = {{Minimum-time reachability in timed games}},
doi = {10.1007/978-3-540-73420-8_71},
volume = {4596},
year = {2007},
}