Model-finders such as SAT-solvers are attractive for producing concrete models, either as sample instances or as counterexamples when properties fail. However, the generated model is arbitrary. To address this, several research efforts have proposed principled forms of output from model-finders. These include minimal and maximal models, unsat cores, and proof-based provenance of facts.

We present Flowlog, a tierless language for programming SDN controllers. In contrast to languages with different abstractions for each program tier—the controlplane, data-plane, and controller state—Flowlog provides a unified abstraction for all three tiers. Flowlog is reminiscent of both SQL and rule-based languages such as Cisco IOS and JunOS; unlike these network configuration languages, Flowlog…

We describe an Alloy model that helps check the correctness of a discrete wet-dry algorithm used in a system for hurricane storm surge prediction. Derived from simplified physics and encoded with empirical rules, the algorithm operates on a finite element mesh to allow the propagation of overland flows. Our study is motivated by complex interactions…

For the past ten years, researchers have used the Stable Paths Problem (SPP) to analyze the stability properties of the Border Gateway Protocol (BGP). Analysis of SPP has revealed several combinations of topologies and routing configurations (or gadgets) where BGP cannot converge to a unique stable solution. Researchers typically analyze SPP by hand, using a…

A crucial requirement for many multi-site production services operating at global scale is the need for exclusive access to latest state. Here, a novel approach to address these requirements through the abstraction of a critical section over geo-distributed state is proposed. This abstraction is realized in a key-value store called MUSIC, which provides critical sections…

The Chord distributed hash table (DHT) is wellknown and often used to implement peer-to-peer systems. Chord peers find other peers, and access their data, through a ringshaped pointer structure in a large identifier space. Despite claims of proven correctness, i.e., eventual reachability, previous work has shown that the Chord ring-maintenance protocol is not correct under…

Correctness of the Chord ring-maintenance protocol would mean that the protocol can eventually repair all disruptions in the ring structure, given ample time and no further disruptions while it is working. In other words, it is “eventual reachability.” Under the same assumptions about failure behavior as made in the Chord papers, no published version of…

The trustworthiness of modern networked services is too important to leave to chance. We need to design these services with specific properties in mind, and verify that the properties hold. In this paper, we argue that a compositional network architecture, based on a notion of layering where each layer is its own complete network customized…