[{"date_published":"1999-10-01T00:00:00Z","publisher":"Wiley-Blackwell","quality_controlled":"1","volume":53,"extern":"1","page":"1611 - 1616","publication_status":"published","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"}],"external_id":{"pmid":["28565554"]},"_id":"4277","article_type":"original","doi":"10.2307/2640907","year":"1999","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.","date_created":"2018-12-11T12:08:00Z","citation":{"short":"L. Kruuk, J. Gilchrist, N.H. Barton, Evolution; International Journal of Organic Evolution 53 (1999) 1611–1616.","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.","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>","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.","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>.","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>.","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>"},"publist_id":"1811","status":"public","type":"journal_article","pmid":1,"author":[{"last_name":"Kruuk","full_name":"Kruuk, Loeske","first_name":"Loeske"},{"last_name":"Gilchrist","full_name":"Gilchrist, Jason","first_name":"Jason"},{"id":"4880FE40-F248-11E8-B48F-1D18A9856A87","last_name":"Barton","orcid":"0000-0002-8548-5240","first_name":"Nicholas H","full_name":"Barton, Nicholas H"}],"publication_identifier":{"issn":["0014-3820"]},"month":"10","user_id":"ea97e931-d5af-11eb-85d4-e6957dddbf17","oa_version":"None","day":"01","language":[{"iso":"eng"}],"publication":"Evolution; International Journal of Organic Evolution","article_processing_charge":"No","issue":"5","date_updated":"2022-09-06T08:20:03Z","title":"Hybrid dysfunction in fire-bellied toads (Bombina)","intvolume":"        53","scopus_import":"1"},{"language":[{"iso":"eng"}],"publication":"Genetics","issue":"1","article_processing_charge":"No","date_updated":"2022-09-06T08:12:14Z","title":"Introgression through rare hybridisation: A genetic study of a hybrid zone between red and sika deer (genus Cervus), in Argyll, Scotland","scopus_import":"1","intvolume":"       152","status":"public","type":"journal_article","pmid":1,"author":[{"full_name":"Goodman, Simon","first_name":"Simon","last_name":"Goodman"},{"full_name":"Barton, Nicholas H","first_name":"Nicholas H","orcid":"0000-0002-8548-5240","id":"4880FE40-F248-11E8-B48F-1D18A9856A87","last_name":"Barton"},{"first_name":"Graeme","full_name":"Swanson, Graeme","last_name":"Swanson"},{"last_name":"Abernethy","first_name":"Kate","full_name":"Abernethy, Kate"},{"last_name":"Pemberton","first_name":"Josephine","full_name":"Pemberton, Josephine"}],"month":"05","publication_identifier":{"issn":["0016-6731"]},"user_id":"ea97e931-d5af-11eb-85d4-e6957dddbf17","oa_version":"None","day":"01","_id":"4279","article_type":"original","doi":"10.1093/genetics/152.1.355","year":"1999","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.","date_created":"2018-12-11T12:08:01Z","publist_id":"1809","citation":{"short":"S. Goodman, N.H. Barton, G. Swanson, K. Abernethy, J. Pemberton, Genetics 152 (1999) 355–371.","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>","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.","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>.","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.","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>"},"date_published":"1999-05-01T00:00:00Z","publisher":"Genetics Society of America","quality_controlled":"1","volume":152,"page":"355 - 371","extern":"1","publication_status":"published","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."}],"external_id":{"pmid":["10224266"]}},{"extern":"1","page":"1 - 150","publisher":"University of California, Berkeley","status":"public","supervisor":[{"first_name":"Thomas A","full_name":"Henzinger, Thomas A","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","last_name":"Henzinger","orcid":"0000-0002-2985-7724"},{"full_name":"Bryton, Robert","first_name":"Robert","last_name":"Bryton"},{"first_name":"John","full_name":"Steel, John","last_name":"Steel"}],"date_published":"1999-10-01T00:00:00Z","type":"dissertation","oa_version":"None","main_file_link":[{"url":"https://www.microsoft.com/en-us/research/publication/algorithms-methodology-scalable-model-checking/"}],"day":"01","user_id":"ea97e931-d5af-11eb-85d4-e6957dddbf17","abstract":[{"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.","lang":"eng"}],"month":"10","publication_status":"published","author":[{"last_name":"Qadeer","first_name":"Shaz","full_name":"Qadeer, Shaz"}],"language":[{"iso":"eng"}],"_id":"4411","degree_awarded":"PhD","publist_id":"321","date_created":"2018-12-11T12:08:43Z","title":"Algorithms and Methodology for Scalable Model Checking","citation":{"ama":"Qadeer S. Algorithms and Methodology for Scalable Model Checking. 1999:1-150.","ieee":"S. Qadeer, “Algorithms and Methodology for Scalable Model Checking,” University of California, Berkeley, 1999.","short":"S. Qadeer, Algorithms and Methodology for Scalable Model Checking, University of California, Berkeley, 1999.","chicago":"Qadeer, Shaz. “Algorithms and Methodology for Scalable Model Checking.” University of California, Berkeley, 1999.","mla":"Qadeer, Shaz. <i>Algorithms and Methodology for Scalable Model Checking</i>. University of California, Berkeley, 1999, pp. 1–150.","ista":"Qadeer S. 1999. Algorithms and Methodology for Scalable Model Checking. University of California, Berkeley.","apa":"Qadeer, S. (1999). <i>Algorithms and Methodology for Scalable Model Checking</i>. University of California, Berkeley."},"date_updated":"2022-09-06T08:07:40Z","article_processing_charge":"No","year":"1999"},{"language":[{"iso":"eng"}],"publication":"Theoretical Computer Science","title":"Discrete-time control for rectangular hybrid automata","date_updated":"2022-09-06T08:03:48Z","article_processing_charge":"No","issue":"1-2","intvolume":"       221","scopus_import":"1","status":"public","type":"journal_article","author":[{"last_name":"Henzinger","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","orcid":"0000−0002−2985−7724","full_name":"Henzinger, Thomas A","first_name":"Thomas A"},{"last_name":"Kopke","first_name":"Peter","full_name":"Kopke, Peter"}],"day":"01","oa_version":"None","user_id":"ea97e931-d5af-11eb-85d4-e6957dddbf17","month":"01","publication_identifier":{"issn":["0304-3975"]},"article_type":"original","_id":"4442","doi":"10.1016/S0304-3975(99)00038-9","citation":{"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>","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>","short":"T.A. Henzinger, P. Kopke, Theoretical Computer Science 221 (1999) 369–392.","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>.","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>.","ista":"Henzinger TA, Kopke P. 1999. Discrete-time control for rectangular hybrid automata. Theoretical Computer Science. 221(1–2), 369–392."},"publist_id":"290","date_created":"2018-12-11T12:08:52Z","year":"1999","extern":"1","page":"369 - 392","quality_controlled":"1","volume":221,"publisher":"Elsevier","date_published":"1999-01-01T00:00:00Z","publication_status":"published","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"}]},{"scopus_import":"1","article_processing_charge":"No","year":"1999","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>","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.","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>","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.","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>.","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>."},"date_created":"2018-12-11T12:09:04Z","title":"Formal specification and verification of a dataflow processor array","publist_id":"246","doi":"10.1109/ICCAD.1999.810700","language":[{"iso":"eng"}],"_id":"4480","month":"01","publication_identifier":{"issn":["1092-3152"]},"conference":{"end_date":"1999-11-11","location":"San Jose, CA, United States of America","start_date":"1999-11-07","name":"ICCAD: Computer-Aided Design"},"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"}],"oa_version":"None","day":"01","publication_status":"published","author":[{"id":"40876CD8-F248-11E8-B48F-1D18A9856A87","last_name":"Henzinger","orcid":"0000−0002−2985−7724","first_name":"Thomas A","full_name":"Henzinger, Thomas A"},{"full_name":"Liu, Xiaojun","first_name":"Xiaojun","last_name":"Liu"},{"first_name":"Shaz","full_name":"Qadeer, Shaz","last_name":"Qadeer"},{"first_name":"Sriram","full_name":"Rajamani, Sriram","last_name":"Rajamani"}],"date_published":"1999-01-01T00:00:00Z","type":"conference","status":"public","publisher":"IEEE","quality_controlled":"1","page":"494 - 499","extern":"1"},{"date_updated":"2022-09-02T09:21:11Z","article_processing_charge":"No","year":"1999","citation":{"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>.","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.","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>.","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>","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.","short":"T.A. Henzinger, S. Qadeer, S. Rajamani, in:, Proceedings of the 11th International Conference on Computer Aided Verification, Springer, 1999, pp. 301–315.","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>"},"date_created":"2018-12-11T12:09:05Z","title":"Verifying sequential consistency on shared-memory multiprocessor systems","publist_id":"244","intvolume":"      1633","_id":"4484","language":[{"iso":"eng"}],"publication":"Proceedings of the 11th International Conference on Computer Aided Verification","doi":"10.1007/3-540-48683-6_27","publication_status":"published","author":[{"last_name":"Henzinger","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","orcid":"0000−0002−2985−7724","first_name":"Thomas A","full_name":"Henzinger, Thomas A"},{"first_name":"Shaz","full_name":"Qadeer, Shaz","last_name":"Qadeer"},{"last_name":"Rajamani","full_name":"Rajamani, Sriram","first_name":"Sriram"}],"conference":{"start_date":"1999-07-06","name":"CAV: Computer Aided Verification","end_date":"1999-07-10","location":"Trento, Italy"},"month":"01","publication_identifier":{"isbn":["9783540662020"]},"oa_version":"None","day":"01","user_id":"ea97e931-d5af-11eb-85d4-e6957dddbf17","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"}],"publisher":"Springer","alternative_title":["LNCS"],"status":"public","date_published":"1999-01-01T00:00:00Z","type":"conference","extern":"1","page":"301 - 315","volume":1633,"quality_controlled":"1"},{"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.","year":"1999","date_created":"2018-12-11T12:09:05Z","citation":{"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.","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>","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.","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>.","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>.","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>"},"publist_id":"245","_id":"4485","doi":"10.1007/3-540-48320-9_23","publication_status":"published","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"}],"publisher":"Schloss Dagstuhl - Leibniz-Zentrum für Informatik","date_published":"1999-01-01T00:00:00Z","extern":"1","page":"320 - 335","volume":1664,"quality_controlled":"1","date_updated":"2022-09-02T10:54:12Z","article_processing_charge":"No","title":"Rectangular hybrid games","intvolume":"      1664","language":[{"iso":"eng"}],"publication":"Proceedings of the 10th International Conference on Concurrency Theory","author":[{"last_name":"Henzinger","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","orcid":"0000−0002−2985−7724","first_name":"Thomas A","full_name":"Henzinger, Thomas A"},{"full_name":"Horowitz, Benjamin","first_name":"Benjamin","last_name":"Horowitz"},{"full_name":"Majumdar, Ritankar","first_name":"Ritankar","last_name":"Majumdar"}],"conference":{"location":"Eindhoven, The Netherlands","name":"CONCUR: Concurrency Theory"},"publication_identifier":{"isbn":["9783540664253"]},"month":"01","oa_version":"None","day":"01","user_id":"ea97e931-d5af-11eb-85d4-e6957dddbf17","alternative_title":["LNCS"],"status":"public","type":"conference"},{"publication":"Proceedings of the 11th International Conference on Computer Aided Verification","doi":"10.1007/3-540-48683-6_20","language":[{"iso":"eng"}],"_id":"4487","intvolume":"      1633","article_processing_charge":"No","year":"1999","date_updated":"2022-09-02T09:04:26Z","title":"Assume-guarantee refinement between different time scales","date_created":"2018-12-11T12:09:06Z","publist_id":"243","citation":{"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>","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.","short":"T.A. Henzinger, S. Qadeer, S. Rajamani, in:, Proceedings of the 11th International Conference on Computer Aided Verification, Springer, 1999, pp. 208–221.","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>.","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>."},"date_published":"1999-01-01T00:00:00Z","type":"conference","status":"public","alternative_title":["LNCS"],"publisher":"Springer","quality_controlled":"1","volume":1633,"extern":"1","page":"208 - 221","month":"01","publication_identifier":{"isbn":["9783540662020"]},"conference":{"name":"CAV: Computer Aided Verification","start_date":"1999-07-06","location":"Trento, Italy","end_date":"1999-07-10"},"user_id":"ea97e931-d5af-11eb-85d4-e6957dddbf17","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."}],"oa_version":"None","day":"01","publication_status":"published","author":[{"orcid":"0000−0002−2985−7724","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","last_name":"Henzinger","full_name":"Henzinger, Thomas A","first_name":"Thomas A"},{"full_name":"Qadeer, Shaz","first_name":"Shaz","last_name":"Qadeer"},{"last_name":"Rajamani","first_name":"Sriram","full_name":"Rajamani, Sriram"}]},{"_id":"4582","article_type":"original","doi":"10.1023/A:1008739929481","citation":{"chicago":"Alur, Rajeev, and Thomas A Henzinger. “Reactive Modules.” <i>Formal Methods in System Design</i>. Springer, 1999. <a href=\"https://doi.org/10.1023/A:1008739929481\">https://doi.org/10.1023/A:1008739929481</a>.","ista":"Alur R, Henzinger TA. 1999. Reactive modules. Formal Methods in System Design. 15(1), 7–48.","mla":"Alur, Rajeev, and Thomas A. Henzinger. “Reactive Modules.” <i>Formal Methods in System Design</i>, vol. 15, no. 1, Springer, 1999, pp. 7–48, doi:<a href=\"https://doi.org/10.1023/A:1008739929481\">10.1023/A:1008739929481</a>.","short":"R. Alur, T.A. Henzinger, Formal Methods in System Design 15 (1999) 7–48.","ieee":"R. Alur and T. A. Henzinger, “Reactive modules,” <i>Formal Methods in System Design</i>, vol. 15, no. 1. Springer, pp. 7–48, 1999.","ama":"Alur R, Henzinger TA. Reactive modules. <i>Formal Methods in System Design</i>. 1999;15(1):7-48. doi:<a href=\"https://doi.org/10.1023/A:1008739929481\">10.1023/A:1008739929481</a>","apa":"Alur, R., &#38; Henzinger, T. A. (1999). Reactive modules. <i>Formal Methods in System Design</i>. Springer. <a href=\"https://doi.org/10.1023/A:1008739929481\">https://doi.org/10.1023/A:1008739929481</a>"},"date_created":"2018-12-11T12:09:35Z","publist_id":"125","acknowledgement":"We thank Albert Benveniste, Bob Kurshan, Ken McMillan, Amir Pnueli, and the VIS group at UC Berkeley for fruitful discussions. We also thank the anonymous referees for suggesting improvements. Alur was supported in part by the DARPA/NASA grant NAG2-1214 and Henzinger was supported in part by the ONR YIP award N00014-95-1-0520, the\r\nNSF CAREER award CCR-9501708, the NSF grant CCR-9504469, the DARPA/NASA grant NAG2-1214, and by the SRC contract 97-DC-324.041.","year":"1999","page":"7 - 48","extern":"1","volume":15,"quality_controlled":"1","publisher":"Springer","date_published":"1999-01-01T00:00:00Z","publication_status":"published","abstract":[{"text":"We present a formal model for concurrent systems. The model represents synchronous and asynchronous components in a uniform framework that supports compositional (assume-guarantee) and hierarchical (stepwise-refinement) design and verification. While synchronous models are based on a notion of atomic computation step, and asynchronous models remove that notion by introducing stuttering, our model is based on a flexible notion of what constitutes a computation step: by applying an abstraction operator to a system, arbitrarily many consecutive steps can be collapsed into a single step. The abstraction operator, which may turn an asynchronous system into a synchronous one, allows us to describe systems at various levels of temporal detail. For describing systems at various levels of spatial detail, we use a hiding operator that may turn a synchronous system into an asynchronous one. We illustrate the model with diverse examples from synchronous circuits, asynchronous shared-memory programs, and synchronous message-passing protocols.\r\n","lang":"eng"}],"language":[{"iso":"eng"}],"publication":"Formal Methods in System Design","title":"Reactive modules","date_updated":"2022-09-02T08:45:58Z","article_processing_charge":"No","issue":"1","intvolume":"        15","scopus_import":"1","type":"journal_article","status":"public","author":[{"full_name":"Alur, Rajeev","first_name":"Rajeev","last_name":"Alur"},{"full_name":"Henzinger, Thomas A","first_name":"Thomas A","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","last_name":"Henzinger","orcid":"0000−0002−2985−7724"}],"day":"01","oa_version":"None","user_id":"ea97e931-d5af-11eb-85d4-e6957dddbf17","month":"01","publication_identifier":{"issn":["0925-9856"]}},{"type":"conference","status":"public","alternative_title":["LNCS"],"author":[{"first_name":"Rajeev","full_name":"Alur, Rajeev","last_name":"Alur"},{"orcid":"0000−0002−2985−7724","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","last_name":"Henzinger","full_name":"Henzinger, Thomas A","first_name":"Thomas A"},{"last_name":"Kupferman","full_name":"Kupferman, Orna","first_name":"Orna"}],"user_id":"ea97e931-d5af-11eb-85d4-e6957dddbf17","oa_version":"None","day":"01","month":"01","publication_identifier":{"isbn":["9783540654933"]},"conference":{"end_date":"1997-09-12","location":"Bad Malente, Germany","start_date":"1997-09-08","name":"COMPOS: Compositionality"},"language":[{"iso":"eng"}],"publication":"Proceedings of the International Symposium on Compositionality","title":"Alternating-time temporal logic","article_processing_charge":"No","date_updated":"2022-09-01T14:23:41Z","intvolume":"      1536","scopus_import":"1","quality_controlled":"1","volume":1536,"page":"23 - 60","extern":"1","date_published":"1999-01-01T00:00:00Z","publisher":"Springer","publication_status":"published","abstract":[{"text":"Temporal logic comes in two varieties: linear-time temporal logic assumes implicit universal quantification over all paths that are generated by system moves; branching-time temporal logic allows explicit existential and universal quantification over all paths. We introduce a third, more general variety of temporal logic: alternating-time temporal logic offers selective quantification over those paths that are possible outcomes of games, such as the game in which the system and the environment alternate moves. While linear-time and branching-time logics are natural specification languages for closed systems, alternating-time logics are natural specification languages for open systems. For example, by preceding the temporal operator “eventually” with a selective path quantifier, we can specify that in the game between the system and the environment, the system has a strategy to reach a certain state. Also the problems of receptiveness, realizability, and controllability can be formulated as model-checking problems for alternating-time formulas.\r\nDepending on whether we admit arbitrary nesting of selective path quantifiers and temporal operators, we obtain the two alternating-time temporal logics ATL and ATL. We interpret the formulas of ATL and ATL over alternating transition systems. While in ordinary transition systems, each transition corresponds to a possible step of the system, in alternating transition systems, each transition corresponds to a possible move in the game between the system and the environment. Fair alternating transition systems can capture both synchronous and asynchronous compositions of open systems. For synchronous systems, the expressive power of ATL beyond CTL comes at no cost: the model-checking complexity of synchronous ATL is linear in the size of the system and the length of the formula. The symbolic model-checking algorithm for CTL extends with few modifications to synchronous ATL, and with some work, also to asynchronous ATL, whose model-checking complexity is quadratic. This makes ATL an obvious candidate for the automatic verification of open systems. In the case of ATL, the model-checking problem is closely related to the synthesis problem for linear-time formulas, and requires doubly exponential time for both synchronous and asynchronous systems.\r\nA preliminary version of this paper appeared in the Proceedings of the 38th IEEE Symposium on Foundations of Computer Science (FOCS 1997), pp. 100–109.","lang":"eng"}],"_id":"4601","doi":"10.1007/3-540-49213-5_2","publist_id":"106","citation":{"ista":"Alur R, Henzinger TA, Kupferman O. 1999. Alternating-time temporal logic. Proceedings of the International Symposium on Compositionality. COMPOS: Compositionality, LNCS, vol. 1536, 23–60.","mla":"Alur, Rajeev, et al. “Alternating-Time Temporal Logic.” <i>Proceedings of the International Symposium on Compositionality</i>, vol. 1536, Springer, 1999, pp. 23–60, doi:<a href=\"https://doi.org/10.1007/3-540-49213-5_2\">10.1007/3-540-49213-5_2</a>.","chicago":"Alur, Rajeev, Thomas A Henzinger, and Orna Kupferman. “Alternating-Time Temporal Logic.” In <i>Proceedings of the International Symposium on Compositionality</i>, 1536:23–60. Springer, 1999. <a href=\"https://doi.org/10.1007/3-540-49213-5_2\">https://doi.org/10.1007/3-540-49213-5_2</a>.","short":"R. Alur, T.A. Henzinger, O. Kupferman, in:, Proceedings of the International Symposium on Compositionality, Springer, 1999, pp. 23–60.","ieee":"R. Alur, T. A. Henzinger, and O. Kupferman, “Alternating-time temporal logic,” in <i>Proceedings of the International Symposium on Compositionality</i>, Bad Malente, Germany, 1999, vol. 1536, pp. 23–60.","ama":"Alur R, Henzinger TA, Kupferman O. Alternating-time temporal logic. In: <i>Proceedings of the International Symposium on Compositionality</i>. Vol 1536. Springer; 1999:23-60. doi:<a href=\"https://doi.org/10.1007/3-540-49213-5_2\">10.1007/3-540-49213-5_2</a>","apa":"Alur, R., Henzinger, T. A., &#38; Kupferman, O. (1999). Alternating-time temporal logic. In <i>Proceedings of the International Symposium on Compositionality</i> (Vol. 1536, pp. 23–60). Bad Malente, Germany: Springer. <a href=\"https://doi.org/10.1007/3-540-49213-5_2\">https://doi.org/10.1007/3-540-49213-5_2</a>"},"date_created":"2018-12-11T12:09:41Z","year":"1999","acknowledgement":"This work was supported in part by the ONR YIP award N00014-95-1-0520, by the NSF CAREER award CCR-9501708, by the NSF grant CCR-9504469, by the AFOSR contract F49620-93-1-0056, by the ARO MURI grant DAAH-04-96-1-0341, by the ARPA grant NAG2-892, and by the SRC contract 97-DC-324.041."},{"date_published":"1999-01-01T00:00:00Z","publisher":"Schloss Dagstuhl - Leibniz-Zentrum für Informatik","quality_controlled":"1","volume":1664,"page":"82 - 97","extern":"1","abstract":[{"lang":"eng","text":"Modular techniques for automatic verification attempt to overcome the state-explosion problem by exploiting the modular structure naturally present in many system designs. Unlike other tasks in the verification of finite-state systems, current modular techniques rely heavily on user guidance. In particular, the user is typically required to construct module abstractions that are neither too detailed as to render insufficient benefits in state exploration, nor too coarse as to invalidate the desired systemproperties. In this paper, we construct abstractmodules automatically, using reachability and controllability information about the concrete modules. This allows us to leverage automatic verification techniques by applying them in layers: first we compute on the state spaces of system components, then we use the results for constructing abstractions, and finally we compute on the abstract state space of the system. Our experimental results indicate that if reachability and controllability information is used in the construction of abstractions, the resulting abstract modules are often significantly smaller than the concrete modules and can drastically reduce the space and time requirements for verification."}],"publication_status":"published","doi":"10.1007/3-540-48320-9_8","_id":"4602","year":"1999","acknowledgement":"This research was supported in part by the NSF CAREER award CCR-9734115, by the NSF CAREER award CCR-9501708, by the DARPA (NASA Ames) grant NAG2-1214, by the DARPA (Wright-Patterson AFB) grant F33615-98-C-3614, by the ARO MURI grant DAAH- 04-96-1-0341, and by the Gigascale Silicon Research Center.","citation":{"apa":"Alur, R., De Alfaro, L., Henzinger, T. A., &#38; Mang, F. (1999). Automating modular verification. In <i>Proceedings of the 10th International Conference on Concurrency Theory</i> (Vol. 1664, pp. 82–97). Eindhoven, The Netherlands: Schloss Dagstuhl - Leibniz-Zentrum für Informatik. <a href=\"https://doi.org/10.1007/3-540-48320-9_8\">https://doi.org/10.1007/3-540-48320-9_8</a>","mla":"Alur, Rajeev, et al. “Automating Modular Verification.” <i>Proceedings of the 10th International Conference on Concurrency Theory</i>, vol. 1664, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 1999, pp. 82–97, doi:<a href=\"https://doi.org/10.1007/3-540-48320-9_8\">10.1007/3-540-48320-9_8</a>.","ista":"Alur R, De Alfaro L, Henzinger TA, Mang F. 1999. Automating modular verification. Proceedings of the 10th International Conference on Concurrency Theory. CONCUR: Concurrency Theory, LNCS, vol. 1664, 82–97.","chicago":"Alur, Rajeev, Luca De Alfaro, Thomas A Henzinger, and Freddy Mang. “Automating Modular Verification.” In <i>Proceedings of the 10th International Conference on Concurrency Theory</i>, 1664:82–97. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 1999. <a href=\"https://doi.org/10.1007/3-540-48320-9_8\">https://doi.org/10.1007/3-540-48320-9_8</a>.","ieee":"R. Alur, L. De Alfaro, T. A. Henzinger, and F. Mang, “Automating modular verification,” in <i>Proceedings of the 10th International Conference on Concurrency Theory</i>, Eindhoven, The Netherlands, 1999, vol. 1664, pp. 82–97.","ama":"Alur R, De Alfaro L, Henzinger TA, Mang F. Automating modular verification. In: <i>Proceedings of the 10th International Conference on Concurrency Theory</i>. Vol 1664. Schloss Dagstuhl - Leibniz-Zentrum für Informatik; 1999:82-97. doi:<a href=\"https://doi.org/10.1007/3-540-48320-9_8\">10.1007/3-540-48320-9_8</a>","short":"R. Alur, L. De Alfaro, T.A. Henzinger, F. Mang, in:, Proceedings of the 10th International Conference on Concurrency Theory, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 1999, pp. 82–97."},"publist_id":"105","date_created":"2018-12-11T12:09:42Z","status":"public","type":"conference","alternative_title":["LNCS"],"publication_identifier":{"isbn":["9783540664253"]},"month":"01","conference":{"name":"CONCUR: Concurrency Theory","start_date":"1999-08-24","location":"Eindhoven, The Netherlands","end_date":"1999-08-27"},"user_id":"ea97e931-d5af-11eb-85d4-e6957dddbf17","oa_version":"None","day":"01","author":[{"full_name":"Alur, Rajeev","first_name":"Rajeev","last_name":"Alur"},{"last_name":"De Alfaro","full_name":"De Alfaro, Luca","first_name":"Luca"},{"first_name":"Thomas A","full_name":"Henzinger, Thomas A","orcid":"0000−0002−2985−7724","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","last_name":"Henzinger"},{"first_name":"Freddy","full_name":"Mang, Freddy","last_name":"Mang"}],"publication":"Proceedings of the 10th International Conference on Concurrency Theory","language":[{"iso":"eng"}],"scopus_import":"1","intvolume":"      1664","article_processing_charge":"No","date_updated":"2022-09-01T14:15:35Z","title":"Automating modular verification"},{"title":"The chloroplast Ndh complex mediates the dark reduction of the plastoquinone pool in response to heat stress in tobacco leaves","date_updated":"2022-09-01T13:12:15Z","article_processing_charge":"No","issue":"1","intvolume":"       429","language":[{"iso":"eng"}],"publication":"FEBS Letters","author":[{"first_name":"Leonid A","full_name":"Sazanov, Leonid A","last_name":"Sazanov","id":"338D39FE-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-0977-7989"},{"first_name":"Paul","full_name":"Burrows, Paul","last_name":"Burrows"},{"last_name":"Nixon","full_name":"Nixon, Peter","first_name":"Peter"}],"day":"05","oa_version":"None","user_id":"ea97e931-d5af-11eb-85d4-e6957dddbf17","month":"06","publication_identifier":{"issn":["0014-5793"]},"pmid":1,"type":"journal_article","status":"public","citation":{"ista":"Sazanov LA, Burrows P, Nixon P. 1998. The chloroplast Ndh complex mediates the dark reduction of the plastoquinone pool in response to heat stress in tobacco leaves. FEBS Letters. 429(1), 115–118.","mla":"Sazanov, Leonid A., et al. “The Chloroplast Ndh Complex Mediates the Dark Reduction of the Plastoquinone Pool in Response to Heat Stress in Tobacco Leaves.” <i>FEBS Letters</i>, vol. 429, no. 1, Elsevier, 1998, pp. 115–18, doi:<a href=\"https://doi.org/10.1016/S0014-5793(98)00573-0\">10.1016/S0014-5793(98)00573-0</a>.","chicago":"Sazanov, Leonid A, Paul Burrows, and Peter Nixon. “The Chloroplast Ndh Complex Mediates the Dark Reduction of the Plastoquinone Pool in Response to Heat Stress in Tobacco Leaves.” <i>FEBS Letters</i>. Elsevier, 1998. <a href=\"https://doi.org/10.1016/S0014-5793(98)00573-0\">https://doi.org/10.1016/S0014-5793(98)00573-0</a>.","ieee":"L. A. Sazanov, P. Burrows, and P. Nixon, “The chloroplast Ndh complex mediates the dark reduction of the plastoquinone pool in response to heat stress in tobacco leaves,” <i>FEBS Letters</i>, vol. 429, no. 1. Elsevier, pp. 115–118, 1998.","ama":"Sazanov LA, Burrows P, Nixon P. The chloroplast Ndh complex mediates the dark reduction of the plastoquinone pool in response to heat stress in tobacco leaves. <i>FEBS Letters</i>. 1998;429(1):115-118. doi:<a href=\"https://doi.org/10.1016/S0014-5793(98)00573-0\">10.1016/S0014-5793(98)00573-0</a>","short":"L.A. Sazanov, P. Burrows, P. Nixon, FEBS Letters 429 (1998) 115–118.","apa":"Sazanov, L. A., Burrows, P., &#38; Nixon, P. (1998). The chloroplast Ndh complex mediates the dark reduction of the plastoquinone pool in response to heat stress in tobacco leaves. <i>FEBS Letters</i>. Elsevier. <a href=\"https://doi.org/10.1016/S0014-5793(98)00573-0\">https://doi.org/10.1016/S0014-5793(98)00573-0</a>"},"date_created":"2018-12-11T11:54:54Z","publist_id":"5128","acknowledgement":"This work was funded by the BBSRC. We would like to thank Professor Peter Horton (University of Sheffield) for the loan of the ED 800 T unit.","year":"1998","_id":"1954","article_type":"original","doi":"10.1016/S0014-5793(98)00573-0","publication_status":"published","external_id":{"pmid":["9657394 "]},"abstract":[{"lang":"eng","text":"\r\nWe have examined the effects of heat stress on electron transfer in the thylakoid membrane of an engineered plastid ndh deletion mutant, Δ1, incapable of performing the Ndh-mediated reduction of the plastoquinone pool in the chloroplast. Upon heat stress in the dark, the rate of PSII- independent reduction of PSI after subsequent illumination by far-red light is dramatically enhanced in both Δ1 and a wild-type control plant (WT). In contrast, in the dark, only the WT shows an increase in the reduction state of the plastoquinone pool. We conclude that the heat stress-induced reduction of the intersystem electron transport chain can be mediated by Ndh- independent pathways in the light but that in the dark the dominant pathway for reduction of the plastoquinone pool is catalysed by the Ndh complex. Our results therefore demonstrate a functional role for the Ndh complex in the dark.\r\n"}],"page":"115 - 118","extern":"1","volume":429,"quality_controlled":"1","publisher":"Elsevier","date_published":"1998-06-05T00:00:00Z"},{"publication_status":"published","abstract":[{"text":"The plastid genomes of several plants contain homologues, termed ndh genes, of genes encoding subunits of the NADH:ubiquinone oxidoreductase or complex I of mitochondria and eubacteria. The functional significance of the Ndh proteins in higher plants is uncertain. We show here that tobacco chloroplasts contain a protein complex of 550 kDa consisting of at least three of the ndh gene products: NdhI, NdhJ and NdhK. We have constructed mutant tobacco plants with disrupted ndhC, ndhK and ndhJ plastid genes, indicating that the Ndh complex is dispensible for plant growth under optimal growth conditions. Chlorophyll fluorescence analysis shows that in vivo the Ndh complex catalyses the post-illumination reduction of the plastoquinone pool and in the light optimizes the induction of photosynthesis under conditions of water stress. We conclude that the Ndh complex catalyses the reduction of the plastoquinone pool using stromal reductant and so acts as a respiratory complex. Overall, our data are compatible with the participation of the Ndh complex in cyclic electron flow around the photosystem I complex in the light and possibly in a chloroplast respiratory chain in the dark.","lang":"eng"}],"external_id":{"pmid":["9463365"]},"quality_controlled":"1","volume":17,"page":"868 - 876","extern":"1","date_published":"1998-02-04T00:00:00Z","publisher":"Wiley-Blackwell","citation":{"chicago":"Burrows, Paul, Leonid A Sazanov, Zóra Sváb, Pàl Maliga, and Peter Nixon. “Identification of a Functional Respiratory Complex in Chloroplasts through Analysis of Tobacco Mutants Containing Disrupted Plastid Ndh Genes.” <i>EMBO Journal</i>. Wiley-Blackwell, 1998. <a href=\"https://doi.org/10.1093/emboj/17.4.868\">https://doi.org/10.1093/emboj/17.4.868</a>.","mla":"Burrows, Paul, et al. “Identification of a Functional Respiratory Complex in Chloroplasts through Analysis of Tobacco Mutants Containing Disrupted Plastid Ndh Genes.” <i>EMBO Journal</i>, vol. 17, no. 4, Wiley-Blackwell, 1998, pp. 868–76, doi:<a href=\"https://doi.org/10.1093/emboj/17.4.868\">10.1093/emboj/17.4.868</a>.","ista":"Burrows P, Sazanov LA, Sváb Z, Maliga P, Nixon P. 1998. Identification of a functional respiratory complex in chloroplasts through analysis of tobacco mutants containing disrupted plastid ndh genes. EMBO Journal. 17(4), 868–876.","ama":"Burrows P, Sazanov LA, Sváb Z, Maliga P, Nixon P. Identification of a functional respiratory complex in chloroplasts through analysis of tobacco mutants containing disrupted plastid ndh genes. <i>EMBO Journal</i>. 1998;17(4):868-876. doi:<a href=\"https://doi.org/10.1093/emboj/17.4.868\">10.1093/emboj/17.4.868</a>","ieee":"P. Burrows, L. A. Sazanov, Z. Sváb, P. Maliga, and P. Nixon, “Identification of a functional respiratory complex in chloroplasts through analysis of tobacco mutants containing disrupted plastid ndh genes,” <i>EMBO Journal</i>, vol. 17, no. 4. Wiley-Blackwell, pp. 868–876, 1998.","short":"P. Burrows, L.A. Sazanov, Z. Sváb, P. Maliga, P. Nixon, EMBO Journal 17 (1998) 868–876.","apa":"Burrows, P., Sazanov, L. A., Sváb, Z., Maliga, P., &#38; Nixon, P. (1998). Identification of a functional respiratory complex in chloroplasts through analysis of tobacco mutants containing disrupted plastid ndh genes. <i>EMBO Journal</i>. Wiley-Blackwell. <a href=\"https://doi.org/10.1093/emboj/17.4.868\">https://doi.org/10.1093/emboj/17.4.868</a>"},"date_created":"2018-12-11T11:54:54Z","publist_id":"5129","year":"1998","acknowledgement":"We thank Professor Süss (Institute of Plant Genetics and Crop Plant Research, Gatersleben, Germany) for the gift of the anti-FNR antiserum, Professor Masahiro Sugiura (Nagoya University, Japan) for the gift of plasmid pTB19 and Professor Peter Horton (University of Sheffield) for the loan of his ED-800T unit. P.B. is a recipient of a BBSRC studentship and the work was supported by grants from the BBSRC, The Royal Society (to P.J.N.) and The National Science Foundation (to P.M.).","_id":"1955","article_type":"original","doi":"10.1093/emboj/17.4.868","author":[{"first_name":"Paul","full_name":"Burrows, Paul","last_name":"Burrows"},{"full_name":"Sazanov, Leonid A","first_name":"Leonid A","orcid":"0000-0002-0977-7989","last_name":"Sazanov","id":"338D39FE-F248-11E8-B48F-1D18A9856A87"},{"first_name":"Zóra","full_name":"Sváb, Zóra","last_name":"Sváb"},{"first_name":"Pàl","full_name":"Maliga, Pàl","last_name":"Maliga"},{"first_name":"Peter","full_name":"Nixon, Peter","last_name":"Nixon"}],"user_id":"ea97e931-d5af-11eb-85d4-e6957dddbf17","day":"04","main_file_link":[{"url":"http://www.ncbi.nlm.nih.gov/pmc/articles/PMC1170436/","open_access":"1"}],"oa_version":"None","publication_identifier":{"issn":["0261-4189"]},"month":"02","status":"public","type":"journal_article","pmid":1,"title":"Identification of a functional respiratory complex in chloroplasts through analysis of tobacco mutants containing disrupted plastid ndh genes","issue":"4","article_processing_charge":"No","date_updated":"2022-09-01T13:17:49Z","oa":1,"intvolume":"        17","scopus_import":"1","language":[{"iso":"eng"}],"publication":"EMBO Journal"},{"main_file_link":[{"url":"https://europepmc.org/article/pmc/18756","open_access":"1"}],"day":"03","oa_version":"None","user_id":"ea97e931-d5af-11eb-85d4-e6957dddbf17","month":"02","publication_identifier":{"issn":["0027-8424"]},"author":[{"last_name":"Sazanov","id":"338D39FE-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-0977-7989","full_name":"Sazanov, Leonid A","first_name":"Leonid A"},{"full_name":"Burrows, Paul","first_name":"Paul","last_name":"Burrows"},{"first_name":"Peter","full_name":"Nixon, Peter","last_name":"Nixon"}],"pmid":1,"status":"public","type":"journal_article","scopus_import":"1","intvolume":"        95","title":"The plastid ndh genes code for an NADH-specific dehydrogenase: Isolation of a complex I analogue from pea thylakoid membranes","oa":1,"date_updated":"2022-09-01T13:47:05Z","issue":"3","article_processing_charge":"No","publication":"PNAS","language":[{"iso":"eng"}],"external_id":{"pmid":["9448329 "]},"abstract":[{"lang":"eng","text":"\r\nThe plastid genomes of several plants contain ndh genes-homologues of genes encoding subunits of the proton-pumping NADH:ubiquinone oxidoreductase, or complex I, involved in respiration in mitochondria and eubacteria. From sequence similarities with these genes, the ndh gene products have been suggested to form a large protein complex (Ndh complex); however, the structure and function of this complex remains to be established. Herein we report the isolation of the Ndh complex from the chloroplasts of the higher plant Pisum sativum. The purification procedure involved selective solubilization of the thylakoid membrane with dodecyl maltoside, followed by two anion-exchange chromatography steps and one size-exclusion chromatography step. The isolated Ndh complex has an apparent total molecular mass of approximately 550 kDa and according to SDS/PAGE consists of at least 16 subunits including NdhA, NdhI, NdhJ, NdhK, and NdhH, which were identified by N-terminal sequencing and immunoblotting. The Ndh complex showed an NADH- and deamino-NADH-specific dehydrogenase activity, characteristic of complex I, when either ferricyanide or the quinones menadione and duroquinone were used as electron acceptors. This study describes the isolation of the chloroplast analogue of the respiratory complex I and provides direct evidence for the function of the plastid Ndh complex as an NADH:plastoquinone oxidoreductase. Our results are compatible with a dual role for the Ndh complex in the chloro-respiratory and cyclic photophosphorylation pathways."}],"publication_status":"published","extern":"1","page":"1319 - 1324","quality_controlled":"1","volume":95,"publisher":"National Academy of Sciences","date_published":"1998-02-03T00:00:00Z","publist_id":"5130","citation":{"apa":"Sazanov, L. A., Burrows, P., &#38; Nixon, P. (1998). The plastid ndh genes code for an NADH-specific dehydrogenase: Isolation of a complex I analogue from pea thylakoid membranes. <i>PNAS</i>. National Academy of Sciences. <a href=\"https://doi.org/10.1073/pnas.95.3.1319\">https://doi.org/10.1073/pnas.95.3.1319</a>","ista":"Sazanov LA, Burrows P, Nixon P. 1998. The plastid ndh genes code for an NADH-specific dehydrogenase: Isolation of a complex I analogue from pea thylakoid membranes. PNAS. 95(3), 1319–1324.","chicago":"Sazanov, Leonid A, Paul Burrows, and Peter Nixon. “The Plastid Ndh Genes Code for an NADH-Specific Dehydrogenase: Isolation of a Complex I Analogue from Pea Thylakoid Membranes.” <i>PNAS</i>. National Academy of Sciences, 1998. <a href=\"https://doi.org/10.1073/pnas.95.3.1319\">https://doi.org/10.1073/pnas.95.3.1319</a>.","mla":"Sazanov, Leonid A., et al. “The Plastid Ndh Genes Code for an NADH-Specific Dehydrogenase: Isolation of a Complex I Analogue from Pea Thylakoid Membranes.” <i>PNAS</i>, vol. 95, no. 3, National Academy of Sciences, 1998, pp. 1319–24, doi:<a href=\"https://doi.org/10.1073/pnas.95.3.1319\">10.1073/pnas.95.3.1319</a>.","ieee":"L. A. Sazanov, P. Burrows, and P. Nixon, “The plastid ndh genes code for an NADH-specific dehydrogenase: Isolation of a complex I analogue from pea thylakoid membranes,” <i>PNAS</i>, vol. 95, no. 3. National Academy of Sciences, pp. 1319–1324, 1998.","ama":"Sazanov LA, Burrows P, Nixon P. The plastid ndh genes code for an NADH-specific dehydrogenase: Isolation of a complex I analogue from pea thylakoid membranes. <i>PNAS</i>. 1998;95(3):1319-1324. doi:<a href=\"https://doi.org/10.1073/pnas.95.3.1319\">10.1073/pnas.95.3.1319</a>","short":"L.A. Sazanov, P. Burrows, P. Nixon, PNAS 95 (1998) 1319–1324."},"date_created":"2018-12-11T11:54:54Z","acknowledgement":"We gratefully acknowledge Dr. A.Carne (Institute of Cancer Research, London, U.K.) for help with N-terminal sequencing. We thank Prof. C. J. Leaver (University of Oxford, U.K.), Prof. K.-H. Süss (Institute of Plant Genetics and Crop Plant Research, Gatersleben, Germany), and Prof. L. J. Rogers (University of Aberystwyth, U.K.) for gifts of antiserum against maize mitochondrial cytochrome oxidase subunit 1 and cytochrome bc1 complex, spinach FNR, and spinach ferredoxin, respectively. This work was supported by grants from The Royal Society and the Biotechnology and Biological Sciences Research Council.","year":"1998","doi":"10.1073/pnas.95.3.1319","article_type":"original","_id":"1956"},{"year":"1998","publist_id":"5746","date_created":"2018-12-11T11:52:05Z","citation":{"apa":"Hausel, T. (1998). Compactification of moduli of Higgs bundles. <i>Journal Fur Die Reine Und Angewandte Mathematik</i>. Walter de Gruyter. <a href=\"https://doi.org/10.1515/crll.1998.096\">https://doi.org/10.1515/crll.1998.096</a>","mla":"Hausel, Tamás. “Compactification of Moduli of Higgs Bundles.” <i>Journal Fur Die Reine Und Angewandte Mathematik</i>, vol. 1998, no. 503, Walter de Gruyter, 1998, pp. 169–92, doi:<a href=\"https://doi.org/10.1515/crll.1998.096\">10.1515/crll.1998.096</a>.","ista":"Hausel T. 1998. Compactification of moduli of Higgs bundles. Journal fur die Reine und Angewandte Mathematik. 1998(503), 169–192.","chicago":"Hausel, Tamás. “Compactification of Moduli of Higgs Bundles.” <i>Journal Fur Die Reine Und Angewandte Mathematik</i>. Walter de Gruyter, 1998. <a href=\"https://doi.org/10.1515/crll.1998.096\">https://doi.org/10.1515/crll.1998.096</a>.","short":"T. Hausel, Journal Fur Die Reine Und Angewandte Mathematik 1998 (1998) 169–192.","ieee":"T. Hausel, “Compactification of moduli of Higgs bundles,” <i>Journal fur die Reine und Angewandte Mathematik</i>, vol. 1998, no. 503. Walter de Gruyter, pp. 169–192, 1998.","ama":"Hausel T. Compactification of moduli of Higgs bundles. <i>Journal fur die Reine und Angewandte Mathematik</i>. 1998;1998(503):169-192. doi:<a href=\"https://doi.org/10.1515/crll.1998.096\">10.1515/crll.1998.096</a>"},"article_type":"original","_id":"1449","doi":"10.1515/crll.1998.096","publication_status":"published","external_id":{"arxiv":["math/9804083"]},"abstract":[{"text":"In this paper we consider a canonical compactification of M, the moduli space of stable Higgs bundles with fixed determinant of odd degree over a Riemann surface Σ, producing a projective variety M̄ = M ∪ Z. We give a detailed study of the spaces M̄, Z and M. In doing so we reprove some assertions of Laumon and Thaddeus on the nilpotent cone.","lang":"eng"}],"publisher":"Walter de Gruyter","date_published":"1998-10-01T00:00:00Z","extern":"1","page":"169 - 192","volume":1998,"quality_controlled":"1","date_updated":"2022-09-01T13:51:07Z","oa":1,"issue":"503","article_processing_charge":"No","title":"Compactification of moduli of Higgs bundles","intvolume":"      1998","scopus_import":"1","language":[{"iso":"eng"}],"publication":"Journal fur die Reine und Angewandte Mathematik","author":[{"id":"4A0666D8-F248-11E8-B48F-1D18A9856A87","last_name":"Hausel","first_name":"Tamas","full_name":"Hausel, Tamas"}],"arxiv":1,"publication_identifier":{"issn":["1435-5345"]},"month":"10","main_file_link":[{"url":"http://arxiv.org/abs/math/9804083","open_access":"1"}],"oa_version":"Preprint","day":"01","user_id":"ea97e931-d5af-11eb-85d4-e6957dddbf17","status":"public","type":"journal_article"},{"publisher":"International Press","date_published":"1998-09-01T00:00:00Z","page":"1011 - 1040","extern":"1","quality_controlled":"1","volume":2,"publication_status":"published","external_id":{"arxiv":["math/9805071"]},"abstract":[{"text":"In this paper we consider the topological side of a problem which is the analogue of Sen's S-duality testing conjecture for Hitchin's moduli space M of rank 2 stable Higgs bundles of fixed determinant of odd degree over a Riemann surface ∑. We prove that all intersection numbers in the compactly supported cohomology of M vanish, i.e. &quot;there are no topological L2 harmonic forms on M&quot;. This result generalizes the well known vanishing of the Euler characteristic of the moduli space of rank 2 stable bundles N of fixed determinant of odd degree over ∑. Our proof shows that the vanishing of all intersection numbers of H* cpt(M) is given by relations analogous to the Mumford relations in the cohomology ring of N.","lang":"eng"}],"article_type":"original","_id":"1450","doi":"10.4310/ATMP.1998.v2.n5.a3","acknowledgement":"First of all I would like to thank my supervisor Nigel Hitchin for suggesting Problem 1, and for his help and \r\n encouragement. I am grateful to Michael Thaddeus for his inspiring paper [Thai], enlightening communications and his constant interest in my work. I am also indebted to Manfred Lehn for the idea of the proof of Theorem 6.2. I have found\r\nconversations with Michael Atiyah, Frances Kirwan and Graeme Segal very stimulating. I thank the Mathematical Institute and St. Catherine's College, Oxford for their hospitality during the preparation of this work. Finally I thank Trinity College, Cambridge for financial support.","year":"1998","citation":{"apa":"Hausel, T. (1998). Vanishing of intersection numbers on the moduli space of Higgs bundles. <i>Advances in Theoretical and Mathematical Physics</i>. International Press. <a href=\"https://doi.org/10.4310/ATMP.1998.v2.n5.a3\">https://doi.org/10.4310/ATMP.1998.v2.n5.a3</a>","ama":"Hausel T. Vanishing of intersection numbers on the moduli space of Higgs bundles. <i>Advances in Theoretical and Mathematical Physics</i>. 1998;2(5):1011-1040. doi:<a href=\"https://doi.org/10.4310/ATMP.1998.v2.n5.a3\">10.4310/ATMP.1998.v2.n5.a3</a>","ieee":"T. Hausel, “Vanishing of intersection numbers on the moduli space of Higgs bundles,” <i>Advances in Theoretical and Mathematical Physics</i>, vol. 2, no. 5. International Press, pp. 1011–1040, 1998.","short":"T. Hausel, Advances in Theoretical and Mathematical Physics 2 (1998) 1011–1040.","mla":"Hausel, Tamás. “Vanishing of Intersection Numbers on the Moduli Space of Higgs Bundles.” <i>Advances in Theoretical and Mathematical Physics</i>, vol. 2, no. 5, International Press, 1998, pp. 1011–40, doi:<a href=\"https://doi.org/10.4310/ATMP.1998.v2.n5.a3\">10.4310/ATMP.1998.v2.n5.a3</a>.","chicago":"Hausel, Tamás. “Vanishing of Intersection Numbers on the Moduli Space of Higgs Bundles.” <i>Advances in Theoretical and Mathematical Physics</i>. International Press, 1998. <a href=\"https://doi.org/10.4310/ATMP.1998.v2.n5.a3\">https://doi.org/10.4310/ATMP.1998.v2.n5.a3</a>.","ista":"Hausel T. 1998. Vanishing of intersection numbers on the moduli space of Higgs bundles. Advances in Theoretical and Mathematical Physics. 2(5), 1011–1040."},"publist_id":"5747","date_created":"2018-12-11T11:52:06Z","status":"public","type":"journal_article","author":[{"id":"4A0666D8-F248-11E8-B48F-1D18A9856A87","last_name":"Hausel","first_name":"Tamas","full_name":"Hausel, Tamas"}],"arxiv":1,"month":"09","publication_identifier":{"issn":["1095-0761"]},"day":"01","main_file_link":[{"open_access":"1","url":"http://arxiv.org/abs/math/9805071"}],"oa_version":"Preprint","user_id":"ea97e931-d5af-11eb-85d4-e6957dddbf17","language":[{"iso":"eng"}],"publication":"Advances in Theoretical and Mathematical Physics","oa":1,"date_updated":"2022-09-01T14:09:49Z","issue":"5","article_processing_charge":"No","title":"Vanishing of intersection numbers on the moduli space of Higgs bundles","intvolume":"         2","scopus_import":"1"},{"publication":"Cell","doi":"10.1016/s0092-8674(00)81609-8","_id":"6160","language":[{"iso":"eng"}],"intvolume":"        94","date_updated":"2021-01-12T08:06:28Z","issue":"5","year":"1998","date_created":"2019-03-21T10:32:06Z","title":"Natural variation in a neuropeptide Y receptor homolog modifies social behavior and food response in C. elegans","citation":{"apa":"de Bono, M., &#38; Bargmann, C. I. (1998). Natural variation in a neuropeptide Y receptor homolog modifies social behavior and food response in C. elegans. <i>Cell</i>. Elsevier. <a href=\"https://doi.org/10.1016/s0092-8674(00)81609-8\">https://doi.org/10.1016/s0092-8674(00)81609-8</a>","ista":"de Bono M, Bargmann CI. 1998. Natural variation in a neuropeptide Y receptor homolog modifies social behavior and food response in C. elegans. Cell. 94(5), 679–689.","mla":"de Bono, Mario, and Cornelia I. Bargmann. “Natural Variation in a Neuropeptide Y Receptor Homolog Modifies Social Behavior and Food Response in C. Elegans.” <i>Cell</i>, vol. 94, no. 5, Elsevier, 1998, pp. 679–89, doi:<a href=\"https://doi.org/10.1016/s0092-8674(00)81609-8\">10.1016/s0092-8674(00)81609-8</a>.","chicago":"Bono, Mario de, and Cornelia I Bargmann. “Natural Variation in a Neuropeptide Y Receptor Homolog Modifies Social Behavior and Food Response in C. Elegans.” <i>Cell</i>. Elsevier, 1998. <a href=\"https://doi.org/10.1016/s0092-8674(00)81609-8\">https://doi.org/10.1016/s0092-8674(00)81609-8</a>.","ama":"de Bono M, Bargmann CI. Natural variation in a neuropeptide Y receptor homolog modifies social behavior and food response in C. elegans. <i>Cell</i>. 1998;94(5):679-689. doi:<a href=\"https://doi.org/10.1016/s0092-8674(00)81609-8\">10.1016/s0092-8674(00)81609-8</a>","ieee":"M. de Bono and C. I. Bargmann, “Natural variation in a neuropeptide Y receptor homolog modifies social behavior and food response in C. elegans,” <i>Cell</i>, vol. 94, no. 5. Elsevier, pp. 679–689, 1998.","short":"M. de Bono, C.I. Bargmann, Cell 94 (1998) 679–689."},"publisher":"Elsevier","pmid":1,"status":"public","type":"journal_article","date_published":"1998-09-04T00:00:00Z","page":"679-689","extern":"1","volume":94,"quality_controlled":"1","publication_identifier":{"issn":["0092-8674"]},"month":"09","oa_version":"None","external_id":{"pmid":["9741632"]},"day":"04","user_id":"3E5EF7F0-F248-11E8-B48F-1D18A9856A87","abstract":[{"text":"Natural isolates of C. elegans exhibit either solitary or social feeding behavior. Solitary foragers move slowly on a bacterial lawn and disperse across it, while social foragers move rapidly on bacteria and aggregate together. A loss-of-function mutation in the npr-1 gene, which encodes a predicted G protein–coupled receptor similar to neuropeptide Y receptors, causes a solitary strain to take on social behavior. Two isoforms of NPR-1 that differ at a single residue occur in the wild. One isoform, NPR-1 215F, is found exclusively in social strains, while the other isoform, NPR-1 215V, is found exclusively in solitary strains. An NPR-1 215V transgene can induce solitary feeding behavior in a wild social strain. Thus, isoforms of a putative neuropeptide receptor generate natural variation in C. elegans feeding behavior.","lang":"eng"}],"publication_status":"published","author":[{"full_name":"de Bono, Mario","first_name":"Mario","last_name":"de Bono","id":"4E3FF80E-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0001-8347-0443"},{"last_name":"Bargmann","first_name":"Cornelia I","full_name":"Bargmann, Cornelia I"}]},{"publication_status":"published","abstract":[{"lang":"eng","text":"We present a model for edge updates with restricted randomness in dynamic graph algorithms and a general technique for analyzing the expected running time of an update operation. This model is able to capture the average case in many applications, since (1) it allows restrictions on the set of edges which can be used for insertions and (2) the type (insertion or deletion) of each update operation is arbitrary, i.e., not random. We use our technique to analyze existing and new dynamic algorithms for the following problems: maximum cardinality matching, minimum spanning forest, connectivity, 2-edge connectivity, k -edge connectivity, k -vertex connectivity, and bipartiteness. Given a random graph G with m 0 edges and n vertices and a sequence of l update operations such that the graph contains m i edges after operation i , the expected time for performing the updates for any l is O(llogn+∑li=1n/m−−√i) in the case of minimum spanning forests, connectivity, 2-edge connectivity, and bipartiteness. The expected time per update operation is O(n) in the case of maximum matching. We also give improved bounds for k -edge and k -vertex connectivity. Additionally we give an insertions-only algorithm for maximum cardinality matching with worst-case O(n) amortized time per insertion."}],"publisher":"Springer Nature","date_published":"1998-01-01T00:00:00Z","page":"31-60","extern":"1","volume":20,"quality_controlled":"1","acknowledgement":"The authors would like to thank Emo Welzl for helpful discussions.","year":"1998","date_created":"2022-07-28T06:50:51Z","citation":{"apa":"Alberts, D., &#38; Henzinger, M. H. (1998). Average-case analysis of dynamic graph algorithms. <i>Algorithmica</i>. Springer Nature. <a href=\"https://doi.org/10.1007/pl00009186\">https://doi.org/10.1007/pl00009186</a>","ista":"Alberts D, Henzinger MH. 1998. Average-case analysis of dynamic graph algorithms. Algorithmica. 20, 31–60.","mla":"Alberts, D., and Monika H. Henzinger. “Average-Case Analysis of Dynamic Graph Algorithms.” <i>Algorithmica</i>, vol. 20, Springer Nature, 1998, pp. 31–60, doi:<a href=\"https://doi.org/10.1007/pl00009186\">10.1007/pl00009186</a>.","chicago":"Alberts, D., and Monika H Henzinger. “Average-Case Analysis of Dynamic Graph Algorithms.” <i>Algorithmica</i>. Springer Nature, 1998. <a href=\"https://doi.org/10.1007/pl00009186\">https://doi.org/10.1007/pl00009186</a>.","short":"D. Alberts, M.H. Henzinger, Algorithmica 20 (1998) 31–60.","ieee":"D. Alberts and M. H. Henzinger, “Average-case analysis of dynamic graph algorithms,” <i>Algorithmica</i>, vol. 20. Springer Nature, pp. 31–60, 1998.","ama":"Alberts D, Henzinger MH. Average-case analysis of dynamic graph algorithms. <i>Algorithmica</i>. 1998;20:31-60. doi:<a href=\"https://doi.org/10.1007/pl00009186\">10.1007/pl00009186</a>"},"keyword":["Dynamic graph algorithm","Average-case analysis","Minimum spanning forest","Connectivity","Bipartiteness","Maximum matching."],"related_material":{"record":[{"status":"public","id":"11928","relation":"earlier_version"}]},"article_type":"original","_id":"11680","doi":"10.1007/pl00009186","author":[{"last_name":"Alberts","full_name":"Alberts, D.","first_name":"D."},{"orcid":"0000-0002-5008-6530","id":"540c9bbd-f2de-11ec-812d-d04a5be85630","last_name":"Henzinger","full_name":"Henzinger, Monika H","first_name":"Monika H"}],"publication_identifier":{"issn":["0178-4617"],"eissn":["1432-0541"]},"month":"01","oa_version":"None","day":"01","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","type":"journal_article","status":"public","date_updated":"2023-02-21T16:33:27Z","article_processing_charge":"No","title":"Average-case analysis of dynamic graph algorithms","intvolume":"        20","scopus_import":"1","language":[{"iso":"eng"}],"publication":"Algorithmica"},{"year":"1998","acknowledgement":".","keyword":["Dynamic planarity testing","Dynamic connectivity testing","Lower bounds","Cell probe model"],"date_created":"2022-07-28T06:58:36Z","citation":{"ieee":"M. H. Henzinger and M. L. Fredman, “Lower bounds for fully dynamic connectivity problems in graphs,” <i>Algorithmica</i>, vol. 22, no. 3. Springer Nature, pp. 351–362, 1998.","ama":"Henzinger MH, Fredman ML. Lower bounds for fully dynamic connectivity problems in graphs. <i>Algorithmica</i>. 1998;22(3):351-362. doi:<a href=\"https://doi.org/10.1007/pl00009228\">10.1007/pl00009228</a>","short":"M.H. Henzinger, M.L. Fredman, Algorithmica 22 (1998) 351–362.","chicago":"Henzinger, Monika H, and M. L. Fredman. “Lower Bounds for Fully Dynamic Connectivity Problems in Graphs.” <i>Algorithmica</i>. Springer Nature, 1998. <a href=\"https://doi.org/10.1007/pl00009228\">https://doi.org/10.1007/pl00009228</a>.","ista":"Henzinger MH, Fredman ML. 1998. Lower bounds for fully dynamic connectivity problems in graphs. Algorithmica. 22(3), 351–362.","mla":"Henzinger, Monika H., and M. L. Fredman. “Lower Bounds for Fully Dynamic Connectivity Problems in Graphs.” <i>Algorithmica</i>, vol. 22, no. 3, Springer Nature, 1998, pp. 351–62, doi:<a href=\"https://doi.org/10.1007/pl00009228\">10.1007/pl00009228</a>.","apa":"Henzinger, M. H., &#38; Fredman, M. L. (1998). Lower bounds for fully dynamic connectivity problems in graphs. <i>Algorithmica</i>. Springer Nature. <a href=\"https://doi.org/10.1007/pl00009228\">https://doi.org/10.1007/pl00009228</a>"},"doi":"10.1007/pl00009228","article_type":"original","_id":"11681","abstract":[{"text":"We prove lower bounds on the complexity of maintaining fully dynamic k -edge or k -vertex connectivity in plane graphs and in (k-1) -vertex connected graphs. We show an amortized lower bound of Ω (log n / {k (log log n} + log b)) per edge insertion, deletion, or query operation in the cell probe model, where b is the word size of the machine and n is the number of vertices in G . We also show an amortized lower bound of Ω (log n /(log log n + log b)) per operation for fully dynamic planarity testing in embedded graphs. These are the first lower bounds for fully dynamic connectivity problems.","lang":"eng"}],"publication_status":"published","date_published":"1998-11-01T00:00:00Z","publisher":"Springer Nature","quality_controlled":"1","volume":22,"page":"351-362","extern":"1","intvolume":"        22","scopus_import":"1","article_processing_charge":"No","issue":"3","date_updated":"2022-09-12T09:03:36Z","title":"Lower bounds for fully dynamic connectivity problems in graphs","publication":"Algorithmica","language":[{"iso":"eng"}],"month":"11","publication_identifier":{"issn":["0178-4617"],"eissn":["1432-0541"]},"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","day":"01","oa_version":"None","author":[{"orcid":"0000-0002-5008-6530","last_name":"Henzinger","id":"540c9bbd-f2de-11ec-812d-d04a5be85630","first_name":"Monika H","full_name":"Henzinger, Monika H"},{"last_name":"Fredman","full_name":"Fredman, M. L.","first_name":"M. L."}],"status":"public","type":"journal_article"},{"_id":"11682","language":[{"iso":"eng"}],"doi":"10.1109/SFCS.1998.743510","publication":"Proceedings of the 39th Annual Symposium on Foundations of Computer Science","citation":{"ista":"Agarwal PK, EppsteinL. J. Guibas D, Henzinger MH. 1998. Parametric and kinetic minimum spanning trees. Proceedings of the 39th Annual Symposium on Foundations of Computer Science. Annual IEEE Symposium on Foundations of Computer Science, 596–605.","chicago":"Agarwal, P. K., D. EppsteinL. J. Guibas, and Monika H Henzinger. “Parametric and Kinetic Minimum Spanning Trees.” In <i>Proceedings of the 39th Annual Symposium on Foundations of Computer Science</i>, 596–605, 1998. <a href=\"https://doi.org/10.1109/SFCS.1998.743510\">https://doi.org/10.1109/SFCS.1998.743510</a>.","mla":"Agarwal, P. K., et al. “Parametric and Kinetic Minimum Spanning Trees.” <i>Proceedings of the 39th Annual Symposium on Foundations of Computer Science</i>, 1998, pp. 596–605, doi:<a href=\"https://doi.org/10.1109/SFCS.1998.743510\">10.1109/SFCS.1998.743510</a>.","short":"P.K. Agarwal, D. EppsteinL. J. Guibas, M.H. Henzinger, in:, Proceedings of the 39th Annual Symposium on Foundations of Computer Science, 1998, pp. 596–605.","ieee":"P. K. Agarwal, D. EppsteinL. J. Guibas, and M. H. Henzinger, “Parametric and kinetic minimum spanning trees,” in <i>Proceedings of the 39th Annual Symposium on Foundations of Computer Science</i>, Palo Alto, CA, United States, 1998, pp. 596–605.","ama":"Agarwal PK, EppsteinL. J. Guibas D, Henzinger MH. Parametric and kinetic minimum spanning trees. In: <i>Proceedings of the 39th Annual Symposium on Foundations of Computer Science</i>. ; 1998:596-605. doi:<a href=\"https://doi.org/10.1109/SFCS.1998.743510\">10.1109/SFCS.1998.743510</a>","apa":"Agarwal, P. K., EppsteinL. J. Guibas, D., &#38; Henzinger, M. H. (1998). Parametric and kinetic minimum spanning trees. In <i>Proceedings of the 39th Annual Symposium on Foundations of Computer Science</i> (pp. 596–605). Palo Alto, CA, United States. <a href=\"https://doi.org/10.1109/SFCS.1998.743510\">https://doi.org/10.1109/SFCS.1998.743510</a>"},"date_created":"2022-07-28T07:21:34Z","title":"Parametric and kinetic minimum spanning trees","year":"1998","article_processing_charge":"No","date_updated":"2023-02-09T11:28:52Z","scopus_import":"1","quality_controlled":"1","extern":"1","page":"596-605","date_published":"1998-09-01T00:00:00Z","type":"conference","status":"public","publication_status":"published","author":[{"last_name":"Agarwal","full_name":"Agarwal, P. K.","first_name":"P. K."},{"first_name":"D.","full_name":"EppsteinL. J. Guibas, D.","last_name":"EppsteinL. J. Guibas"},{"first_name":"Monika H","full_name":"Henzinger, Monika H","id":"540c9bbd-f2de-11ec-812d-d04a5be85630","last_name":"Henzinger","orcid":"0000-0002-5008-6530"}],"abstract":[{"lang":"eng","text":"We consider the parametric minimum spanning tree problem, in which we are given a graph with edge weights that are linear functions of a parameter /spl lambda/ and wish to compute the sequence of minimum spanning trees generated as /spl lambda/ varies. We also consider the kinetic minimum spanning tree problem, in which /spl lambda/ represents time and the graph is subject in addition to changes such as edge insertions, deletions, and modifications of the weight functions as time progresses. We solve both problems in time O(n/sup 2/3/log/sup 4/3/) per combinatorial change in the tree (or randomized O(n/sup 2/3/log/sup 4/3/ n) per change). Our time bounds reduce to O(n/sup 1/2/log/sup 3/2/ n) per change (O(n/sup 1/2/log n) randomized) for planar graphs or other minor-closed families of graphs, and O(n/sup 1/4/log/sup 3/2/ n) per change (O(n/sup 1/4/ log n) randomized) for planar graphs with weight changes but no insertions or deletions."}],"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","oa_version":"None","day":"01","month":"09","publication_identifier":{"issn":["0272-5428"],"isbn":["0-8186-9172-7"]},"conference":{"location":"Palo Alto, CA, United States","end_date":"1998-11-11","name":"Annual IEEE Symposium on Foundations of Computer Science","start_date":"1998-11-08"}}]