@article{3515,
  abstract     = {Oscillations in neuronal networks are assumed to serve various physiological functions, from coordination of motor patterns to perceptual binding of sensory information. Here, we describe an ultra-slow oscillation (0.025 Hz) in the hippocampus. Extracellular and intracellular activity was recorded from the CA1 and subicular regions in rats of the Wistar and Sprague-Dawley strains. anesthetized with urethane. in a subgroup of Wistar rats (23%), spontaneous afterdischarges (4.7 +/- 1.6 s) occurred regularly at 40.8 +/- 15.7 s. The afterdischarge was initiated by a fast increase of population synchrony (100-250 Hz oscillation; “tonic” phase), followed by large-amplitude rhythmic waves and associated action potentials at gamma and beta frequency (15-50 Hz; “clonic” phase). The afterdischarges were bilaterally synchronous and terminated relatively abruptly without post-ictal depression. Single-pulse stimulation of the commissural input could trigger afterdischarges, but only at times when they were about to occur. Commissural stimulation evoked inhibitory postsynaptic potentials in pyramidal cells. However, when the stimulus triggered an afterdischarge, the inhibitory postsynaptic potential was absent and the cells remained depolarized during most of the afterdischarge. Afterdischarges were not observed in the Sprague-Dawley rats. Long-term analysis of interneuronal activity in intact, drug-free rats also revealed periodic excitability changes in the hippocampal network at 0.025 Hz. These findings indicate the presence of an ultra-slow oscillation in the hippocampal formation. The ultra-slow clock induced afterdischarges in susceptible animals. We hypothesize that a transient failure of GABAergic inhibition in a subset of Wistar rats is responsible for the emergence of epileptiform patterns. (C) 1999 IBRO. Published by Elsevier Science Ltd.},
  author       = {Penttonen, Markku and Nurminen, Nina and Miettinen, Riitta and Sirviö, Jouni and Henze, Darrell and Csicsvari, Jozsef L and Buzsáki, György},
  issn         = {0306-4522},
  journal      = {Neuroscience},
  number       = {3},
  pages        = {735 -- 743},
  publisher    = {Elsevier},
  title        = {{Ultra-slow oscillation (0.025 Hz) triggers hippocampal afterdischarges in Wistar rats}},
  doi          = {10.1016/S0306-4522(99)00367-X},
  volume       = {94},
  year         = {1999},
}

@article{3518,
  abstract     = {Information in neuronal networks may be represented by the spatiotemporal patterns of spikes. Here we examined the temporal coordination of pyramidal cell spikes in the rat hippocampus during slow-wave sleep. In addition, rats were trained to run in a defined position in space (running wheel) to activate a selected group of pyramidal cells. A template-matching method and a joint probability map method were used for sequence search. Repeating spike sequences in excess of chance occurrence were examined by comparing the number of repeating sequences in the original spike trains and in surrogate trains after Monte Carlo shuffling of the spikes. Four different shuffling procedures were used to control for the population dynamics of hippocampal neurons. Repeating spike sequences in the recorded cell assemblies were present in both the awake and sleeping animal in excess of what might be predicted by random variations. Spike sequences observed during wheel running were “replayed” at a faster timescale during single sharp-wave bursts of slow-wave sleep. We hypothesize that the endogenously expressed spike sequences during sleep reflect reactivation of the circuitry modified by previous experience. Reactivation of acquired sequences may serve to consolidate information.},
  author       = {Nádasdy, Zoltán and Hirase, Hajima and Czurkó, András and Csicsvari, Jozsef L and Buzsáki, György},
  issn         = {0270-6474},
  journal      = {Journal of Neuroscience},
  number       = {21},
  pages        = {9497 -- 9507},
  publisher    = {Society for Neuroscience},
  title        = {{Replay and time compression of recurring spike sequences in the hippocampus}},
  doi          = {10.1523/JNEUROSCI.19-21-09497.1999},
  volume       = {19},
  year         = {1999},
}

