---
_id: '4014'
abstract:
- lang: eng
  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.
article_processing_charge: No
article_type: original
author:
- first_name: Herbert
  full_name: Edelsbrunner, Herbert
  id: 3FB178DA-F248-11E8-B48F-1D18A9856A87
  last_name: Edelsbrunner
  orcid: 0000-0002-9823-6833
citation:
  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>
  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>.
  ieee: H. Edelsbrunner, “Deformable smooth surface design,” <i>Discrete &#38; Computational
    Geometry</i>, vol. 21, no. 1. Springer, pp. 87–115, 1999.
  ista: Edelsbrunner H. 1999. Deformable smooth surface design. Discrete &#38; Computational
    Geometry. 21(1), 87–115.
  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.
date_created: 2018-12-11T12:06:26Z
date_published: 1999-01-01T00:00:00Z
date_updated: 2022-09-06T09:02:23Z
day: '01'
doi: 10.1007/PL00009412
extern: '1'
intvolume: '        21'
issue: '1'
language:
- iso: eng
month: '01'
oa_version: None
page: 87 - 115
publication: Discrete & Computational Geometry
publication_identifier:
  issn:
  - 0179-5376
publication_status: published
publisher: Springer
publist_id: '2115'
quality_controlled: '1'
scopus_import: '1'
status: public
title: Deformable smooth surface design
type: journal_article
user_id: ea97e931-d5af-11eb-85d4-e6957dddbf17
volume: 21
year: '1999'
...
---
_id: '4204'
abstract:
- lang: eng
  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.
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"
article_processing_charge: No
article_type: original
author:
- first_name: Carl-Philipp J
  full_name: Heisenberg, Carl-Philipp J
  id: 39427864-F248-11E8-B48F-1D18A9856A87
  last_name: Heisenberg
  orcid: 0000-0002-0912-4566
- first_name: Caroline
  full_name: Brennan, Caroline
  last_name: Brennan
- first_name: Stephen
  full_name: Wilson, Stephen
  last_name: Wilson
citation:
  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>
  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>
  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>.
  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.
  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.
  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.
date_created: 2018-12-11T12:07:34Z
date_published: 1999-05-15T00:00:00Z
date_updated: 2022-09-06T08:38:01Z
day: '15'
doi: 10.1242/dev.126.10.2129
extern: '1'
external_id:
  pmid:
  - '10207138'
intvolume: '       126'
issue: '10'
language:
- iso: eng
month: '05'
oa_version: None
page: 2129 - 2140
pmid: 1
publication: Development
publication_identifier:
  issn:
  - 0950-1991
publication_status: published
publisher: Company of Biologists
publist_id: '1914'
quality_controlled: '1'
scopus_import: '1'
status: public
title: Zebrafish aussicht mutant embryos exhibit widespread overexpression of ace
  (fgf8) and coincident defects in CNS development
type: journal_article
user_id: ea97e931-d5af-11eb-85d4-e6957dddbf17
volume: 126
year: '1999'
...
---
_id: '4277'
abstract:
- lang: eng
  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.'
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.
article_processing_charge: No
article_type: original
author:
- first_name: Loeske
  full_name: Kruuk, Loeske
  last_name: Kruuk
- first_name: Jason
  full_name: Gilchrist, Jason
  last_name: Gilchrist
- first_name: Nicholas H
  full_name: Barton, Nicholas H
  id: 4880FE40-F248-11E8-B48F-1D18A9856A87
  last_name: Barton
  orcid: 0000-0002-8548-5240
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>
  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>.
  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.
  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.
  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>.
  short: L. Kruuk, J. Gilchrist, N.H. Barton, Evolution; International Journal of
    Organic Evolution 53 (1999) 1611–1616.
date_created: 2018-12-11T12:08:00Z
date_published: 1999-10-01T00:00:00Z
date_updated: 2022-09-06T08:20:03Z
day: '01'
doi: 10.2307/2640907
extern: '1'
external_id:
  pmid:
  - '28565554'
intvolume: '        53'
issue: '5'
language:
- iso: eng
month: '10'
oa_version: None
page: 1611 - 1616
pmid: 1
publication: Evolution; International Journal of Organic Evolution
publication_identifier:
  issn:
  - 0014-3820
publication_status: published
publisher: Wiley-Blackwell
publist_id: '1811'
quality_controlled: '1'
scopus_import: '1'
status: public
title: Hybrid dysfunction in fire-bellied toads (Bombina)
type: journal_article
user_id: ea97e931-d5af-11eb-85d4-e6957dddbf17
volume: 53
year: '1999'
...
---
_id: '4279'
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.
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.
article_processing_charge: No
article_type: original
author:
- first_name: Simon
  full_name: Goodman, Simon
  last_name: Goodman
- first_name: Nicholas H
  full_name: Barton, Nicholas H
  id: 4880FE40-F248-11E8-B48F-1D18A9856A87
  last_name: Barton
  orcid: 0000-0002-8548-5240
