[{"publication":"Discrete & Computational Geometry","month":"01","oa_version":"None","language":[{"iso":"eng"}],"date_published":"1999-01-01T00:00:00Z","type":"journal_article","publist_id":"2115","publication_identifier":{"issn":["0179-5376"]},"user_id":"ea97e931-d5af-11eb-85d4-e6957dddbf17","status":"public","author":[{"orcid":"0000-0002-9823-6833","full_name":"Edelsbrunner, Herbert","first_name":"Herbert","last_name":"Edelsbrunner","id":"3FB178DA-F248-11E8-B48F-1D18A9856A87"}],"issue":"1","_id":"4014","scopus_import":"1","title":"Deformable smooth surface design","intvolume":"        21","publication_status":"published","date_created":"2018-12-11T12:06:26Z","article_processing_charge":"No","page":"87 - 115","quality_controlled":"1","article_type":"original","publisher":"Springer","date_updated":"2022-09-06T09:02:23Z","year":"1999","citation":{"mla":"Edelsbrunner, Herbert. “Deformable Smooth Surface Design.” <i>Discrete &#38; Computational Geometry</i>, vol. 21, no. 1, Springer, 1999, pp. 87–115, doi:<a href=\"https://doi.org/10.1007/PL00009412\">10.1007/PL00009412</a>.","short":"H. Edelsbrunner, Discrete &#38; Computational Geometry 21 (1999) 87–115.","ista":"Edelsbrunner H. 1999. Deformable smooth surface design. Discrete &#38; Computational Geometry. 21(1), 87–115.","ama":"Edelsbrunner H. Deformable smooth surface design. <i>Discrete &#38; Computational Geometry</i>. 1999;21(1):87-115. doi:<a href=\"https://doi.org/10.1007/PL00009412\">10.1007/PL00009412</a>","apa":"Edelsbrunner, H. (1999). Deformable smooth surface design. <i>Discrete &#38; Computational Geometry</i>. Springer. <a href=\"https://doi.org/10.1007/PL00009412\">https://doi.org/10.1007/PL00009412</a>","ieee":"H. Edelsbrunner, “Deformable smooth surface design,” <i>Discrete &#38; Computational Geometry</i>, vol. 21, no. 1. Springer, pp. 87–115, 1999.","chicago":"Edelsbrunner, Herbert. “Deformable Smooth Surface Design.” <i>Discrete &#38; Computational Geometry</i>. Springer, 1999. <a href=\"https://doi.org/10.1007/PL00009412\">https://doi.org/10.1007/PL00009412</a>."},"abstract":[{"text":"A new paradigm for designing smooth surfaces is described. A finite set of points with weights specifies a closed surface in space referred to as skin. It consists of one or more components, each tangent continuous and free of self-intersections and intersections with other components. The skin varies continuously with the weights and locations of the points, and the variation includes the possibility of a topology change facilitated by the violation of tangent continuity at a single point in space and time. Applications of the skin to molecular modeling and to geometric deformation are discussed.","lang":"eng"}],"doi":"10.1007/PL00009412","day":"01","extern":"1","volume":21},{"article_type":"original","publisher":"Company of Biologists","quality_controlled":"1","page":"2129 - 2140","intvolume":"       126","title":"Zebrafish aussicht mutant embryos exhibit widespread overexpression of ace (fgf8) and coincident defects in CNS development","article_processing_charge":"No","date_created":"2018-12-11T12:07:34Z","publication_status":"published","issue":"10","author":[{"id":"39427864-F248-11E8-B48F-1D18A9856A87","full_name":"Heisenberg, Carl-Philipp J","orcid":"0000-0002-0912-4566","last_name":"Heisenberg","first_name":"Carl-Philipp J"},{"first_name":"Caroline","last_name":"Brennan","full_name":"Brennan, Caroline"},{"full_name":"Wilson, Stephen","last_name":"Wilson","first_name":"Stephen"}],"scopus_import":"1","pmid":1,"_id":"4204","extern":"1","volume":126,"acknowledgement":"We thank Corinne Houart, Michael Brand and the late Nigel Holder for comments and advice on this study, many colleagues for providing probes used in this analysis, other members of our laboratories for suggestions throughout the course of the work and Michael Brand, Jörg Rauch and Pascal Haffter for providing data prior to publication. We also would like to thank Christiane Nüsslein-Volhard in whose laboratory the mutant described in this study was initially isolated.\r\nThis study was supported by grants from The Wellcome Trust and\r\nBBSRC. C. P. H. was supported by Fellowships from EMBO and the\r\nEC, and S. W. W. is a Wellcome Trust Senior Research Fellow.\r\n","abstract":[{"text":"During the development of the zebrafish nervous system both noi, a zebrafish pax2 homolog, and ace, a zebrafish fgf8 homolog, are required for development of the midbrain and cerebellum. Here we describe a dominant mutation, aussicht (aus), in which the expression of noi and ace is upregulated, In aus mutant embryos, ace is upregulated at many sites in the embryo, while Itoi expression is only upregulated in regions of the forebrain and midbrain which also express ace. Subsequent to the alterations in noi and ace expression, aus mutants exhibit defects in the differentiation of the forebrain, midbrain and eyes. Within the forebrain, the formation of the anterior and postoptic commissures is delayed and the expression of markers within the pretectal area is reduced. Within the midbrain, En and wnt1 expression is expanded. In heterozygous aus embryos, there is ectopic outgrowth of neural retina in the temporal half of the eyes, whereas in putative homozygous aus embryos, the ventral retina is reduced and the pigmented retinal epithelium is expanded towards the midline, The observation that ans mutant embryos exhibit widespread upregulation of ace raised the possibility that aus might represent an allele of the ace gene itself. However, by crossing carriers for both aus and ace, we were able to generate homozygous ace mutant embryos that also exhibited the aus phenotype, This indicated that aus is not tightly linked to ace and is unlikely to be a mutation directly affecting the ace locus. However, increased Ace activity may underly many aspects of the aus phenotype and we show that the upregulation of noi in the forebrain of aus mutants is partially dependent upon functional Ace activity. Conversely, increased ace expression in the forebrain of arcs mutants is not dependent upon functional Noi activity. We conclude that aus represents a mutation involving a locus normally required for the regulation of ace expression during embryogenesis.","lang":"eng"}],"day":"15","doi":"10.1242/dev.126.10.2129","external_id":{"pmid":["10207138"]},"year":"1999","citation":{"mla":"Heisenberg, Carl-Philipp J., et al. “Zebrafish Aussicht Mutant Embryos Exhibit Widespread Overexpression of Ace (Fgf8) and Coincident Defects in CNS Development.” <i>Development</i>, vol. 126, no. 10, Company of Biologists, 1999, pp. 2129–40, doi:<a href=\"https://doi.org/10.1242/dev.126.10.2129\">10.1242/dev.126.10.2129</a>.","short":"C.-P.J. Heisenberg, C. Brennan, S. Wilson, Development 126 (1999) 2129–2140.","ista":"Heisenberg C-PJ, Brennan C, Wilson S. 1999. Zebrafish aussicht mutant embryos exhibit widespread overexpression of ace (fgf8) and coincident defects in CNS development. Development. 126(10), 2129–2140.","apa":"Heisenberg, C.-P. J., Brennan, C., &#38; Wilson, S. (1999). Zebrafish aussicht mutant embryos exhibit widespread overexpression of ace (fgf8) and coincident defects in CNS development. <i>Development</i>. Company of Biologists. <a href=\"https://doi.org/10.1242/dev.126.10.2129\">https://doi.org/10.1242/dev.126.10.2129</a>","ama":"Heisenberg C-PJ, Brennan C, Wilson S. Zebrafish aussicht mutant embryos exhibit widespread overexpression of ace (fgf8) and coincident defects in CNS development. <i>Development</i>. 1999;126(10):2129-2140. doi:<a href=\"https://doi.org/10.1242/dev.126.10.2129\">10.1242/dev.126.10.2129</a>","ieee":"C.-P. J. Heisenberg, C. Brennan, and S. Wilson, “Zebrafish aussicht mutant embryos exhibit widespread overexpression of ace (fgf8) and coincident defects in CNS development,” <i>Development</i>, vol. 126, no. 10. Company of Biologists, pp. 2129–2140, 1999.","chicago":"Heisenberg, Carl-Philipp J, Caroline Brennan, and Stephen Wilson. “Zebrafish Aussicht Mutant Embryos Exhibit Widespread Overexpression of Ace (Fgf8) and Coincident Defects in CNS Development.” <i>Development</i>. Company of Biologists, 1999. <a href=\"https://doi.org/10.1242/dev.126.10.2129\">https://doi.org/10.1242/dev.126.10.2129</a>."},"date_updated":"2022-09-06T08:38:01Z","language":[{"iso":"eng"}],"month":"05","oa_version":"None","publication":"Development","user_id":"ea97e931-d5af-11eb-85d4-e6957dddbf17","status":"public","publist_id":"1914","publication_identifier":{"issn":["0950-1991"]},"type":"journal_article","date_published":"1999-05-15T00:00:00Z"},{"volume":53,"acknowledgement":"We thank the Perovic family for their generous hospitality in Croatia and B.Nurnberger, C.MacCallum, D.Howard, and ananonymous reviewer for comments on the manuscript. The work was supported by a Natural Environment Research Council studentship to LEBK.","extern":"1","day":"01","doi":"10.2307/2640907","abstract":[{"text":"Reproductive isolation between two taxa may be due to endogenous selection, which is generated by incompatibilities between the respective genomes, to exogenous selection, which is generated by differential adaptations to alternative environments, or to both. The continuing debate over the relative importance of either mode of selection has highlighted the need for unambiguous data on the fitness of hybrid genotypes. The hybrid zone between the fire-bellied toad (Bombina bombina) and the yellow-bellied toad (B. variegata) in central Europe involves adaptation to different environments, but evidence of hybrid dysfunction is equivocal. In this study, we followed the development under laboratory conditions of naturally laid eggs collected from a transect across the Bombina hybrid zone in Croatia. Fitness was significantly reduced in hybrid populations: Egg batches from the center of the hybrid zone showed significantly higher embryonic and larval mortality and higher frequencies of morphological abnormalities relative to either parental type. Overall mortality from day of egg collection to three weeks after hatching reached 20% in central hybrid populations, compared to 2% in pure populations. There was no significant difference in fitness between two parental types. Within hybrid populations, there was considerable variation in fitness, with some genotypes showing no evidence of reduced viability. We discuss the implications of these findings for our understanding of barriers to gene flow between species.","lang":"eng"}],"year":"1999","citation":{"ama":"Kruuk L, Gilchrist J, Barton NH. Hybrid dysfunction in fire-bellied toads (Bombina). <i>Evolution; International Journal of Organic Evolution</i>. 1999;53(5):1611-1616. doi:<a href=\"https://doi.org/10.2307/2640907\">10.2307/2640907</a>","apa":"Kruuk, L., Gilchrist, J., &#38; Barton, N. H. (1999). Hybrid dysfunction in fire-bellied toads (Bombina). <i>Evolution; International Journal of Organic Evolution</i>. Wiley-Blackwell. <a href=\"https://doi.org/10.2307/2640907\">https://doi.org/10.2307/2640907</a>","ieee":"L. Kruuk, J. Gilchrist, and N. H. Barton, “Hybrid dysfunction in fire-bellied toads (Bombina),” <i>Evolution; International Journal of Organic Evolution</i>, vol. 53, no. 5. Wiley-Blackwell, pp. 1611–1616, 1999.","chicago":"Kruuk, Loeske, Jason Gilchrist, and Nicholas H Barton. “Hybrid Dysfunction in Fire-Bellied Toads (Bombina).” <i>Evolution; International Journal of Organic Evolution</i>. Wiley-Blackwell, 1999. <a href=\"https://doi.org/10.2307/2640907\">https://doi.org/10.2307/2640907</a>.","short":"L. Kruuk, J. Gilchrist, N.H. Barton, Evolution; International Journal of Organic Evolution 53 (1999) 1611–1616.","mla":"Kruuk, Loeske, et al. “Hybrid Dysfunction in Fire-Bellied Toads (Bombina).” <i>Evolution; International Journal of Organic Evolution</i>, vol. 53, no. 5, Wiley-Blackwell, 1999, pp. 1611–16, doi:<a href=\"https://doi.org/10.2307/2640907\">10.2307/2640907</a>.","ista":"Kruuk L, Gilchrist J, Barton NH. 1999. Hybrid dysfunction in fire-bellied toads (Bombina). Evolution; International Journal of Organic Evolution. 53(5), 1611–1616."},"date_updated":"2022-09-06T08:20:03Z","external_id":{"pmid":["28565554"]},"publisher":"Wiley-Blackwell","article_type":"original","quality_controlled":"1","page":"1611 - 1616","article_processing_charge":"No","date_created":"2018-12-11T12:08:00Z","publication_status":"published","intvolume":"        53","title":"Hybrid dysfunction in fire-bellied toads (Bombina)","scopus_import":"1","_id":"4277","pmid":1,"issue":"5","author":[{"last_name":"Kruuk","first_name":"Loeske","full_name":"Kruuk, Loeske"},{"last_name":"Gilchrist","first_name":"Jason","full_name":"Gilchrist, Jason"},{"id":"4880FE40-F248-11E8-B48F-1D18A9856A87","last_name":"Barton","first_name":"Nicholas H","full_name":"Barton, Nicholas H","orcid":"0000-0002-8548-5240"}],"user_id":"ea97e931-d5af-11eb-85d4-e6957dddbf17","status":"public","publication_identifier":{"issn":["0014-3820"]},"publist_id":"1811","type":"journal_article","date_published":"1999-10-01T00:00:00Z","language":[{"iso":"eng"}],"oa_version":"None","month":"10","publication":"Evolution; International Journal of Organic Evolution"},{"external_id":{"pmid":["10224266"]},"date_updated":"2022-09-06T08:12:14Z","citation":{"ieee":"S. Goodman, N. H. Barton, G. Swanson, K. Abernethy, and J. Pemberton, “Introgression through rare hybridisation: A genetic study of a hybrid zone between red and sika deer (genus Cervus), in Argyll, Scotland,” <i>Genetics</i>, vol. 152, no. 1. Genetics Society of America, pp. 355–371, 1999.","chicago":"Goodman, Simon, Nicholas H Barton, Graeme Swanson, Kate Abernethy, and Josephine Pemberton. “Introgression through Rare Hybridisation: A Genetic Study of a Hybrid Zone between Red and Sika Deer (Genus Cervus), in Argyll, Scotland.” <i>Genetics</i>. Genetics Society of America, 1999. <a href=\"https://doi.org/10.1093/genetics/152.1.355\">https://doi.org/10.1093/genetics/152.1.355</a>.","apa":"Goodman, S., Barton, N. H., Swanson, G., Abernethy, K., &#38; Pemberton, J. (1999). Introgression through rare hybridisation: A genetic study of a hybrid zone between red and sika deer (genus Cervus), in Argyll, Scotland. <i>Genetics</i>. Genetics Society of America. <a href=\"https://doi.org/10.1093/genetics/152.1.355\">https://doi.org/10.1093/genetics/152.1.355</a>","ama":"Goodman S, Barton NH, Swanson G, Abernethy K, Pemberton J. Introgression through rare hybridisation: A genetic study of a hybrid zone between red and sika deer (genus Cervus), in Argyll, Scotland. <i>Genetics</i>. 1999;152(1):355-371. doi:<a href=\"https://doi.org/10.1093/genetics/152.1.355\">10.1093/genetics/152.1.355</a>","ista":"Goodman S, Barton NH, Swanson G, Abernethy K, Pemberton J. 1999. Introgression through rare hybridisation: A genetic study of a hybrid zone between red and sika deer (genus Cervus), in Argyll, Scotland. Genetics. 152(1), 355–371.","mla":"Goodman, Simon, et al. “Introgression through Rare Hybridisation: A Genetic Study of a Hybrid Zone between Red and Sika Deer (Genus Cervus), in Argyll, Scotland.” <i>Genetics</i>, vol. 152, no. 1, Genetics Society of America, 1999, pp. 355–71, doi:<a href=\"https://doi.org/10.1093/genetics/152.1.355\">10.1093/genetics/152.1.355</a>.","short":"S. Goodman, N.H. Barton, G. Swanson, K. Abernethy, J. Pemberton, Genetics 152 (1999) 355–371."},"year":"1999","abstract":[{"lang":"eng","text":"In this article we describe the structure of a hybrid zone in Argyll, Scotland, between native red deer (Cervus elaphus) and introduced Japanese sika deer (Cervus nippon), on the basis of a genetic analysis using 11 microsatellite markers and mitochondrial DNA. In contrast to the findings of a previous study of the same population, we conclude that the deer fall into two distinct genetic classes, corresponding to either a sika-like or red- like phenotype. Introgression is rare at any one locus, but where the taxa overlap up to 40% of deer carry apparently introgressed alleles. While most putative hybrids are heterozygous at only one locus, there are rare multiple heterozygotes, reflecting significant linkage disequilibrium within both sika- and red-like populations. The rate of backcrossing into the sika population is estimated as H = 0.002 per generation and into red, H = 0.001 per generation. On the basis of historical evidence that red deer entered Kintyre only recently, a diffusion model evaluated by maximum likelihood shows that sika have increased at ~9.2% yr-1 from low frequency and disperse at a rate of ~3.7 km yr-1. Introgression into the red-like population is greater in the south, while introgression into sika varies little along the transect. For both sika- and red-like populations, the degree of introgression is 30-40% of that predicted from the rates of current hybridization inferred from linkage disequilibria; however, in neither case is this statistically significant evidence for selection against introgression."}],"doi":"10.1093/genetics/152.1.355","day":"01","extern":"1","acknowledgement":"We are grateful to Forest Enterprise in Argyll for providing the samples used in this study. We also thank Loeske Kruuk plus the communicating editor and two anonymous referees for their helpful comments on the manuscript. This work was supported by a Natural Environment Research Council grant to N.B. and J.P. and by a University of Edinburgh postgraduate bursary to G.S.","volume":152,"author":[{"first_name":"Simon","last_name":"Goodman","full_name":"Goodman, Simon"},{"orcid":"0000-0002-8548-5240","full_name":"Barton, Nicholas H","first_name":"Nicholas H","last_name":"Barton","id":"4880FE40-F248-11E8-B48F-1D18A9856A87"},{"first_name":"Graeme","last_name":"Swanson","full_name":"Swanson, Graeme"},{"last_name":"Abernethy","first_name":"Kate","full_name":"Abernethy, Kate"},{"full_name":"Pemberton, Josephine","first_name":"Josephine","last_name":"Pemberton"}],"issue":"1","_id":"4279","pmid":1,"scopus_import":"1","title":"Introgression through rare hybridisation: A genetic study of a hybrid zone between red and sika deer (genus Cervus), in Argyll, Scotland","intvolume":"       152","publication_status":"published","date_created":"2018-12-11T12:08:01Z","article_processing_charge":"No","page":"355 - 371","quality_controlled":"1","article_type":"original","publisher":"Genetics Society of America","date_published":"1999-05-01T00:00:00Z","type":"journal_article","publist_id":"1809","publication_identifier":{"issn":["0016-6731"]},"status":"public","user_id":"ea97e931-d5af-11eb-85d4-e6957dddbf17","publication":"Genetics","month":"05","oa_version":"None","language":[{"iso":"eng"}]},{"publisher":"University of California, Berkeley","language":[{"iso":"eng"}],"page":"1 - 150","title":"Algorithms and Methodology for Scalable Model Checking","month":"10","article_processing_charge":"No","date_created":"2018-12-11T12:08:43Z","publication_status":"published","oa_version":"None","author":[{"first_name":"Shaz","last_name":"Qadeer","full_name":"Qadeer, Shaz"}],"_id":"4411","user_id":"ea97e931-d5af-11eb-85d4-e6957dddbf17","status":"public","extern":"1","main_file_link":[{"url":"https://www.microsoft.com/en-us/research/publication/algorithms-methodology-scalable-model-checking/"}],"publist_id":"321","supervisor":[{"last_name":"Henzinger","first_name":"Thomas A","full_name":"Henzinger, Thomas A","orcid":"0000-0002-2985-7724","id":"40876CD8-F248-11E8-B48F-1D18A9856A87"},{"last_name":"Bryton","first_name":"Robert","full_name":"Bryton, Robert"},{"full_name":"Steel, John","first_name":"John","last_name":"Steel"}],"abstract":[{"lang":"eng","text":"Model checking algorithms for the verification of reactive systems proceed by a systematic and exhaustive exploration of the system state space. They do not scale to large designs because of the state explosion problem --the number of states grows exponentially with the number of components in the design. Consequently, the model checking problem is PSPACE-hard in the size of the design description. This dissertation proposes three novel techniques to combat the state explosion problem.\r\n\r\nOne of the most important advances in model checking in recent years has been the discovery of symbolic methods, which use a calculus of expressions, such as binary decision diagrams, to represent the state sets encountered during state space exploration. Symbolic model checking has proved to be effective for verifying hardware designs. Traditionally, symbolic checking of temporal logic specifications is performed by backward fixpoint reasoning with the operator Pre. Backward reasoning can be wasteful since unreachable states are explored. We suggest the use of forward fixpoint reasoning based on the operator Post. We show how all linear temporal logic specifications can be model checked symbolically by forward reasoning. In contrast to backward reasoning, forward reasoning performs computations only on the reachable states.\r\n\r\nHeuristics that improve algorithms for application domains, such as symbolic methods for hardware designs, are useful but not enough to make model checking feasible on industrial designs. Currently, exhaustive state exploration is possible only on designs with about 50-100 boolean state variables. Assume-guarantee verification attempts to combat the state explosion problem by using the principle of &quot;divide and conquer,&quot; where the components of the implementation are analyzed one at a time. Typically, an implementation component refines its specification only when its inputs are suitably constrained by other components in the implementation. The assume-guarantee principle states that instead of constraining the inputs by implementation components, it is sound to constrain them by the corresponding specification components, which can be significantly smaller. We extend the assume-guarantee proof rule to deal with the case where the specification operates at a coarser time scale than the implementation. Using our model checker Mocha, which implements this methodology, we verify VGI, a parallel DSP processor chip with 64 compute processors each containing approximately 800 state variables and 30K gates.\r\n\r\nOur third contribution is a systematic model checking methodology for verifying the abstract shared-memory interface of sequential consistency on multiprocessor systems with three parameters --number of processors, number of memory locations, and number of data values. Sequential consistency requires that some interleaving of the local temporal orders of read/write events at different processors be a trace of serial memory. Therefore, it suffices to construct a non-interfering serializer that watches and reorders read/write events so that a trace of serial memory is obtained. While in general such a serializer must be unbounded even for fixed values of the parameters --checking sequential consistency is undecidable!-- we show that the paradigmatic class of snoopy cache coherence protocols has finite-state serializers. In order to reduce the arbitrary-parameter problem to the fixed-parameter problem, we develop a novel framework for induction over the number of processors and use the notion of a serializer to reduce the problem of verifying sequential consistency to that of checking language inclusion between finite state machines."}],"day":"01","degree_awarded":"PhD","type":"dissertation","date_published":"1999-10-01T00:00:00Z","year":"1999","citation":{"chicago":"Qadeer, Shaz. “Algorithms and Methodology for Scalable Model Checking.” University of California, Berkeley, 1999.","ieee":"S. Qadeer, “Algorithms and Methodology for Scalable Model Checking,” University of California, Berkeley, 1999.","ama":"Qadeer S. Algorithms and Methodology for Scalable Model Checking. 1999:1-150.","apa":"Qadeer, S. (1999). <i>Algorithms and Methodology for Scalable Model Checking</i>. University of California, Berkeley.","ista":"Qadeer S. 1999. Algorithms and Methodology for Scalable Model Checking. University of California, Berkeley.","mla":"Qadeer, Shaz. <i>Algorithms and Methodology for Scalable Model Checking</i>. University of California, Berkeley, 1999, pp. 1–150.","short":"S. Qadeer, Algorithms and Methodology for Scalable Model Checking, University of California, Berkeley, 1999."},"date_updated":"2022-09-06T08:07:40Z"},{"abstract":[{"text":"Rectangular hybrid automata model digital control programs of analog plant environments. We study rectangular hybrid automata where the plant state evolves continuously in real-numbered time, and the controller samples the plant state and changes the control state discretely, only at the integer points in time. We prove that rectangular hybrid automata have finite bisimilarity quotients when all control transitions happen at integer times, even if the constraints on the derivatives of the variables vary between control states. This is in contrast with the conventional model where control transitions may happen at any real time, and already the reachability problem is undecidable. Based on the finite bisimilarity quotients, we give an exponential algorithm for the symbolic sampling-controller synthesis of rectangular automata. We show our algorithm to be optimal by proving the problem to be EXPTIME-hard. We also show that rectangular automata form a maximal class of systems for which the sampling-controller synthesis problem can be solved algorithmically.","lang":"eng"}],"doi":"10.1016/S0304-3975(99)00038-9","day":"01","date_updated":"2022-09-06T08:03:48Z","citation":{"chicago":"Henzinger, Thomas A, and Peter Kopke. “Discrete-Time Control for Rectangular Hybrid Automata.” <i>Theoretical Computer Science</i>. Elsevier, 1999. <a href=\"https://doi.org/10.1016/S0304-3975(99)00038-9\">https://doi.org/10.1016/S0304-3975(99)00038-9</a>.","ieee":"T. A. Henzinger and P. Kopke, “Discrete-time control for rectangular hybrid automata,” <i>Theoretical Computer Science</i>, vol. 221, no. 1–2. Elsevier, pp. 369–392, 1999.","ama":"Henzinger TA, Kopke P. Discrete-time control for rectangular hybrid automata. <i>Theoretical Computer Science</i>. 1999;221(1-2):369-392. doi:<a href=\"https://doi.org/10.1016/S0304-3975(99)00038-9\">10.1016/S0304-3975(99)00038-9</a>","apa":"Henzinger, T. A., &#38; Kopke, P. (1999). Discrete-time control for rectangular hybrid automata. <i>Theoretical Computer Science</i>. Elsevier. <a href=\"https://doi.org/10.1016/S0304-3975(99)00038-9\">https://doi.org/10.1016/S0304-3975(99)00038-9</a>","ista":"Henzinger TA, Kopke P. 1999. Discrete-time control for rectangular hybrid automata. Theoretical Computer Science. 221(1–2), 369–392.","mla":"Henzinger, Thomas A., and Peter Kopke. “Discrete-Time Control for Rectangular Hybrid Automata.” <i>Theoretical Computer Science</i>, vol. 221, no. 1–2, Elsevier, 1999, pp. 369–92, doi:<a href=\"https://doi.org/10.1016/S0304-3975(99)00038-9\">10.1016/S0304-3975(99)00038-9</a>.","short":"T.A. Henzinger, P. Kopke, Theoretical Computer Science 221 (1999) 369–392."},"year":"1999","extern":"1","volume":221,"title":"Discrete-time control for rectangular hybrid automata","intvolume":"       221","publication_status":"published","date_created":"2018-12-11T12:08:52Z","article_processing_charge":"No","author":[{"id":"40876CD8-F248-11E8-B48F-1D18A9856A87","last_name":"Henzinger","first_name":"Thomas A","full_name":"Henzinger, Thomas A","orcid":"0000−0002−2985−7724"},{"full_name":"Kopke, Peter","last_name":"Kopke","first_name":"Peter"}],"issue":"1-2","_id":"4442","scopus_import":"1","article_type":"original","publisher":"Elsevier","page":"369 - 392","quality_controlled":"1","publist_id":"290","publication_identifier":{"issn":["0304-3975"]},"date_published":"1999-01-01T00:00:00Z","type":"journal_article","user_id":"ea97e931-d5af-11eb-85d4-e6957dddbf17","status":"public","month":"01","oa_version":"None","publication":"Theoretical Computer Science","language":[{"iso":"eng"}]},{"conference":{"location":"San Jose, CA, United States of America","end_date":"1999-11-11","start_date":"1999-11-07","name":"ICCAD: Computer-Aided Design"},"publisher":"IEEE","language":[{"iso":"eng"}],"page":"494 - 499","quality_controlled":"1","month":"01","title":"Formal specification and verification of a dataflow processor array","oa_version":"None","publication_status":"published","article_processing_charge":"No","date_created":"2018-12-11T12:09:04Z","author":[{"id":"40876CD8-F248-11E8-B48F-1D18A9856A87","full_name":"Henzinger, Thomas A","orcid":"0000−0002−2985−7724","last_name":"Henzinger","first_name":"Thomas A"},{"first_name":"Xiaojun","last_name":"Liu","full_name":"Liu, Xiaojun"},{"full_name":"Qadeer, Shaz","first_name":"Shaz","last_name":"Qadeer"},{"full_name":"Rajamani, Sriram","last_name":"Rajamani","first_name":"Sriram"}],"_id":"4480","scopus_import":"1","extern":"1","status":"public","user_id":"ea97e931-d5af-11eb-85d4-e6957dddbf17","abstract":[{"text":"We describe the formal specification and verification of the VGI parallel DSP chip [1], which contains 64 compute processors with ~30K gates in each processor. Our effort coincided in time with the “informal” verification stage of the chip. By interacting with the designers, we produced an abstract but executable specification of the design which embodies the programmer's view of the system. Given the size of the design, an automatic check that even one of the 64 processors satisfies its specification is well beyond the scope of current verification tools. However, the check can be decomposed using assume-guarantee reasoning. For VGI, the implementation and specification operate at different time scales: several steps of the implementation correspond to a single step in the specification. We generalized both the assume-guarantee method and our model checker MOCHA to allow compositional verification for such applications. We used our proof rule to decompose the verification problem of the VGI chip into smaller proof obligations that were discharged automatically by MOCHA. Using our formal approach, we uncovered and fixed subtle bugs that were unknown to the designers.","lang":"eng"}],"publist_id":"246","doi":"10.1109/ICCAD.1999.810700","day":"01","publication_identifier":{"issn":["1092-3152"]},"date_published":"1999-01-01T00:00:00Z","type":"conference","date_updated":"2022-09-05T14:48:48Z","citation":{"apa":"Henzinger, T. A., Liu, X., Qadeer, S., &#38; Rajamani, S. (1999). Formal specification and verification of a dataflow processor array (pp. 494–499). Presented at the ICCAD: Computer-Aided Design, San Jose, CA, United States of America: IEEE. <a href=\"https://doi.org/10.1109/ICCAD.1999.810700\">https://doi.org/10.1109/ICCAD.1999.810700</a>","ama":"Henzinger TA, Liu X, Qadeer S, Rajamani S. Formal specification and verification of a dataflow processor array. In: IEEE; 1999:494-499. doi:<a href=\"https://doi.org/10.1109/ICCAD.1999.810700\">10.1109/ICCAD.1999.810700</a>","chicago":"Henzinger, Thomas A, Xiaojun Liu, Shaz Qadeer, and Sriram Rajamani. “Formal Specification and Verification of a Dataflow Processor Array,” 494–99. IEEE, 1999. <a href=\"https://doi.org/10.1109/ICCAD.1999.810700\">https://doi.org/10.1109/ICCAD.1999.810700</a>.","ieee":"T. A. Henzinger, X. Liu, S. Qadeer, and S. Rajamani, “Formal specification and verification of a dataflow processor array,” presented at the ICCAD: Computer-Aided Design, San Jose, CA, United States of America, 1999, pp. 494–499.","mla":"Henzinger, Thomas A., et al. <i>Formal Specification and Verification of a Dataflow Processor Array</i>. IEEE, 1999, pp. 494–99, doi:<a href=\"https://doi.org/10.1109/ICCAD.1999.810700\">10.1109/ICCAD.1999.810700</a>.","short":"T.A. Henzinger, X. Liu, S. Qadeer, S. Rajamani, in:, IEEE, 1999, pp. 494–499.","ista":"Henzinger TA, Liu X, Qadeer S, Rajamani S. 1999. Formal specification and verification of a dataflow processor array. ICCAD: Computer-Aided Design, 494–499."},"year":"1999"},{"publication":"Proceedings of the 11th International Conference on Computer Aided Verification","_id":"4484","author":[{"id":"40876CD8-F248-11E8-B48F-1D18A9856A87","full_name":"Henzinger, Thomas A","orcid":"0000−0002−2985−7724","last_name":"Henzinger","first_name":"Thomas A"},{"first_name":"Shaz","last_name":"Qadeer","full_name":"Qadeer, Shaz"},{"first_name":"Sriram","last_name":"Rajamani","full_name":"Rajamani, Sriram"}],"publication_status":"published","oa_version":"None","date_created":"2018-12-11T12:09:05Z","article_processing_charge":"No","title":"Verifying sequential consistency on shared-memory multiprocessor systems","alternative_title":["LNCS"],"month":"01","intvolume":"      1633","page":"301 - 315","quality_controlled":"1","language":[{"iso":"eng"}],"publisher":"Springer","conference":{"location":"Trento, Italy","end_date":"1999-07-10","start_date":"1999-07-06","name":"CAV: Computer Aided Verification"},"date_updated":"2022-09-02T09:21:11Z","citation":{"ama":"Henzinger TA, Qadeer S, Rajamani S. Verifying sequential consistency on shared-memory multiprocessor systems. In: <i>Proceedings of the 11th International Conference on Computer Aided Verification</i>. Vol 1633. Springer; 1999:301-315. doi:<a href=\"https://doi.org/10.1007/3-540-48683-6_27\">10.1007/3-540-48683-6_27</a>","apa":"Henzinger, T. A., Qadeer, S., &#38; Rajamani, S. (1999). Verifying sequential consistency on shared-memory multiprocessor systems. In <i>Proceedings of the 11th International Conference on Computer Aided Verification</i> (Vol. 1633, pp. 301–315). Trento, Italy: Springer. <a href=\"https://doi.org/10.1007/3-540-48683-6_27\">https://doi.org/10.1007/3-540-48683-6_27</a>","ieee":"T. A. Henzinger, S. Qadeer, and S. Rajamani, “Verifying sequential consistency on shared-memory multiprocessor systems,” in <i>Proceedings of the 11th International Conference on Computer Aided Verification</i>, Trento, Italy, 1999, vol. 1633, pp. 301–315.","chicago":"Henzinger, Thomas A, Shaz Qadeer, and Sriram Rajamani. “Verifying Sequential Consistency on Shared-Memory Multiprocessor Systems.” In <i>Proceedings of the 11th International Conference on Computer Aided Verification</i>, 1633:301–15. Springer, 1999. <a href=\"https://doi.org/10.1007/3-540-48683-6_27\">https://doi.org/10.1007/3-540-48683-6_27</a>.","short":"T.A. Henzinger, S. Qadeer, S. Rajamani, in:, Proceedings of the 11th International Conference on Computer Aided Verification, Springer, 1999, pp. 301–315.","mla":"Henzinger, Thomas A., et al. “Verifying Sequential Consistency on Shared-Memory Multiprocessor Systems.” <i>Proceedings of the 11th International Conference on Computer Aided Verification</i>, vol. 1633, Springer, 1999, pp. 301–15, doi:<a href=\"https://doi.org/10.1007/3-540-48683-6_27\">10.1007/3-540-48683-6_27</a>.","ista":"Henzinger TA, Qadeer S, Rajamani S. 1999. Verifying sequential consistency on shared-memory multiprocessor systems. Proceedings of the 11th International Conference on Computer Aided Verification. CAV: Computer Aided Verification, LNCS, vol. 1633, 301–315."},"year":"1999","date_published":"1999-01-01T00:00:00Z","type":"conference","doi":"10.1007/3-540-48683-6_27","day":"01","publication_identifier":{"isbn":["9783540662020"]},"abstract":[{"text":"In shared-memory multiprocessors sequential consistency offers a natural tradeoff between the flexibility afforded to the implementor and the complexity of the programmer’s view of the memory. Sequential consistency requires that some interleaving of the local temporal orders of read/write events at different processors be a trace of serial memory. We develop a systematic methodology for proving sequential consistency for memory systems with three parameters —number of processors, number of memory locations, and number of data values. From the definition of sequential consistency it suffices to construct a non-interfering observer that watches and reorders read/write events so that a trace of serial memory is obtained. While in general such an observer must be unbounded even for fixed values of the parameters —checking sequential consistency is undecidable!— we show that for two paradigmatic protocol classes—lazy caching and snoopy cache coherence—there exist finite-state observers. In these cases, sequential consistency for fixed parameter values can thus be checked by language inclusion between finite automata.\r\nIn order to reduce the arbitrary-parameter problem to the fixed-parameter problem, we develop a novel framework for induction over the number of processors. Classical induction schemas, which are based on process invariants that are inductive with respect to an implementation preorder that preserves the temporal sequence of events, are inadequate for our purposes, because proving sequential consistency requires the reordering of events. Hence we introduce merge invariants, which permit certain reorderings of read/write events. We show that under certain reasonable assumptions about the memory system, it is possible to conclude sequential consistency for any number of processors, memory locations, and data values by model checking two finite-state lemmas about process and merge invariants: they involve two processors each accessing a maximum of three locations, where each location stores at most two data values. For both lazy caching and snoopy cache coherence we are able to discharge the two lemmas using the model checker MOCHA.","lang":"eng"}],"publist_id":"244","volume":1633,"extern":"1","user_id":"ea97e931-d5af-11eb-85d4-e6957dddbf17","status":"public"},{"date_published":"1999-01-01T00:00:00Z","type":"conference","publist_id":"245","publication_identifier":{"isbn":["9783540664253"]},"user_id":"ea97e931-d5af-11eb-85d4-e6957dddbf17","status":"public","publication":"Proceedings of the 10th International Conference on Concurrency Theory","month":"01","oa_version":"None","language":[{"iso":"eng"}],"conference":{"location":"Eindhoven, The Netherlands","name":"CONCUR: Concurrency Theory"},"date_updated":"2022-09-02T10:54:12Z","citation":{"apa":"Henzinger, T. A., Horowitz, B., &#38; Majumdar, R. (1999). Rectangular hybrid games. In <i>Proceedings of the 10th International Conference on Concurrency Theory</i> (Vol. 1664, pp. 320–335). Eindhoven, The Netherlands: Schloss Dagstuhl - Leibniz-Zentrum für Informatik. <a href=\"https://doi.org/10.1007/3-540-48320-9_23\">https://doi.org/10.1007/3-540-48320-9_23</a>","ama":"Henzinger TA, Horowitz B, Majumdar R. Rectangular hybrid games. In: <i>Proceedings of the 10th International Conference on Concurrency Theory</i>. Vol 1664. Schloss Dagstuhl - Leibniz-Zentrum für Informatik; 1999:320-335. doi:<a href=\"https://doi.org/10.1007/3-540-48320-9_23\">10.1007/3-540-48320-9_23</a>","chicago":"Henzinger, Thomas A, Benjamin Horowitz, and Ritankar Majumdar. “Rectangular Hybrid Games.” In <i>Proceedings of the 10th International Conference on Concurrency Theory</i>, 1664:320–35. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 1999. <a href=\"https://doi.org/10.1007/3-540-48320-9_23\">https://doi.org/10.1007/3-540-48320-9_23</a>.","ieee":"T. A. Henzinger, B. Horowitz, and R. Majumdar, “Rectangular hybrid games,” in <i>Proceedings of the 10th International Conference on Concurrency Theory</i>, Eindhoven, The Netherlands, 1999, vol. 1664, pp. 320–335.","mla":"Henzinger, Thomas A., et al. “Rectangular Hybrid Games.” <i>Proceedings of the 10th International Conference on Concurrency Theory</i>, vol. 1664, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 1999, pp. 320–35, doi:<a href=\"https://doi.org/10.1007/3-540-48320-9_23\">10.1007/3-540-48320-9_23</a>.","short":"T.A. Henzinger, B. Horowitz, R. Majumdar, in:, Proceedings of the 10th International Conference on Concurrency Theory, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 1999, pp. 320–335.","ista":"Henzinger TA, Horowitz B, Majumdar R. 1999. Rectangular hybrid games. Proceedings of the 10th International Conference on Concurrency Theory. CONCUR: Concurrency Theory, LNCS, vol. 1664, 320–335."},"year":"1999","abstract":[{"text":"In order to study control problems for hybrid systems, we generalize hybrid automata to hybrid games —say, controller vs. plant. If we specify the continuous dynamics by constant lower and upper bounds, we obtain rectangular games. We show that for rectangular games with objectives expressed in Ltl (linear temporal logic), the winning states for each player can be computed, and winning strategies can be synthesized. Our result is sharp, as already reachability is undecidable for generalizations of rectangular systems, and optimal —singly exponential in the size of the game structure and doubly exponential in the size of the Ltl objective. Our proof systematically generalizes the theory of hybrid systems from automata (single-player structures) [9] to games (multi-player structures): we show that the successively more general infinite-state classes of timed, 2D rectangular, and rectangular games induce successively weaker, but still finite, quotient structures called game bisimilarity, game similarity, and game trace equivalence. These quotients can be used, in particular, to solve the Ltl control problem.","lang":"eng"}],"doi":"10.1007/3-540-48320-9_23","day":"01","extern":"1","volume":1664,"acknowledgement":"This research was supported in part by the NSF CAREER award CCR-9501708, by the NSF grant CCR-9504469, by the DARPA (NASA Ames) grant NAG2-1214, by the DARPA (Wright-Patterson AFB) grant F33615-98-C-3614, and by the ARO MURI grant DAAH-04-96-1-0341.","author":[{"id":"40876CD8-F248-11E8-B48F-1D18A9856A87","full_name":"Henzinger, Thomas A","orcid":"0000−0002−2985−7724","last_name":"Henzinger","first_name":"Thomas A"},{"full_name":"Horowitz, Benjamin","last_name":"Horowitz","first_name":"Benjamin"},{"full_name":"Majumdar, Ritankar","first_name":"Ritankar","last_name":"Majumdar"}],"_id":"4485","title":"Rectangular hybrid games","alternative_title":["LNCS"],"intvolume":"      1664","publication_status":"published","article_processing_charge":"No","date_created":"2018-12-11T12:09:05Z","page":"320 - 335","quality_controlled":"1","publisher":"Schloss Dagstuhl - Leibniz-Zentrum für Informatik"},{"_id":"4487","publication":"Proceedings of the 11th International Conference on Computer Aided Verification","author":[{"first_name":"Thomas A","last_name":"Henzinger","orcid":"0000−0002−2985−7724","full_name":"Henzinger, Thomas A","id":"40876CD8-F248-11E8-B48F-1D18A9856A87"},{"full_name":"Qadeer, Shaz","last_name":"Qadeer","first_name":"Shaz"},{"last_name":"Rajamani","first_name":"Sriram","full_name":"Rajamani, Sriram"}],"publication_status":"published","oa_version":"None","article_processing_charge":"No","date_created":"2018-12-11T12:09:06Z","title":"Assume-guarantee refinement between different time scales","alternative_title":["LNCS"],"month":"01","intvolume":"      1633","page":"208 - 221","quality_controlled":"1","language":[{"iso":"eng"}],"publisher":"Springer","conference":{"location":"Trento, Italy","end_date":"1999-07-10","start_date":"1999-07-06","name":"CAV: Computer Aided Verification"},"date_updated":"2022-09-02T09:04:26Z","year":"1999","citation":{"ista":"Henzinger TA, Qadeer S, Rajamani S. 1999. Assume-guarantee refinement between different time scales. Proceedings of the 11th International Conference on Computer Aided Verification. CAV: Computer Aided Verification, LNCS, vol. 1633, 208–221.","mla":"Henzinger, Thomas A., et al. “Assume-Guarantee Refinement between Different Time Scales.” <i>Proceedings of the 11th International Conference on Computer Aided Verification</i>, vol. 1633, Springer, 1999, pp. 208–21, doi:<a href=\"https://doi.org/10.1007/3-540-48683-6_20\">10.1007/3-540-48683-6_20</a>.","short":"T.A. Henzinger, S. Qadeer, S. Rajamani, in:, Proceedings of the 11th International Conference on Computer Aided Verification, Springer, 1999, pp. 208–221.","ieee":"T. A. Henzinger, S. Qadeer, and S. Rajamani, “Assume-guarantee refinement between different time scales,” in <i>Proceedings of the 11th International Conference on Computer Aided Verification</i>, Trento, Italy, 1999, vol. 1633, pp. 208–221.","chicago":"Henzinger, Thomas A, Shaz Qadeer, and Sriram Rajamani. “Assume-Guarantee Refinement between Different Time Scales.” In <i>Proceedings of the 11th International Conference on Computer Aided Verification</i>, 1633:208–21. Springer, 1999. <a href=\"https://doi.org/10.1007/3-540-48683-6_20\">https://doi.org/10.1007/3-540-48683-6_20</a>.","apa":"Henzinger, T. A., Qadeer, S., &#38; Rajamani, S. (1999). Assume-guarantee refinement between different time scales. In <i>Proceedings of the 11th International Conference on Computer Aided Verification</i> (Vol. 1633, pp. 208–221). Trento, Italy: Springer. <a href=\"https://doi.org/10.1007/3-540-48683-6_20\">https://doi.org/10.1007/3-540-48683-6_20</a>","ama":"Henzinger TA, Qadeer S, Rajamani S. Assume-guarantee refinement between different time scales. In: <i>Proceedings of the 11th International Conference on Computer Aided Verification</i>. Vol 1633. Springer; 1999:208-221. doi:<a href=\"https://doi.org/10.1007/3-540-48683-6_20\">10.1007/3-540-48683-6_20</a>"},"date_published":"1999-01-01T00:00:00Z","type":"conference","doi":"10.1007/3-540-48683-6_20","publication_identifier":{"isbn":["9783540662020"]},"day":"01","abstract":[{"lang":"eng","text":"Refinement checking is used to verify implementations against more abstract specifications. Assume-guarantee reasoning is used to decompose refinement proofs in order to avoid state-space explosion. In previous approaches, specifications are forced to operate on the same time scale as the implementation. This may lead to unnatural specifications and inefficiencies in verification. We introduce a novel methodology for decomposing refinement proofs of temporally abstract specifications, which specify implementation requirements only at certain sampling instances in time. Our new assume-guarantee rule allows separate refinement maps for specifying functionality and timing.We present the theory for the correctness of our methodology, and illustrate it using a simple example. Support for sampling and the generalized assume-guarantee rule have been implemented in the model checker Mocha and successfully applied to verify the VGI multiprocessor dataflow chip with 6 million transistors."}],"publist_id":"243","volume":1633,"extern":"1","status":"public","user_id":"ea97e931-d5af-11eb-85d4-e6957dddbf17"}]