Search for: All records

ABSTRACT Water redistribution during rain events in drylands plays a critical role in the persistence and spatial pattern of vascular plants in these patchy ecosystems. Biological soil crusts (BSCs) form a membrane in the soil surface and mediate ecohydrological dynamics. However, little is known about their influence on dryland ecosystem state and spatial pattern under changing climate, which may alter total annual rainfall and intraannual rainfall regime. Building on existing models, we develop a model that considers BSC–vascular plant interactions and realistic ecohydrological dynamics under rainfall pulses. We find that the presence of BSCs often increases ecosystem resilience by promoting runoff to plants under high aridity. However, the benefit of BSCs comes at the cost of plant biomass under relatively wetter conditions; a threshold in BSC effect occurs when water losses from BSCs exceed the benefit by their surface water routing to plants. Increased resilience from BSCs, and their own persistence, can be promoted in finer soils and under rainfall regimes of less frequent events—projected for many drylands. Lastly, we find that BSCs alter feedbacks underlying plant spatial self‐organization and hence their formed patterns. In high aridity, BSCs likely ameliorate competition between plants through large scale runoff promotion, reducing plant spatial pattern regularity. Our analysis highlights that BSCs significantly shape drylands' response to climate change and their positive effects on resilience may be stronger and more pervasive in a drier future, but such benefits come at a cost of ecosystem biomass and productivity when aridity is outside a critical range. 

Formal verification is a gold standard for building reliable computer systems. Certified systems in particular come with a formal specification, and a proof of correctness which can easily be checked by a third party. Unfortunately, verifying large-scale, heterogeneous systems remains out of reach of current techniques. Addressing this challenge will require the use of compositional methods capable of accommodating and interfacing a range of program verification and certified compilation techniques. In principle, compositional semantics could play a role in enabling this kind of flexibility, but in practice existing tools tend to rely on simple and specialized operational models which are difficult to interface with one another. To tackle this issue, we present a compositional semantics framework which can accommodate a broad range of verification techniques. Its core is a three-dimensional algebra of refinement which operates across program modules, levels of abstraction, and components of the system's state. Our framework is mechanized in the Coq proof assistant and we showcase its capabilities with multiple use cases.