- first_name: Graeme
  full_name: Swanson, Graeme
  last_name: Swanson
- first_name: Kate
  full_name: Abernethy, Kate
  last_name: Abernethy
- first_name: Josephine
  full_name: Pemberton, Josephine
  last_name: Pemberton
citation:
  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>'
  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>'
  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>.'
  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.'
  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.
date_created: 2018-12-11T12:08:01Z
date_published: 1999-05-01T00:00:00Z
date_updated: 2022-09-06T08:12:14Z
day: '01'
doi: 10.1093/genetics/152.1.355
extern: '1'
external_id:
  pmid:
  - '10224266'
intvolume: '       152'
issue: '1'
language:
- iso: eng
month: '05'
oa_version: None
page: 355 - 371
pmid: 1
publication: Genetics
publication_identifier:
  issn:
  - 0016-6731
publication_status: published
publisher: Genetics Society of America
publist_id: '1809'
quality_controlled: '1'
scopus_import: '1'
status: public
title: 'Introgression through rare hybridisation: A genetic study of a hybrid zone
  between red and sika deer (genus Cervus), in Argyll, Scotland'
type: journal_article
user_id: ea97e931-d5af-11eb-85d4-e6957dddbf17
volume: 152
year: '1999'
...
---
_id: '4411'
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."
article_processing_charge: No
author:
- first_name: Shaz
  full_name: Qadeer, Shaz
  last_name: Qadeer
citation:
  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.
  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.
  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_created: 2018-12-11T12:08:43Z
date_published: 1999-10-01T00:00:00Z
date_updated: 2022-09-06T08:07:40Z
day: '01'
degree_awarded: PhD
extern: '1'
language:
- iso: eng
main_file_link:
- url: https://www.microsoft.com/en-us/research/publication/algorithms-methodology-scalable-model-checking/
month: '10'
oa_version: None
page: 1 - 150
publication_status: published
publisher: University of California, Berkeley
publist_id: '321'
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
- first_name: Robert
  full_name: Bryton, Robert
  last_name: Bryton
- first_name: John
  full_name: Steel, John
  last_name: Steel
title: Algorithms and Methodology for Scalable Model Checking
type: dissertation
user_id: ea97e931-d5af-11eb-85d4-e6957dddbf17
year: '1999'
...
---
_id: '4442'
abstract:
- lang: eng
  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.
article_processing_charge: No
article_type: original
author:
- first_name: Thomas A
  full_name: Henzinger, Thomas A
  id: 40876CD8-F248-11E8-B48F-1D18A9856A87
  last_name: Henzinger
  orcid: 0000−0002−2985−7724
- first_name: Peter
  full_name: Kopke, Peter
  last_name: Kopke
citation:
  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>
  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.
  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.
date_created: 2018-12-11T12:08:52Z
date_published: 1999-01-01T00:00:00Z
date_updated: 2022-09-06T08:03:48Z
day: '01'
doi: 10.1016/S0304-3975(99)00038-9
extern: '1'
intvolume: '       221'
issue: 1-2
language:
- iso: eng
month: '01'
oa_version: None
page: 369 - 392
publication: Theoretical Computer Science
publication_identifier:
  issn:
  - 0304-3975
publication_status: published
publisher: Elsevier
publist_id: '290'
quality_controlled: '1'
scopus_import: '1'
status: public
title: Discrete-time control for rectangular hybrid automata
type: journal_article
user_id: ea97e931-d5af-11eb-85d4-e6957dddbf17
volume: 221
year: '1999'
...
---
_id: '4480'
abstract:
- lang: eng
  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.'
article_processing_charge: No
author:
- first_name: Thomas A
  full_name: Henzinger, Thomas A
  id: 40876CD8-F248-11E8-B48F-1D18A9856A87
  last_name: Henzinger
  orcid: 0000−0002−2985−7724
- first_name: Xiaojun
  full_name: Liu, Xiaojun
  last_name: Liu
- first_name: Shaz
  full_name: Qadeer, Shaz
  last_name: Qadeer
- first_name: Sriram
  full_name: Rajamani, Sriram
  last_name: Rajamani
citation:
  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>'
  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>'
  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.'
  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.'
  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.
conference:
  end_date: 1999-11-11
  location: San Jose, CA, United States of America
  name: 'ICCAD: Computer-Aided Design'
  start_date: 1999-11-07
date_created: 2018-12-11T12:09:04Z
date_published: 1999-01-01T00:00:00Z
date_updated: 2022-09-05T14:48:48Z
day: '01'
doi: 10.1109/ICCAD.1999.810700
extern: '1'
language:
- iso: eng
month: '01'
oa_version: None
page: 494 - 499
publication_identifier:
  issn:
  - 1092-3152
