User Studies of Principled Model Finder Output

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.

Tierless Programming and Reasoning for Software-Defined Networks

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…

Toward a Lightweight Model of BGP Safety

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…

Using lightweight modeling to understand Chord

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…

A Repair Framework for Alloy

ARepair is a command line tool built on top of Alloy4.2. Given a faulty Alloy model (potentially with multiple faults) and a set of AUnit tests that capture the desired model properties, ARepair is able to repair the model so that all AUnit tests. Internally, ARepair has three main components: a fault locator that is…