Batfish is a tool to analyze network configurations and forwarding. It has evolved from a research prototype to an industrial-strength product, guided by scalability, fidelity, and usability challenges encountered when analyzing complex, real-world networks. We share key lessons from this evolution, including how Datalog had significant limitations when generating and analyzing forwarding state and how binary decision diagrams (BDDs) proved highly versatile. We also describe our new techniques for addressing real-world challenges, which increase Batfish performance by three orders of magnitude and enable high-fidelity analysis of networks with thousands of nodes within minutes.

Test-driven methodologies encourage testing early and often. "Mock objects" support this approach by allowing a component to be tested before all depended-upon components are available. Today mock objects typically reflect little to none of an object's intended functionality, which makes it difficult and error-prone for developers to test rich properties of their code. This paper presents "declarative mocking", which enables the creation of expressive and reliable mock objects with relatively little effort. In our approach, developers write method specifications in a high-level logical language for the API being mocked, and a constraint solver dynamically executes these specifications when the methods are invoked. In addition to mocking functionality, this approach seamlessly allows data and other aspects of the environment to be easily mocked. We have implemented the approach as an extension to an existing tool for executable specifications in Java called PBnJ. We have performed an exploratory study of declarative mocking on several existing Java applications, in order to understand the power of the approach and to categorize its potential benefits and limitations. We also performed an experiment to port the unit tests of several open-source applications from a widely used mocking library to PBnJ. We found that more than half of these unit tests can be enhanced, in terms of the strength of properties and coverage, by exploiting executable specifications, with relatively little additional developer effort.