Search for: All records

The increasing wildfire activity and rapid population growth in the wildland–urban interface (WUI) have made more Americans exposed to wildfire risk. WUI mapping plays a significant role in wildfire management. This study used the Microsoft building footprint (MBF) and the Montana address/structure framework datasets to map the WUI in Montana. A systematic comparison of the following three types of WUI was performed: the WUI maps derived from the Montana address/structure framework dataset (WUI-P), the WUI maps derived from the MBF dataset (WUI-S), and the Radeloff WUI map derived from census data (WUI-Z). The results show that WUI-S and WUI-P are greater than WUI-Z in the WUI area. Moreover, WUI-S has more WUI area than WUI-P due to the inclusion of all structures rather than just address points. Spatial analysis revealed clusters of high percentage WUI area in western Montana and low percentage WUI area in eastern Montana, which is likely related to a combination of factors including topography and population density. A web GIS application was also developed to facilitate the dissemination of the resulting WUI maps and allow visual comparison between the three WUI types. This study demonstrated that the MBF can be a useful resource for mapping themore »WUI and could be used in place of a national address point dataset.« less

Memory models play an important role in verified compilation of imperative programming languages. A representative one is the block-based memory model of CompCert---the state-of-the-art verified C compiler. Despite its success, the abstraction over memory space provided by CompCert's memory model is still primitive and inflexible. In essence, it uses a fixed representation for identifying memory blocks in a global memory space and uses a globally shared state for distinguishing between used and unused blocks. Therefore, any reasoning about memory must work uniformly for the global memory; it is impossible to individually reason about different sub-regions of memory (i.e., the stack and global definitions). This not only incurs unnecessary complexity in compiler verification, but also poses significant difficulty for supporting verified compilation of open or concurrent programs which need to work with contextual memory, as manifested in many previous extensions of CompCert. To remove the above limitations, we propose an enhancement to the block-based memory model based on nominal techniques; we call it the nominal memory model. By adopting the key concepts of nominal techniques such as atomic names and supports to model the memory space, we are able to 1) generalize the representation of memory blocks to any types satisfyingmore »the properties of atomic names and 2) remove the global constraints for managing memory blocks, enabling flexible memory structures for open and concurrent programs. To demonstrate the effectiveness of the nominal memory model, we develop a series of extensions of CompCert based on it. These extensions show that the nominal memory model 1) supports a general framework for verified compilation of C programs, 2) enables intuitive reasoning of compiler transformations on partial memory; and 3) enables modular reasoning about programs working with contextual memory. We also demonstrate that these extensions require limited changes to the original CompCert, making the verification techniques based on the nominal memory model easy to adopt.« less