publication_status: published
publisher: IEEE
publist_id: '246'
quality_controlled: '1'
scopus_import: '1'
status: public
title: Formal specification and verification of a dataflow processor array
type: conference
user_id: ea97e931-d5af-11eb-85d4-e6957dddbf17
year: '1999'
...
---
_id: '4484'
abstract:
- lang: eng
  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."
alternative_title:
- LNCS
article_processing_charge: No
author:
- first_name: Thomas A
  full_name: Henzinger, Thomas A
  id: 40876CD8-F248-11E8-B48F-1D18A9856A87
  last_name: Henzinger
  orcid: 0000−0002−2985−7724
- first_name: Shaz
  full_name: Qadeer, Shaz
  last_name: Qadeer
- first_name: Sriram
  full_name: Rajamani, Sriram
  last_name: Rajamani
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>'
  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>.
  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.
  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>.
  short: T.A. Henzinger, S. Qadeer, S. Rajamani, in:, Proceedings of the 11th International
    Conference on Computer Aided Verification, Springer, 1999, pp. 301–315.
conference:
  end_date: 1999-07-10
  location: Trento, Italy
  name: 'CAV: Computer Aided Verification'
  start_date: 1999-07-06
date_created: 2018-12-11T12:09:05Z
date_published: 1999-01-01T00:00:00Z
date_updated: 2022-09-02T09:21:11Z
day: '01'
doi: 10.1007/3-540-48683-6_27
extern: '1'
intvolume: '      1633'
language:
- iso: eng
month: '01'
oa_version: None
page: 301 - 315
publication: Proceedings of the 11th International Conference on Computer Aided Verification
publication_identifier:
  isbn:
  - '9783540662020'
publication_status: published
publisher: Springer
publist_id: '244'
quality_controlled: '1'
status: public
title: Verifying sequential consistency on shared-memory multiprocessor systems
type: conference
user_id: ea97e931-d5af-11eb-85d4-e6957dddbf17
volume: 1633
year: '1999'
...
---
_id: '4485'
abstract:
- lang: eng
  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.'
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.
alternative_title:
- LNCS
article_processing_charge: No
author:
- first_name: Thomas A
  full_name: Henzinger, Thomas A
  id: 40876CD8-F248-11E8-B48F-1D18A9856A87
  last_name: Henzinger
  orcid: 0000−0002−2985−7724
- first_name: Benjamin
  full_name: Horowitz, Benjamin
  last_name: Horowitz
- first_name: Ritankar
  full_name: Majumdar, Ritankar
  last_name: Majumdar
citation:
  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>'
  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>'
  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.
  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.'
  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.
conference:
  location: Eindhoven, The Netherlands
  name: 'CONCUR: Concurrency Theory'
date_created: 2018-12-11T12:09:05Z
date_published: 1999-01-01T00:00:00Z
date_updated: 2022-09-02T10:54:12Z
day: '01'
doi: 10.1007/3-540-48320-9_23
extern: '1'
intvolume: '      1664'
language:
- iso: eng
month: '01'
oa_version: None
page: 320 - 335
publication: Proceedings of the 10th International Conference on Concurrency Theory
publication_identifier:
  isbn:
  - '9783540664253'
publication_status: published
publisher: Schloss Dagstuhl - Leibniz-Zentrum für Informatik
publist_id: '245'
quality_controlled: '1'
status: public
title: Rectangular hybrid games
type: conference
user_id: ea97e931-d5af-11eb-85d4-e6957dddbf17
volume: 1664
year: '1999'
...
---
_id: '4487'
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.
alternative_title:
- LNCS
article_processing_charge: No
author:
- first_name: Thomas A
  full_name: Henzinger, Thomas A
  id: 40876CD8-F248-11E8-B48F-1D18A9856A87
  last_name: Henzinger
  orcid: 0000−0002−2985−7724
- first_name: Shaz
  full_name: Qadeer, Shaz
  last_name: Qadeer
- first_name: Sriram
  full_name: Rajamani, Sriram
  last_name: Rajamani
citation:
  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>'
  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>'
  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>.
  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.
  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.
conference:
  end_date: 1999-07-10
  location: Trento, Italy
  name: 'CAV: Computer Aided Verification'
  start_date: 1999-07-06
date_created: 2018-12-11T12:09:06Z
date_published: 1999-01-01T00:00:00Z
date_updated: 2022-09-02T09:04:26Z
day: '01'
doi: 10.1007/3-540-48683-6_20
extern: '1'
intvolume: '      1633'
language:
- iso: eng
month: '01'
oa_version: None
page: 208 - 221
publication: Proceedings of the 11th International Conference on Computer Aided Verification
publication_identifier:
  isbn:
  - '9783540662020'
publication_status: published
publisher: Springer
publist_id: '243'
quality_controlled: '1'
status: public
title: Assume-guarantee refinement between different time scales
type: conference
user_id: ea97e931-d5af-11eb-85d4-e6957dddbf17
volume: 1633
year: '1999'
...