@article{4135,
  author       = {Storch,D. and Šizling,A. L and Reif,J. and Jitka Polechova and Šizlingová,E. and Gaston,K. J},
  journal      = {Ecology Letters},
  number       = {8},
  pages        = {771 -- 784},
  publisher    = {Wiley-Blackwell},
  title        = {{The quest for a null model for macroecological patterns: geometry of species distributions at multiple spatial scales}},
  doi          = {3817},
  volume       = {11},
  year         = {2008},
}

@inbook{4137,
  author       = {Bridle, Jon R and Jitka Polechova and Vines, Timothy H},
  booktitle    = {Evolution and Speciation},
  editor       = {R. K. Butlin,J.R. Bridle and Schluter,D.},
  pages        = {77 -- 101},
  publisher    = {Cambridge University Press},
  title        = {{Patterns of biodiversity and limits to adaptation in time and space}},
  doi          = {3816},
  year         = {2008},
}

@article{4141,
  abstract     = {The zyxin-related LPP protein is localized at focal adhesions and cell-cell contacts and is involved in the regulation of smooth muscle cell migration. A known interaction partner of LPP in human is the tumor suppressor protein SCRIB. Knocking down scrib expression c uring zebrafish embryonic development results in defects of convergence and extension (C&amp;amp;E) movements, which occur during gastrulation and mediate elongation of the anterior-posterior body axis. Mediolateral cell polarization underlying C&amp;amp;E is regulated by a noncanonical Writ signaling pathway constituting the vertebrate planar cell polarity (PCP) pathway. Here, we investigated the role of Lpp during early zebrafish development. We show that morpholino knockdown of Ipp results in defects of C&amp;amp;E, phenocopying noncanonical Wnt signaling mutants. Time-lapse analysis associates the defective dorsal convergence movements with a reduced ability to migrate along straight paths. In addition, expression of Lpp is significantly reduced in Wnt11 morphants and in embryos overexpressing Wnt11 or a dominant-negative form of Rho kinase 2, which is a downstream effector of Wnt11, Suggesting that Lpp expression is dependent on noncanonical Wnt signaling. Finally, we demonstrate that Lpp interacts with the PCP protein Scrib in zebrafish, and that Lpp and Scrib cooperate for the mediation of C&amp;amp;E. (C) 2008 Elsevier Inc. All rights reserved.},
  author       = {Vervenne, Hilke and Crombez, Koen and Lambaerts, Kathleen and Carvalho, Lara and Köppen, Mathias and Heisenberg, Carl-Philipp J and Van De Ven, Wim and Petit, Marleen},
  journal      = {Developmental Biology},
  number       = {1},
  pages        = {267 -- 277},
  publisher    = {Elsevier},
  title        = {{Lpp is involved in Wnt/PCP signaling and acts together with Scrib to mediate convergence and extension movements during zebrafish gastrulation}},
  doi          = {10.1016/j.ydbio.2008.05.529},
  volume       = {320},
  year         = {2008},
}

@article{4150,
  abstract     = {This study provides direct functional evidence that differential adhesion, measurable as quantitative differences in tissue surface tension, influences spatial positioning between zebrafish germ layer tissues. We show that embryonic ectodermal and mesendodermal tissues generated by mRNA-overexpression behave on long-time scales like immiscible fluids. When mixed in hanging drop culture, their cells segregate into discrete phases with ectoderm adopting an internal position relative to the mesendoderm. The position adopted directly correlates with differences in tissue surface tension. We also show that germ layer tissues from untreated embryos, when extirpated and placed in culture, adopt a configuration similar to those of their mRNA-overexpressing counterparts. Down-regulating E-cadherin expression in the ectoderm leads to reduced surface tension and results in phase reversal with E-cadherin-depleted ectoderm cells now adopting an external position relative to the mesendoderm. These results show that in vitro cell sorting of zebrafish mesendoderm and ectoderm tissues is specified by tissue interfacial tensions. We perform a mathematical analysis indicating that tissue interfacial tension between actively motile cells contributes to the spatial organization and dynamics of these zebrafish germ layers in vivo.},
  author       = {Schötz, Eva and Burdine, Rebecca and Julicher, Frank and Steinberg, Malcolm and Heisenberg, Carl-Philipp J and Foty, Ramsey},
  journal      = {HFSP Journal},
  number       = {1},
  pages        = {42 -- 56},
  publisher    = {HFSP Publishing},
  title        = {{Quantitative differences in tissue surface tension influence zebrafish germ layer positioning}},
  doi          = {10.2976/1.2834817},
  volume       = {2},
  year         = {2008},
}