@article{3519,
  abstract     = {In contrast to sensory cortical areas of the brain, the relevant physiological inputs to the hippocampus, leading to selective activation of pyramidal cells, are largely unknown. Pyramidal cells are thought to be phasically activated by spatial cues and a variety of sensory and motor stimuli. Here, we used a behavioural `space clamp' method, which involved the confinement of the actively running animal in a defined position in space (running wheel) and kept sensory inputs constant. Twelve percent of the recorded CA1 pyramidal cells were selectively active while the rat was running in the wheel. Cell firing was specific to the direction of running and disappeared after rotating the recording apparatus. The discharge frequency of pyramidal cells and interneurons was sustained as long as the rat ran continuously in the wheel. Furthermore, the discharge frequency of pyramidal cells and interneurons increased with increasing running velocity, even though the frequency of hippocampal theta waves remained constant. The discharge frequency of some `wheel-related' pyramidal cells could increase more than 10-fold between 10 and 100 cm/s, whereas the firing rate of `non-wheel' cells remained constantly low. We hypothesize that: (i) a necessary condition for place-specific discharge of hippocampal pyramidal cells is the presence of theta oscillation; and (ii) relevant stimuli can tonically and selectively activate hippocampal pyramidal cells as long as theta activity is present.},
  author       = {Czurkó, András and Hirase, Hajima and Csicsvari, Jozsef L and Buzsáki, György},
  issn         = {0953-816X},
  journal      = {European Journal of Neuroscience},
  number       = {1},
  pages        = {344 -- 352},
  publisher    = {Wiley-Blackwell},
  title        = {{Sustained activation of hippocampal pyramidal cells by ‘space clamping' in a running wheel}},
  doi          = {10.1046/j.1460-9568.1999.00446.x},
  volume       = {11},
  year         = {1999},
}

@article{3524,
  abstract     = {We examined whether excitation and inhibition are balanced in hippocampal cortical networks. Extracellular field and single-unit activity were recorded by multiple tetrodes and multisite silicon probes to reveal the timing of the activity of hippocampal CAI pyramidal cells and classes of interneurons during theta waves and sharp wave burst (SPW)-associated field ripples. The somatic and dendritic inhibition of pyramidal cells was deduced from the activity of interneurons in the pyramidal layer [int(p)] and in the alveus and st. oriens [int(a/o)], respectively. int(p) and int(a/o) discharged an average of 60 and 20 degrees before the population discharge of pyramidal cells during the theta cycle, respectively. SPW ripples were associated with a 2.5-fold net increase of excitation. The discharge frequency of int(a/o) increased, decreased (”anti-SPW” cells), or did not change (”SPW-independent” cells) during SPW suggesting that not all interneurons are innervated by pyramidal cells. Int(p) either fired together with (unimodal cells) or both before and after (bimodal cells) the pyramidal cell burst. During fast-ripple oscillation, the activity of interneurons in both the int(p) and int(a/o) groups lagged the maximum discharge probability of pyramidal neurons by 1-2 msec. Network state changes, as reflected by field activity, covaried with changes in the spike train dynamics of single cells and their interactions. Summed activity of parallel-recorded interneurons, but not of pyramidal cells, reliably predicted theta cycles, whereas the reverse was true for the ripple cycles of SPWs. We suggest that network-driven excitability changes provide temporal windows of opportunity for single pyramidal cells to suppress, enable, or facilitate selective synaptic inputs.},
  author       = {Csicsvari, Jozsef L and Hirase, Hajima and Czurkó, András and Mamiya, Akira and Buzsáki, György},
  issn         = {0270-6474},
  journal      = {Journal of Neuroscience},
  number       = {1},
  pages        = {274 -- 287},
  publisher    = {Society for Neuroscience},
  title        = {{Oscillatory coupling of hippocampal pyramidal cells and interneurons in the behaving rat}},
  doi          = {10.1523/JNEUROSCI.19-01-00274.1999},
  volume       = {19},
  year         = {1999},
}

@article{3539,
  abstract     = {In the hippocampus, spatial representation of the environment has been suggested to be coded by either the firing rate of pyramidal cell assemblies or the relative timing of the action potentials during the theta EEG cycle. Here, we used a behavioural `space clamp' method, which involved the confinement of the actively running animal in a defined position in space (running wheel) to examine how `spatial' and other inputs affect firing rate and timing of hippocampal CA1 pyramidal cells and interneurons. Nineteen per cent of the recorded CA1 pyramidal cells were selectively active while the rat was running in the wheel in a given direction ('wheel' cells). Spatial rotation of the apparatus showed that selective discharge of pyramidal cells in the wheel was under the combined influence of distal and apparatus cues. During steady running, both discharge rate and theta phase were constant. Rotation of the wheel apparatus resulted in a shift of both firing rate and preferred theta phase. The discharge frequency of `wheel' cells increased threefold (on average) with increasing running velocity. In contrast, change in running speed had relatively little effect on the theta phase-related discharge of `wheel' cells. Our findings indicate that mechanisms that regulate rate and phase of spikes are overlapping but not necessarily identical.},
  author       = {Hirase, Hajima and Czurkó, András and Csicsvari, Jozsef L and Buzsáki, György},
  issn         = {0953-816X},
  journal      = {European Journal of Neuroscience},
  number       = {12},
  pages        = {4373 -- 4380},
  publisher    = {Wiley-Blackwell},
  title        = {{Firing rate and theta-phase coding by hippocampal pyramidal neurons during ‘space clamping’}},
  doi          = {10.1046/j.1460-9568.1999.00853.x},
  volume       = {11},
  year         = {1999},
}

@inproceedings{3554,
  abstract     = {In computational simulation of coupled, multicomponent systems, it is frequently necessary to transfer data between meshes that may differ in resolution, structure, and discretization methodology. Typically, nodes from one mesh must be associated with elements of another mesh. In this paper, we formulate mesh association as a geometric problem and introduce two efficient mesh association algorithms. One of these algorithms requires linear time in the worst case if the meshes are well shaped and geometrically well aligned. Our formulation of the problem and our algorithms are more general than previous work and can be applied to surface meshes with curved elements.},
  author       = {Jiao, Xiangmin and Edelsbrunner, Herbert and Heath, Michael},
  booktitle    = {Proceedings of the 8th International Meshing Roundtable},
  location     = {South Lake Tahoe, CA, United States of America},
  pages        = {75 -- 82},
  publisher    = {Elsevier},
  title        = {{Mesh association: formulation and algorithms}},
  year         = {1999},
}

@inbook{3571,
  author       = {Dey, Tamal and Edelsbrunner, Herbert and Guha, Sumanta},
  booktitle    = {Advances in Discrete and Computational Geometry},
  isbn         = {9780821878149},
  pages        = {109 -- 143},
  publisher    = {American Mathematical Society},
  title        = {{Computational topology}},
  volume       = {223},
  year         = {1999},
}

@article{3582,
  abstract     = {We study edge contractions in simplicial complexes and local conditions under which they preserve the topological type. The conditions are based on a generalized notion of boundary, which lends itself to defining a nested hierarchy of triangulable spaces measuring the distance to being a manifold.},
  author       = {Dey, Tamal and Edelsbrunner, Herbert and Guha, Sumanta and Nekhayev, Dmitry},
  issn         = {0350-1302},
  journal      = {Publications de l'Institut Mathématique},
  pages        = {23 -- 45},
  publisher    = {Mathematical Institute, Serbian Academy of Sciences and Arts},
  title        = {{Topology preserving edge contraction}},
  volume       = {66},
  year         = {1999},
}

@article{3625,
  abstract     = {This article outlines theoretical models of clines in additive polygenic traits, which are maintained by stabilizing selection towards a spatially varying optimum. Clines in the trait mean can be accurately predicted, given knowledge of the genetic variance. However, predicting the variance is difficult, because it depends on genetic details. Changes in genetic variance arise from changes in allele frequency, and in linkage disequilibria. Allele frequency changes dominate when selection is weak relative to recombination, and when there are a moderate number of loci. With a continuum of alleles, gene flow inflates the genetic variance in the same way as a source of mutations of small effect. The variance can be approximated by assuming a Gaussian distribution of allelic effects; with a sufficiently steep cline, this is accurate even when mutation and selection alone are better described by the 'House of Cards' approximation. With just two alleles at each locus, the phenotype changes in a similar way: the mean remains close to the optimum, while the variance changes more slowly, and over a wider region. However, there may be substantial cryptic divergence at the underlying loci. With strong selection and many loci, linkage disequilibria are the main cause of changes in genetic variance. Even for strong selection, the infinitesimal model can be closely approximated by assuming a Gaussian distribution of breeding values. Linkage disequilibria can generate a substantial increase in genetic variance, which is concentrated at sharp gradients in trait means.},
  author       = {Barton, Nicholas H},
  issn         = {0016-6723},
  journal      = {Genetical Research},
  number       = {3},
  pages        = {223 -- 236},
  publisher    = {Cambridge University Press},
  title        = {{Clines in polygenic traits}},
  doi          = {10.1017/S001667239900422X},
  volume       = {74},
  year         = {1999},
}

@article{3626,
  abstract     = {There has recently been considerable debate over the relative importance of selection against hybrids ("endogenous" selection) vs. adaptation to different environments ("exogenous") in maintaining stable hybrid zones and hence in speciation. Single-locus models of endogenous and exogenous viability selection generate clines of similar shape, but the comparison has not been extended to multilocus systems, which are both quantitatively and qualitatively very different from the single-locus case. Here we develop an analytical multilocus model of differential adaptation across an environmental transition and compare it to previous heterozygote disadvantage models. We show that the shape of clines generated by exogenous selection is indistinguishable from that generated by endogenous selection. A stochastic simulation model is used to test the robustness of the analytical description to the effects of drift and strong selection, and confirms the prediction that pairwise linkage disequilibria are predominantly generated by migration. However, although analytical predictions for the width of clines maintained by heterozygote disadvantage fit well with the simulation results, those for environmental adaptation are consistently too narrow; reasons for the discrepancy are discussed. There is a smooth transition between a system in which a set of loci effectively act independently of each other and one in which they act as a single nonrecombining unit.},
  author       = {Kruuk, Loeske and Baird, Stuart and Gale, Katherine and Barton, Nicholas H},
  issn         = {0016-6731},
  journal      = {Genetics},
  number       = {4},
  pages        = {1959 -- 1971},
  publisher    = {Genetics Society of America},
  title        = {{A comparison of multilocus clines maintained by environmental adaptation or by selection against hybrids}},
  doi          = {10.1093/genetics/153.4.1959},
  volume       = {153},
  year         = {1999},
}

@article{4014,
  abstract     = {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.},
  author       = {Edelsbrunner, Herbert},
  issn         = {0179-5376},
  journal      = {Discrete & Computational Geometry},
  number       = {1},
  pages        = {87 -- 115},
  publisher    = {Springer},
  title        = {{Deformable smooth surface design}},
  doi          = {10.1007/PL00009412},
  volume       = {21},
  year         = {1999},
}

@article{4204,
  abstract     = {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.},
  author       = {Heisenberg, Carl-Philipp J and Brennan, Caroline and Wilson, Stephen},
  issn         = {0950-1991},
  journal      = {Development},
  number       = {10},
  pages        = {2129 -- 2140},
  publisher    = {Company of Biologists},
  title        = {{Zebrafish aussicht mutant embryos exhibit widespread overexpression of ace (fgf8) and coincident defects in CNS development}},
  doi          = {10.1242/dev.126.10.2129},
  volume       = {126},
  year         = {1999},
}

@article{4277,
  abstract     = {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.},
  author       = {Kruuk, Loeske and Gilchrist, Jason and Barton, Nicholas H},
  issn         = {0014-3820},
  journal      = {Evolution; International Journal of Organic Evolution},
  number       = {5},
  pages        = {1611 -- 1616},
  publisher    = {Wiley-Blackwell},
  title        = {{Hybrid dysfunction in fire-bellied toads (Bombina)}},
  doi          = {10.2307/2640907},
  volume       = {53},
  year         = {1999},
}

@article{4279,
  abstract     = {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.},
  author       = {Goodman, Simon and Barton, Nicholas H and Swanson, Graeme and Abernethy, Kate and Pemberton, Josephine},
  issn         = {0016-6731},
  journal      = {Genetics},
  number       = {1},
  pages        = {355 -- 371},
  publisher    = {Genetics Society of America},
  title        = {{Introgression through rare hybridisation: A genetic study of a hybrid zone between red and sika deer (genus Cervus), in Argyll, Scotland}},
  doi          = {10.1093/genetics/152.1.355},
  volume       = {152},
  year         = {1999},
}

@phdthesis{4411,
  abstract     = {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.

One 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.

Heuristics 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 "divide and conquer," 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.

Our 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.},
  author       = {Qadeer, Shaz},
  pages        = {1 -- 150},
  publisher    = {University of California, Berkeley},
  title        = {{Algorithms and Methodology for Scalable Model Checking}},
  year         = {1999},
}

@article{4442,
  abstract     = {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.},
  author       = {Henzinger, Thomas A and Kopke, Peter},
  issn         = {0304-3975},
  journal      = {Theoretical Computer Science},
  number       = {1-2},
  pages        = {369 -- 392},
  publisher    = {Elsevier},
  title        = {{Discrete-time control for rectangular hybrid automata}},
  doi          = {10.1016/S0304-3975(99)00038-9},
  volume       = {221},
  year         = {1999},
}

@inproceedings{4480,
  abstract     = {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.},
  author       = {Henzinger, Thomas A and Liu, Xiaojun and Qadeer, Shaz and Rajamani, Sriram},
  issn         = {1092-3152},
  location     = {San Jose, CA, United States of America},
  pages        = {494 -- 499},
  publisher    = {IEEE},
  title        = {{Formal specification and verification of a dataflow processor array}},
  doi          = {10.1109/ICCAD.1999.810700},
  year         = {1999},
}

@inproceedings{4484,
  abstract     = {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.
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. 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.},
  author       = {Henzinger, Thomas A and Qadeer, Shaz and Rajamani, Sriram},
  booktitle    = {Proceedings of the 11th International Conference on Computer Aided Verification},
  isbn         = {9783540662020},
  location     = {Trento, Italy},
  pages        = {301 -- 315},
  publisher    = {Springer},
  title        = {{Verifying sequential consistency on shared-memory multiprocessor systems}},
  doi          = {10.1007/3-540-48683-6_27},
  volume       = {1633},
  year         = {1999},
}

@inproceedings{4485,
  abstract     = {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.},
  author       = {Henzinger, Thomas A and Horowitz, Benjamin and Majumdar, Ritankar},
  booktitle    = {Proceedings of the 10th International Conference on Concurrency Theory},
  isbn         = {9783540664253},
  location     = {Eindhoven, The Netherlands},
  pages        = {320 -- 335},
  publisher    = {Schloss Dagstuhl - Leibniz-Zentrum für Informatik},
  title        = {{Rectangular hybrid games}},
  doi          = {10.1007/3-540-48320-9_23},
  volume       = {1664},
  year         = {1999},
}

@inproceedings{4487,
  abstract     = {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.},
  author       = {Henzinger, Thomas A and Qadeer, Shaz and Rajamani, Sriram},
  booktitle    = {Proceedings of the 11th International Conference on Computer Aided Verification},
  isbn         = {9783540662020},
  location     = {Trento, Italy},
  pages        = {208 -- 221},
  publisher    = {Springer},
  title        = {{Assume-guarantee refinement between different time scales}},
  doi          = {10.1007/3-540-48683-6_20},
  volume       = {1633},
  year         = {1999},
}