@article{11762, abstract = {In this paper, we describe six algorithmic problems that arise in web search engines and that are not or only partially solved: (1) Uniformly sampling of web pages; (2) modeling the web graph; (3) finding duplicate hosts; (4) finding top gainers and losers in data streams; (5) finding large dense bipartite graphs; and (6) understanding how eigenvectors partition the web.}, author = {Henzinger, Monika H}, issn = {1944-9488}, journal = {Internet Mathematics}, number = {1}, pages = {115--123}, publisher = {Internet Mathematics}, title = {{Algorithmic challenges in web search engines}}, doi = {10.1080/15427951.2004.10129079}, volume = {1}, year = {2004}, } @inproceedings{11800, abstract = {Web search engines have emerged as one of the central applications on the Internet. In fact, search has become one of the most important activities that people engage in on the the Internet. Even beyond becoming the number one source of information, a growing number of businesses are depending on web search engines for customer acquisition. The first generation of web search engines used text-only retrieval techniques. Google revolutionized the field by deploying the PageRank technology – an eigenvector-based analysis of the hyperlink structure – to analyze the web in order to produce relevant results. Moving forward, our goal is to achieve a better understanding of a page with a view towards producing even more relevant results.}, author = {Henzinger, Monika H}, booktitle = {31st International Colloquium on Automata, Languages and Programming}, issn = {1611-3349}, location = {Turku, Finland}, pages = {3}, publisher = {Springer Nature}, title = {{The past, present, and future of web search engines}}, doi = {10.1007/978-3-540-27836-8_2}, volume = {3142}, year = {2004}, } @inproceedings{11801, abstract = {Web search engines have emerged as one of the central applications on the internet. In fact, search has become one of the most important activities that people engage in on the Internet. Even beyond becoming the number one source of information, a growing number of businesses are depending on web search engines for customer acquisition. In this talk I will brief review the history of web search engines: The first generation of web search engines used text-only retrieval techniques. Google revolutionized the field by deploying the PageRank technology – an eigenvector-based analysis of the hyperlink structure- to analyze the web in order to produce relevant results. Moving forward, our goal is to achieve a better understanding of a page with a view towards producing even more relevant results. Google is powered by a large number of PCs. Using this infrastructure and striving to be as efficient as possible poses challenging systems problems but also various algorithmic challenges. I will discuss some of them in my talk.}, author = {Henzinger, Monika H}, booktitle = {2th Annual European Symposium on Algorithms}, isbn = { 3540230254}, issn = {1611-3349}, location = {Bergen, Norway}, pages = {3}, publisher = {Springer Nature}, title = {{Algorithmic aspects of web search engines}}, doi = {10.1007/978-3-540-30140-0_2}, volume = {3221}, year = {2004}, } @inproceedings{11859, abstract = {In this article we describe the approach taken by the first web search engines, discuss the state of the art, and present some of the challenges for the future.}, author = {Henzinger, Monika H}, booktitle = {SPIE Proceedings}, issn = {0277-786X}, location = {San Jose, CA, United States}, pages = {23 -- 26}, publisher = {Society of Photo-Optical Instrumentation Engineers}, title = {{The past, present, and future of web information retrieval}}, doi = {10.1117/12.537534}, volume = {5296}, year = {2004}, } @article{11877, abstract = {The World Wide Web provides a unprecedented opportunity to automatically analyze a large sample of interests and activity in the world. We discuss methods for extracting knowledge from the web by randomly sampling and analyzing hosts and pages, and by analyzing the link structure of the web and how links accumulate over time. A variety of interesting and valuable information can be extracted, such as the distribution of web pages over domains, the distribution of interest in different areas, communities related to different topics, the nature of competition in different categories of sites, and the degree of communication between different communities or countries.}, author = {Henzinger, Monika H and Lawrence, Steve}, issn = {1091-6490}, journal = {Proceedings of the National Academy of Sciences}, number = {suppl_1}, pages = {5186--5191}, publisher = {Proceedings of the National Academy of Sciences}, title = {{Extracting knowledge from the World Wide Web}}, doi = {10.1073/pnas.0307528100}, volume = {101}, year = {2004}, } @misc{2461, author = {Sauer, Michael and Friml, Jirí}, booktitle = {Development}, number = {23}, pages = {5774 -- 5775}, publisher = {Company of Biologists}, title = {{The Matryoshka dolls of plant polarity}}, doi = {10.1242/dev.01463}, volume = {131}, year = {2004}, } @misc{2636, author = {Momiyama, Akiko and Ryuichi Shigemoto}, booktitle = {Tanpakushitsu kakusan koso Protein nucleic acid enzyme}, number = {3 Suppl}, pages = {287 -- 294}, publisher = {Kyoritsu Shuppan}, title = {{Function and distribution of glutamate receptors in the central synapses}}, volume = {49}, year = {2004}, } @article{12203, abstract = {Geranylgeranyl diphosphate synthase (GGPPS, EC: 2.5.1.29) catalyzes the biosynthesis of geranylgeranyl diphosphate (GGPP), which is a key precursor for ginkgolide biosynthesis. Here we reported for the first time the cloning of a new full-length cDNA encoding GGPPS from the living fossil plant Ginkgo biloba. The full-length cDNA encoding G. biloba GGPPS (designated as GbGGPPS) was 1657bp long and contained a 1176bp open reading frame encoding a 391 amino acid protein. Comparative analysis showed that GbGGPPS possessed a 79 amino acid transit peptide at its N-terminal, which directed GbGGPPS to target to the plastids. Bioinformatic analysis revealed that GbGGPPS was a member of polyprenyltransferases with two highly conserved aspartate-rich motifs like other plant GGPPSs. Phylogenetic tree analysis indicated that plant GGPPSs could be classified into two groups, angiosperm and gymnosperm GGPPSs, while GbGGPPS had closer relationship with gymnosperm plant GGPPSs.}, author = {Liao, Zhihua and Chen, Min and Gong, Yifu and Guo, Liang and Tan, Qiumin and Feng, Xiaoqi and Sun, Xiaofen and Tan, Feng and Tang, Kexuan}, issn = {1042-5179}, journal = {DNA Sequence}, keywords = {Endocrinology, Genetics, Molecular Biology, Biochemistry}, number = {2}, pages = {153--158}, publisher = {Informa UK Limited}, title = {{A new geranylgeranyl Diphosphate synthase gene from Ginkgo biloba, which intermediates the biosynthesis of the key precursor for ginkgolides}}, doi = {10.1080/10425170410001667348}, volume = {15}, year = {2004}, } @article{12658, abstract = {[1] During the ablation period 2001 a glaciometeorological experiment was carried out on Haut Glacier d'Arolla, Switzerland. Five meteorological stations were installed on the glacier, and one permanent automatic weather station in the glacier foreland. The altitudes of the stations ranged between 2500 and 3000 m a.s.l., and they were in operation from end of May to beginning of September 2001. The spatial arrangement of the stations and temporal duration of the measurements generated a unique data set enabling the analysis of the spatial and temporal variability of the meteorological variables across an alpine glacier. All measurements were taken at a nominal height of 2 m, and hourly averages were derived for the analysis. The wind regime was dominated by the glacier wind (mean value 2.8 m s−1) but due to erosion by the synoptic gradient wind, occasionally the wind would blow up the valley. A slight decrease in mean 2 m air temperatures with altitude was found, however the 2 m air temperature gradient varied greatly and frequently changed its sign. Mean relative humidity was 71% and exhibited limited spatial variation. Mean incoming shortwave radiation and albedo both generally increased with elevation. The different components of shortwave radiation are quantified with a parameterization scheme. Resulting spatial variations are mainly due to horizon obstruction and reflections from surrounding slopes, i.e., topography. The effect of clouds accounts for a loss of 30% of the extraterrestrial flux. Albedos derived from a Landsat TM image of 30 July show remarkably constant values, in the range 0.49 to 0.50, across snow covered parts of the glacier, while albedo is highly spatially variable below the zone of continuous snow cover. These results are verified with ground measurements and compared with parameterized albedo. Mean longwave radiative fluxes decreased with elevation due to lower air temperatures and the effect of upper hemisphere slopes. It is shown through parameterization that this effect would even be more pronounced without the effect of clouds. Results are discussed with respect to a similar study which has been carried out on Pasterze Glacier (Austria). The presented algorithms for interpolating, parameterizing and simulating variables and parameters in alpine regions are integrated in the software package AMUNDSEN which is freely available to be adapted and further developed by the community.}, author = {Strasser, Ulrich and Corripio, Javier and Pellicciotti, Francesca and Burlando, Paolo and Brock, Ben and Funk, Martin}, issn = {0148-0227}, journal = {Journal of Geophysical Research: Atmospheres}, keywords = {Paleontology, Space and Planetary Science, Earth and Planetary Sciences (miscellaneous), Atmospheric Science, Earth-Surface Processes, Geochemistry and Petrology, Soil Science, Water Science and Technology, Ecology, Aquatic Science, Forestry, Oceanography, Geophysics}, number = {D3}, publisher = {American Geophysical Union}, title = {{Spatial and temporal variability of meteorological variables at Haut Glacier d'Arolla (Switzerland) during the ablation season 2001: Measurements and simulations}}, doi = {10.1029/2003jd003973}, volume = {109}, year = {2004}, } @article{13434, abstract = {Thin films of ionically doped gelatin have been color-patterned with submicrometer precision using the wet-stamping technique. Inorganic salts are delivered onto the gelatin surface from an agarose stamp, and diffuse into the gelatine layer, producting deeply colored precipitates. Reaction fronts originating from different features of the stamp cease within < 1 μm of each other, leaving sharp, transparent regions in between.}, author = {Campbell, C. J. and Fialkowski, M. and Klajn, Rafal and Bensemann, I. T. and Grzybowski, B. A.}, issn = {1521-4095}, journal = {Advanced Materials}, keywords = {Mechanical Engineering, Mechanics of Materials, General Materials Science}, number = {21}, pages = {1912--1917}, publisher = {Wiley}, title = {{Color micro- and nanopatterning with counter-propagating reaction-diffusion fronts}}, doi = {10.1002/adma.200400383}, volume = {16}, year = {2004}, } @article{13435, abstract = {Micropatterning of surfaces with several chemicals at different spatial locations usually requires multiple stamping and registration steps. Here, we describe an experimental method based on reaction–diffusion phenomena that allows for simultaneous micropatterning of a substrate with several coloured chemicals. In this method, called wet stamping (WETS), aqueous solutions of two or more inorganic salts are delivered onto a film of dry, ionically doped gelatin from an agarose stamp patterned in bas relief. Once in conformal contact, these salts diffuse into the gelatin, where they react to give deeply coloured precipitates. Separation of colours in the plane of the surface is the consequence of the differences in the diffusion coefficients, the solubility products, and the amounts of different salts delivered from the stamp, and is faithfully reproduced by a theoretical model based on a system of reaction–diffusion partial differential equations. The multicolour micropatterns are useful as non-binary optical elements, and could potentially form the basis of new applications in microseparations and in controlled delivery.}, author = {Klajn, Rafal and Fialkowski, Marcin and Bensemann, Igor T. and Bitner, Agnieszka and Campbell, C. J. and Bishop, Kyle and Smoukov, Stoyan and Grzybowski, Bartosz A.}, issn = {1476-4660}, journal = {Nature Materials}, keywords = {Mechanical Engineering, Mechanics of Materials, Condensed Matter Physics, General Materials Science, General Chemistry}, pages = {729--735}, publisher = {Springer Nature}, title = {{Multicolour micropatterning of thin films of dry gels}}, doi = {10.1038/nmat1231}, volume = {3}, year = {2004}, } @inbook{18739, abstract = {The first massive astrophysical black holes likely formed at high redshifts (z≳ 10) at the centers of low mass (~ 106 M⊙) dark matter concentrations. These black holes grow by mergers and gas accretion, evolve into the population of bright quasars observed at lower redshifts, and eventually leave the supermassive black hole remnants that are ubiquitous at the centers of galaxies in the nearby universe. The astrophysical processes responsible for the formation of the earliest seed black holes are poorly understood. The purpose of this review is threefold: (1) to describe theoretical expectations for the formation and growth of the earliest black holes within the general paradigm of hierarchical cold dark matter cosmologies, (2) to summarize several relevant recent observations that have implications for the formation of the earliest black holes, and (3) to look into the future and assess the power of forthcoming observations to probe the physics of the first active galactic nuclei.}, author = {Haiman, Zoltán and Quataert, Eliot}, booktitle = {Supermassive Black Holes in the Distant Universe}, isbn = {9789048166626}, issn = {0067-0057}, pages = {147--185}, publisher = {Springer Nature}, title = {{The Formation and Evolution of the First Massive Black Holes}}, doi = {10.1007/978-1-4020-2471-9_5}, volume = {308}, year = {2004}, } @article{18742, abstract = {Recent improved determinations of the mass density ρBH of supermassive black holes (SMBHs) in the local universe have allowed accurate comparisons of ρBH with the amount of light received from past quasar activity. These comparisons support the notion that local SMBHs are "dead quasars" and yield a value epsilon ≳ 0.1 for the average radiative efficiency of cosmic SMBH accretion. BH coalescences may represent an important component of the quasar mass assembly and yet not produce any observable electromagnetic signature. Therefore, ignoring gravitational wave (GW) emission during such coalescences, which reduces the amount of mass locked into remnant BHs, results in an overestimate of epsilon. Here we put constraints on the magnitude of this bias. We calculate the cumulative mass loss to GWs experienced by a representative population of BHs during repeated cosmological mergers, using loss prescriptions based on detailed general relativistic calculations. Despite the possibly large number of mergers in the assembly history of each individual SMBH, we find that near-equal mass mergers are rare; therefore, the cumulative loss is likely to be modest, amounting at most to a 20% increase in the inferred epsilon value. Thus, recent estimates of epsilon ≳ 0.1 appear robust. The space interferometer LISA should provide empirical constraints on the dark side of quasar evolution by measuring the masses and rates of coalescence of massive BHs to cosmological distances.}, author = {Menou, Kristen and Haiman, Zoltán}, issn = {1538-4357}, journal = {The Astrophysical Journal}, number = {1}, pages = {130--134}, publisher = {American Astronomical Society}, title = {{On the dark side of quasar evolution}}, doi = {10.1086/423951}, volume = {615}, year = {2004}, } @inproceedings{4372, author = {Maler, Oded and Nickovic, Dejan}, pages = {152 -- 166}, publisher = {Springer}, title = {{Monitoring Temporal Properties of Continuous Signals}}, doi = {10.1007/978-3-540-30206-3_12}, year = {2004}, } @phdthesis{4424, abstract = {The enormous cost and ubiquity of software errors necessitates the need for techniques and tools that can precisely analyze large systems and prove that they meet given specifications, or if they don't, return counterexample behaviors showing how the system fails. Recent advances in model checking, decision procedures, program analysis and type systems, and a shift of focus to partial specifications common to several systems (e.g., memory safety and race freedom) have resulted in several practical verification methods. However, these methods are either precise or they are scalable, depending on whether they track the values of variables or only a fixed small set of dataflow facts (e.g., types), and are usually insufficient for precisely verifying large programs. We describe a new technique called Lazy Abstraction (LA) which achieves both precision and scalability by localizing the use of precise information. LA automatically builds, explores and refines a single abstract model of the program in a way that different parts of the model exhibit different degrees of precision, namely just enough to verify the desired property. The algorithm automatically mines the information required by partitioning mechanical proofs of unsatisfiability of spurious counterexamples into Craig Interpolants. For multithreaded systems, we give a new technique based on analyzing the behavior of a single thread executing in a context which is an abstraction of the other (arbitrarily many) threads. We define novel context models and show how to automatically infer them and analyze the full system (thread + context) using LA. LA is implemented in BLAST. We have run BLAST on Windows and Linux Device Drivers to verify API conformance properties, and have used it to find (or guarantee the absence of) data races in multithreaded Networked Embedded Systems (NESC) applications. BLAST is able to prove the absence of races in several cases where earlier methods, which depend on lock-based synchronization, fail.}, author = {Jhala, Ranjit}, pages = {1 -- 165}, publisher = {University of California, Berkeley}, title = {{Program verification by lazy abstraction}}, year = {2004}, } @inproceedings{4445, abstract = {We present a type system for E code, which is an assembly language that manages the release, interaction, and termination of real-time tasks. E code specifies a deadline for each task, and the type system ensures that the deadlines are path-insensitive. We show that typed E programs allow, for given worst-case execution times of tasks, a simple schedulability analysis. Moreover, the real-time programming language Giotto can be compiled into typed E~code. This shows that typed E~code identifies an easily schedulable yet expressive class of real-time programs. We have extended the Giotto compiler to generate typed E code, and enabled the run-time system for E code to perform a type and schedulability check before executing the code.}, author = {Henzinger, Thomas A and Kirsch, Christoph}, booktitle = {Proceedings of the 4th ACM international conference on Embedded software}, isbn = {9781581138603}, location = {Pisa, Italy}, pages = {104 -- 113}, publisher = {Association for Computing Machinery}, title = {{A typed assembly language for real-time programs}}, doi = {10.1145/1017753.1017774}, year = {2004}, } @inproceedings{4458, abstract = {The success of model checking for large programs depends crucially on the ability to efficiently construct parsimonious abstractions. A predicate abstraction is parsimonious if at each control location, it specifies only relationships between current values of variables, and only those which are required for proving correctness. Previous methods for automatically refining predicate abstractions until sufficient precision is obtained do not systematically construct parsimonious abstractions: predicates usually contain symbolic variables, and are added heuristically and often uniformly to many or all control locations at once. We use Craig interpolation to efficiently construct, from a given abstract error trace which cannot be concretized, a parsominous abstraction that removes the trace. At each location of the trace, we infer the relevant predicates as an interpolant between the two formulas that define the past and the future segment of the trace. Each interpolant is a relationship between current values of program variables, and is relevant only at that particular program location. It can be found by a linear scan of the proof of infeasibility of the trace.We develop our method for programs with arithmetic and pointer expressions, and call-by-value function calls. For function calls, Craig interpolation offers a systematic way of generating relevant predicates that contain only the local variables of the function and the values of the formal parameters when the function was called. We have extended our model checker Blast with predicate discovery by Craig interpolation, and applied it successfully to C programs with more than 130,000 lines of code, which was not possible with approaches that build less parsimonious abstractions.}, author = {Henzinger, Thomas A and Jhala, Ranjit and Majumdar, Ritankar and Mcmillan, Kenneth}, booktitle = {Proceedings of the 31st ACM SIGPLAN-SIGACT symposium on Principles of programming languages}, isbn = {9781581137293}, location = {Venice, Italy}, pages = {232 -- 244}, publisher = {Association for Computing Machinery}, title = {{Abstractions from proofs}}, doi = {10.1145/964001.964021}, year = {2004}, } @inproceedings{4459, abstract = {Software model checking has been successful for sequential programs, where predicate abstraction offers suitable models, and counterexample-guided abstraction refinement permits the automatic inference of models. When checking concurrent programs, we need to abstract threads as well as the contexts in which they execute. Stateless context models, such as predicates on global variables, prove insufficient for showing the absence of race conditions in many examples. We therefore use richer context models, which combine (1) predicates for abstracting data state, (2) control flow quotients for abstracting control state, and (3) counters for abstracting an unbounded number of threads. We infer suitable context models automatically by a combination of counterexample-guided abstraction refinement, bisimulation minimization, circular assume-guarantee reasoning, and parametric reasoning about an unbounded number of threads. This algorithm, called CIRC, has been implemented in BLAST and succeeds in checking many examples of NESC code for data races. In particular, BLAST proves the absence of races in several cases where previous race checkers give false positives.}, author = {Henzinger, Thomas A and Jhala, Ranjit and Majumdar, Ritankar}, booktitle = {Proceedings of the ACM SIGPLAN 2004 conference on Programming language design and implementation}, isbn = {1581138075}, location = {Washington, DC, United States}, pages = {1 -- 13}, publisher = {Association for Computing Machinery}, title = {{Race checking by context inference}}, doi = {10.1145/996841.996844}, year = {2004}, } @inbook{4461, abstract = {One of the central axioms of extreme programming is the disciplined use of regression testing during stepwise software development. Due to recent progress in software model checking, it has become possible to supplement this process with automatic checks for behavioral safety properties of programs, such as conformance with locking idioms and other programming protocols and patterns. For efficiency reasons, all checks must be incremental, i.e., they must reuse partial results from previous checks in order to avoid all unnecessary repetition of expensive verification tasks. We show that the lazy-abstraction algorithm, and its implementation in Blast, can be extended to support the fully automatic and incremental checking of temporal safety properties during software development.}, author = {Henzinger, Thomas A and Jhala, Ranjit and Majumdar, Ritankar and Sanvido, Marco}, booktitle = {Verification: Theory and Practice}, isbn = {9783540210023}, pages = {332 -- 358}, publisher = {Springer Nature}, title = {{Extreme Model Checking}}, doi = {10.1007/978-3-540-39910-0_16}, volume = {2772}, year = {2004}, } @inproceedings{4525, abstract = {We present a new high-level programming language, called xGiotto, for programming applications with hard real-time constraints. Like its predecessor, xGiotto is based on the LET (logical execution time) assumption: the programmer specifies when the outputs of a task become available, and the compiler checks if the specification can be implemented on a given platform. However, while the predecessor language xGiotto was purely time-triggered, xGiotto accommodates also asynchronous events. Indeed, through a mechanism called event scoping, events are the main structuring principle of the new language. The xGiotto compiler and run-time system implement event scoping through a tree-based event filter. The compiler also checks programs for determinism (absence of race conditions).}, author = {Ghosal, Arkadeb and Henzinger, Thomas A and Kirsch, Christoph and Sanvido, Marco}, isbn = {9783540212591}, location = {Philadelphia, PA, United States}, pages = {357--371}, publisher = {Springer Nature}, title = {{Event-driven programming with logical execution times}}, doi = {10.1007/978-3-540-24743-2_24}, year = {2004}, }