@article{4161,
  abstract     = {Handedness of the vertebrate body plan critically depends on transient embryonic structures/ organs that generate cilia-dependent leftward fluid flow within constrained extracellular environments. Although the function of ciliated organs in laterality determination has been extensively studied, how they are formed during embryogenesis is still poorly understood. Here we show that Kupffer's vesicle (KV), the zebrafish organ of laterality, arises from a surface epithelium previously thought to adopt exclusively extra-embryonic fates. Live multi-photon confocal imaging reveals that surface epithelial cells undergo Nodal/TGF beta signalling-dependent ingression at the dorsal germ ring margin prior to gastrulation, to give rise to dorsal forerunner cells (DFCs), the precursors of KV. DFCs then migrate attached to the overlying surface epithelium and rearrange into rosette-like epithelial structures at the end of gastrulation. During early somitogenesis, these epithelial rosettes coalesce into a single rosette that differentiates into the KV with a ciliated lumen at its apical centre. Our results provide novel insights into the morphogenetic transformations that shape the laterality organ in zebrafish and suggest a conserved progenitor role of the surface epithelium during laterality organ formation in vertebrates.},
  author       = {Oteíza, Pablo and Köppen, Mathias and Concha, Miguel and Heisenberg, Carl-Philipp J},
  journal      = {Development},
  number       = {16},
  pages        = {2807 -- 2813},
  publisher    = {Company of Biologists},
  title        = {{Origin and shaping of the laterality organ in zebrafish}},
  doi          = {10.1242/dev.022228},
  volume       = {135},
  year         = {2008},
}

@article{4180,
  abstract     = {(Figure Presented) The name's Bond: Separated cells form membranous nanotubes whose tips are tethered by adhesive bonds (see picture). The lifetime of receptor-ligand interactions can be measured by using membrane nanotubes of living cells as constant force actuators. Because the nanotubes are extruded from living cells at conditions approaching the physiological, cellular processes can be both studied and utilized. },
  author       = {Krieg, Michael and Helenius, Jonne and Heisenberg, Carl-Philipp J and Mueller, Daniel},
  journal      = {Angewandte Chemie - International Edition},
  number       = {50},
  pages        = {9775 -- 9777},
  publisher    = {Wiley-Blackwell},
  title        = {{A Bond for a Lifetime: Employing Membrane Nanotubes from Living Cells to Determine Receptor-Ligand Kinetics}},
  doi          = {10.1002/anie.200803552},
  volume       = {47},
  year         = {2008},
}

@article{4181,
  abstract     = {Understanding the factors that direct tissue organization during development is one of the most fundamental goals in developmental biology. Various hypotheses explain cell sorting and tissue organization on the basis of the adhesive and mechanical properties of the constituent cells(1). However, validating these hypotheses has been difficult due to the lack of appropriate tools to measure these parameters. Here we use atomic force microscopy ( AFM) to quantify the adhesive and mechanical properties of individual ectoderm, mesoderm and endoderm progenitor cells from gastrulating zebrafish embryos. Combining these data with tissue self-assembly in vitro and the sorting behaviour of progenitors in vivo, we have shown that differential actomyosin-dependent cell-cortex tension, regulated by Nodal/ TGF beta-signalling ( transforming growth factor beta), constitutes a key factor that directs progenitor-cell sorting. These results demonstrate a previously unrecognized role for Nodal-controlled cell-cortex tension in germ-layer organization during gastrulation.},
  author       = {Krieg, Michael and Arboleda Estudillo, Yohanna and Puech, Pierre and Käfer, Jos and Graner, François and Mueller, Daniel and Heisenberg, Carl-Philipp J},
  journal      = {Nature Cell Biology},
  number       = {4},
  pages        = {429 -- 436},
  publisher    = {Nature Publishing Group},
  title        = {{Tensile forces govern germ-layer organization in zebrafish}},
  doi          = {10.1038/ncb1705},
  volume       = {10},
  year         = {2008},
}

@article{4190,
  abstract     = {During vertebrate gastrulation, cells forming the prechordal plate undergo directed migration as a cohesive cluster. Recent studies revealed that E-cadherin-mediated coherence between these cells plays an important role in effective anterior migration, and that platelet-derived growth factor (Pdgf) appears to act as a guidance cue in this process. However, the mechanisms underlying this process at the individual cell level remain poorly understood. We have identified miles apart (mil) as a suppressor of defective anterior migration of the prospective prechordal plate in silberblick (slb)/wnt11 mutant embryos, in which E-cadherin-mediated coherence of cell movement is reduced. mil encodes Edg5, a sphingosine-1-phosphate (S1P) receptor belonging to a family of five G-protein-coupled receptors (S1PRs). S1P is a lipid signalling molecule that has been implicated in regulating cytoskeletal rearrangements, cell motility and cell adhesion in a variety of cell types. We examined the roles of Mil in anterior migration of prechordal plate progenitor cells and found that, in slb embryos injected with mil-MO, cells migrate with increased motility but decreased directionality, without restoring the coherence of cell migration. This indicates that prechordal plate progenitor cells can migrate effectively as individuals, as well as in a coherent cluster of cells. Moreover, we demonstrate that Mil regulates cell motility and polarisation through Pdgf and its intracellular effecter PI3K, but modulates cell coherence independently of the Pdgf/PI3K pathway, thus co-ordinating cell motility and coherence. These results suggest that the net migration of prechordal plate progenitors is determined by different parameters, including motility, persistence and coherence.},
  author       = {Kai, Masatake and Heisenberg, Carl-Philipp J and Tada, Masazumi},
  journal      = {Development},
  number       = {18},
  pages        = {3043 -- 3051},
  publisher    = {Company of Biologists},
  title        = {{Sphingosine-1-phosphate receptors regulate individual cell behaviours underlying the directed migration of prechordal plate progenitor cells during zebrafish gastrulation}},
  doi          = {10.1242/dev.020396},
  volume       = {135},
  year         = {2008},
}

@article{4193,
  abstract     = {The controlled adhesion of cells to each other and to the extracellular matrix is crucial for tissue development and maintenance. Numerous assays have been developed to quantify cell adhesion. Among these, the use of atomic force microscopy (AFM) for single-cell force spectroscopy (SCFS) has recently been established. This assay permits the adhesion of living cells to be studied in near-physiological conditions. This implementation of AFM allows unrivaled spatial and temporal control of cells, as well as highly quantitative force actuation and force measurement that is sufficiently sensitive to characterize the interaction of single molecules. Therefore, not only overall cell adhesion but also the properties of single adhesion-receptor-ligand interactions can be studied. Here we describe current implementations and applications of SCFS, as well as potential pitfalls, and outline how developments will provide insight into the forces, energetics and kinetics of cell-adhesion processes.},
  author       = {Helenius, Jonne and Heisenberg, Carl-Philipp J and Gaub, Hermann and Mueller, Daniel},
  journal      = {Journal of Cell Science},
  number       = {11},
  pages        = {1785 -- 1791},
  publisher    = {Company of Biologists},
  title        = {{Single-cell force spectroscopy}},
  doi          = {10.1242/​jcs.030999},
  volume       = {121},
  year         = {2008},
}

@article{4198,
  abstract     = {Animal body plan arises during gastrulation and organogenesis by the coordination of inductive events and cell movements. Several signaling pathways, such as BMP, FGF, Hedgehog, Nodal, and Wnt have well-recognized instructive roles in cell fate specification during vertebrate embryogenesis. Growing evidence indicates that BMP, Nodal, and FGF signaling also regulate cell movements, and that they do so through mechanisms distinct from those that specify cell fates. Moreover, pathways controlling cell movements can also indirectly influence cell fate specification by regulating dimensions and relative positions of interacting tissues. The current challenge is to delineate the molecular mechanisms via which the major signaling pathways regulate cell fate specification and movements, and how these two processes are coordinated to ensure normal development.},
  author       = {Heisenberg, Carl-Philipp J and Solnica Krezel, Lilianna},
  journal      = {Current Opinion in Genetics & Development},
  number       = {4},
  pages        = {311 -- 316},
  publisher    = {Elsevier},
  title        = {{Back and forth between cell fate specification and movement during vertebrate gastrulation}},
  doi          = {10.1016/j.gde.2008.07.011},
  volume       = {18},
  year         = {2008},
}

@article{4227,
  abstract     = {Morphogen concentration gradients provide positional information by activating target genes in a concentration-dependent manner. Recent reports show that the gradient of the syncytial morphogen Bicoid seems to provide precise positional information to determine target gene domains. For secreted morphogenetic ligands, the precision of the gradients, the signal transduction and the reliability of target gene expression domains have not been studied. Here we investigate these issues for the TGF-beta-type morphogen Dpp. We first studied theoretically how cell-to-cell variability in the source, the target tissue, or both, contribute to the variations of the gradient. Fluctuations in the source and target generate a local maximum of precision at a finite distance to the source. We then determined experimentally in the wing epithelium: (1) the precision of the Dpp concentration gradient; (2) the precision of the Dpp signaling activity profile; and (3) the precision of activation of the Dpp target gene spalt. As captured by our theoretical description, the Dpp gradient provides positional information with a maximal precision a few cells away from the source. This maximal precision corresponds to a positional uncertainly of about a single cell diameter. The precision of the Dpp gradient accounts for the precision of the spalt expression range, implying that Dpp can act as a morphogen to coarsely determine the expression pattern of target genes.},
  author       = {Bollenbach, Tobias and Pantazis, Periklis and Anna Kicheva and Bokel,  Christian and González-Gaitán, Marcos and Julicher, Frank},
  journal      = {Development},
  number       = {6},
  pages        = {1137 -- 1146},
  publisher    = {Company of Biologists},
  title        = {{Precision of the Dpp gradient}},
  doi          = {10.1242/dev.012062},
  volume       = {135},
  year         = {2008},
}

@inproceedings{4244,
  abstract     = {This paper presents a new approach to optimization of an energy-constrained modulation scheme for wireless sensor networks by taking advantage of a novel bio-inspired optimization algorithm. The algorithm is inspired by Wrightpsilas shifting balance theory (SBT) of evolution in population genetics. The total energy consumption of an energy-constrained modulation scheme is minimized by using the new SBT-based optimization algorithm. The results obtained by this new algorithm are compared with other popular optimization algorithms. Numerical experiments are performed to demonstrate that the SBT-based algorithm could be used as an efficient optimizer for solving the optimization problems arising from currently emerging energy-efficient wireless sensor networks.},
  author       = {Yang, Erfu and Nicholas Barton and Arslan, Tughrul and Erdogan, Ahmet T},
  pages        = {2749 -- 2756},
  publisher    = {IEEE},
  title        = {{A novel shifting balance theory-based approach to optimization of an energy-constrained modulation scheme for wireless sensor networks}},
  doi          = {10.1109/CEC.2008.4631167},
  year         = {2008},
}

@article{4245,
  abstract     = {Sex allocation theory has proved extremely successful at predicting when individuals should adjust the sex of their offspring in response to environmental conditions. However, we know rather little about the underlying genetics of sex ratio or how genetic architecture might constrain adaptive sex-ratio behavior. We examined how mutation influenced genetic variation in the sex ratios produced by the parasitoid wasp Nasonia vitripennis. In a mutation accumulation experiment, we determined the mutability of sex ratio, and compared this with the amount of genetic variation observed in natural populations. We found that the mutability (h2m) ranges from 0.001 to 0.002, similar to estimates for life-history traits in other organisms. These estimates suggest one mutation every 5–60 generations, which shift the sex ratio by approximately 0.01 (proportion males). In this and other studies, the genetic variation in N. vitripennis sex ratio ranged from 0.02 to 0.17 (broad-sense heritability, H2). If sex ratio is maintained by mutation–selection balance, a higher genetic variance would be expected given our mutational parameters. Instead, the observed genetic variance perhaps suggests additional selection against sex-ratio mutations with deleterious effects on other fitness traits as well as sex ratio (i.e., pleiotropy), as has been argued to be the case more generally.},
  author       = {Pannebakker, Bart A and Halligan, Daniel and Reynolds, K Tracy and Ballantyne, Gavin A and Shuker, David M and Nicholas Barton and West, Stuart A},
  journal      = {Evolution; International Journal of Organic Evolution},
  number       = {8},
  pages        = {1921 -- 1935},
  publisher    = {Wiley-Blackwell},
  title        = {{Effects of spontaneous mutation accumulation on sex ratio traits}},
  doi          = {10.1111/j.1558-5646.2008.00434.x},
  volume       = {62},
  year         = {2008},
}

@inproceedings{4366,
  abstract     = {Termination of a heap-manipulating program generally depends on preconditions that express heap assumptions (i.e., assertions describing reachability, aliasing, separation and sharing in the heap). We present an algorithm for the inference of such preconditions. The algorithm exploits a unique interplay between counterexample-producing abstract termination checker and shape analysis. The shape analysis produces heap assumptions on demand to eliminate counterexamples, i.e., non-terminating abstract computations. The experiments with our prototype implementation indicate its practical potential.},
  author       = {Podelski,Andreas and Rybalchenko, Andrey and Thomas Wies},
  pages        = {314 -- 327},
  publisher    = {Springer},
  title        = {{Heap Assumptions on Demand}},
  doi          = {10.1007/978-3-540-70545-1_31},
  volume       = {5123},
  year         = {2008},
}

@inbook{4371,
  abstract     = {We survey some of the problems associated with checking whether a given behavior (a sequence, a Boolean signal or a continuous signal) satisfies a property specified in an appropriate temporal logic and describe two such monitoring algorithms for the real-time logic MITL.},
  author       = {Maler, Oded and Nickovic, Dejan and Pnueli, Amir},
  booktitle    = {Pillars of Computer science: Essays Dedicated To Boris (Boaz) Trakhtenbrot on the Occasion of His 85th Birthday},
  isbn         = {9783540781264},
  pages        = {475 -- 505},
  publisher    = {Springer},
  title        = {{Checking Temporal Properties of Discrete, Timed and Continuous Behaviors}},
  doi          = {10.1007/978-3-540-78127-1_26},
  year         = {2008},
}

@inproceedings{4384,
  abstract     = {Model checking software transactional memories (STMs) is difficult because of the unbounded number, length, and delay of concurrent transactions and the unbounded size of the memory. We show that, under certain conditions, the verification problem can be reduced to a finite-state problem, and we illustrate the use of the method by proving the correctness of several STMs, including two-phase locking, DSTM, TL2, and optimistic concurrency control. The safety properties we consider include strict serializability and opacity; the liveness properties include obstruction freedom, livelock freedom, and wait freedom.

Our main contribution lies in the structure of the proofs, which are largely automated and not restricted to the STMs mentioned above. In a first step we show that every STM that enjoys certain structural properties either violates a safety or liveness requirement on some program with two threads and two shared variables, or satisfies the requirement on all programs. In the second step we use a model checker to prove the requirement for the STM applied to a most general program with two threads and two variables. In the safety case, the model checker constructs a simulation relation between two carefully constructed finite-state transition systems, one representing the given STM applied to a most general program, and the other representing a most liberal safe STM applied to the same program. In the liveness case, the model checker analyzes fairness conditions on the given STM transition system.},
  author       = {Guerraoui, Rachid and Thomas Henzinger and Jobstmann, Barbara and Vasu Singh},
  pages        = {372 -- 382},
  publisher    = {ACM},
  title        = {{Model checking transactional memories}},
  doi          = {10.1145/1375581.1375626},
  year         = {2008},
}

@inproceedings{4386,
  abstract     = {We introduce the notion of permissiveness in transactional memories (TM). Intuitively, a TM is permissive if it never aborts a transaction when it need not. More specifically, a TM is permissive with respect to a safety property p if the TM accepts every history that satisfies p. Permissiveness, like safety and liveness, can be used as a metric to compare TMs. We illustrate that it is impractical to achieve permissiveness deterministically, and then show how randomization can be used to achieve permissiveness efficiently. We introduce Adaptive Validation STM (AVSTM), which is probabilistically permissive with respect to opacity; that is, every opaque history is accepted by AVSTM with positive probability. Moreover, AVSTM guarantees lock freedom. Owing to its permissiveness, AVSTM outperforms other STMs by up to 40% in read dominated workloads in high contention scenarios. But, in low contention scenarios, the book-keeping done by AVSTM to achieve permissiveness makes AVSTM, on average, 20-30% worse than existing STMs.},
  author       = {Guerraoui, Rachid and Thomas Henzinger and Vasu Singh},
  pages        = {305 -- 319},
  publisher    = {Springer},
  title        = {{Permissiveness in transactional memories}},
  doi          = {10.1007/978-3-540-87779-0_21},
  volume       = {5218},
  year         = {2008},
}

@inproceedings{4387,
  abstract     = {Software transactional memory (STM) offers a disciplined concurrent programming model for exploiting the parallelism of modern processor architectures. This paper presents the first deterministic specification automata for strict serializability and opacity in STMs. Using an antichain-based tool, we show our deterministic specifications to be equivalent to more intuitive, nondeterministic specification automata (which are too large to be determinized automatically). Using deterministic specification automata, we obtain a complete verification tool for STMs. We also show how to model and verify contention management within STMs. We automatically check the opacity of popular STM algorithms, such as TL2 and DSTM, with a universal contention manager. The universal contention manager is nondeterministic and establishes correctness for all possible contention management schemes.},
  author       = {Guerraoui, Rachid and Thomas Henzinger and Vasu Singh},
  pages        = {21 -- 35},
  publisher    = {Schloss Dagstuhl - Leibniz-Zentrum für Informatik},
  title        = {{Completeness and nondeterminism in model checking transactional memories}},
  doi          = {10.1007/978-3-540-85361-9_6},
  volume       = {5201},
  year         = {2008},
}

@inproceedings{4397,
  author       = {Beyer, Dirk and Damien Zufferey and Majumdar, Ritankar S},
  pages        = {304 -- 308},
  publisher    = {Springer},
  title        = {{CSIsat: Interpolation for LA+EUF}},
  year         = {2008},
}

@inproceedings{4400,
  author       = {Aviv,Adam J. and Pavol Cerny and Clark,Sandy and Cronin,Eric and Shah,Gaurav and Sherr,Micah and Blaze,Matt},
  publisher    = {USENIX},
  title        = {{Security Evaluation of ES&amp;S Voting Machines and Election Management System}},
  doi          = {1545},
  year         = {2008},
}

