The Retail Market for Bednets in Kenya: How Well Is It Working?

Background Achieving the goals set by Roll Back Malaria and the Government of Kenya for use of insecticide treated bednets (ITNs) will require that the private retail market for nets and insecticide treatments grow substantially. This paper applies some basic concepts of market structure and pricing to a set of recently-collected retail price data from Kenya in order to answer the question, “How well are Kenyan retail markets for ITNs working?” Methods Data on the availability and prices of ITNs at a wide range of retail outlets throughout Kenya were collected in January 2002, and vendors and manufacturers were interviewed regarding market structure. Findings Untreated nets are manufactured in Kenya by a number of companies and are widely available in large and medium-sized towns. Availability in smaller villages is limited. There is relatively little geographic price variation, and nets can be found at competitive prices in towns and cities. Marketing margins on prices appear to be within normal ranges. No finished nets are imported. Few pre-treated nets or net+treatment combinations are available, with the exception of the subsidized Supanet/Power Tab combination marketed by a donor-funded social marketing project. Conclusions Retail markets for untreated nets in Kenya are well established and appear to be competitive. Markets for treated nets and insecticide treatment kits are not well established. The role of subsidized ITN marketing projects should be monitored to ensure that these projects support, rather than hinder, the development of retail markets.

Verification with Natural Contexts: Soundness of Safe Compositional Network Sketches

In research areas involving mathematical rigor, there are numerous benefits to adopting a formal representation of models and arguments: reusability, automatic evaluation of examples, and verification of consistency and correctness. However, accessibility has not been a priority in the design of formal verification tools that can provide these benefits. In earlier work [30] we attempt to address this broad problem by proposing several specific design criteria organized around the notion of a natural context: the sphere of awareness a working human user maintains of the relevant constructs, arguments, experiences, and background materials necessary to accomplish the task at hand. In this report we evaluate our proposed design criteria by utilizing within the context of novel research a formal reasoning system that is designed according to these criteria. In particular, we consider how the design and capabilities of the formal reasoning system that we employ influence, aid, or hinder our ability to accomplish a formal reasoning task – the assembly of a machine-verifiable proof pertaining to the NetSketch formalism. NetSketch is a tool for the specification of constrained-flow applications and the certification of desirable safety properties imposed thereon. NetSketch is conceived to assist system integrators in two types of activities: modeling and design. It provides capabilities for compositional analysis based on a strongly-typed domain-specific language (DSL) for describing and reasoning about constrained-flow networks and invariants that need to be enforced thereupon. In a companion paper [13] we overview NetSketch, highlight its salient features, and illustrate how it could be used in actual applications. In this paper, we define using a machine-readable syntax major parts of the formal system underlying the operation of NetSketch, along with its semantics and a corresponding notion of validity. We then provide a proof of soundness for the formalism that can be partially verified using a lightweight formal reasoning system that simulates natural contexts. A traditional presentation of these definitions and arguments can be found in the full report on the NetSketch formalism [12].

Robust Sketching and Aggregation of Distributed Data Streams

The data streaming model provides an attractive framework for one-pass summarization of massive data sets at a single observation point. However, in an environment where multiple data streams arrive at a set of distributed observation points, sketches must be computed remotely and then must be aggregated through a hierarchy before queries may be conducted. As a result, many sketch-based methods for the single stream case do not apply directly, as either the error introduced becomes large, or because the methods assume that the streams are non-overlapping. These limitations hinder the application of these techniques to practical problems in network traffic monitoring and aggregation in sensor networks. To address this, we develop a general framework for evaluating and enabling robust computation of duplicate-sensitive aggregate functions (e.g., SUM and QUANTILE), over data produced by distributed sources. We instantiate our approach by augmenting the Count-Min and Quantile-Digest sketches to apply in this distributed setting, and analyze their performance. We conclude with experimental evaluation to validate our analysis.