Model checking black-box distributed systems


We model check unmodified Go-based implementations of distributed systems.

Model checking is a bug finding technique that attempts to exhaustively explore a model of the system, checking a property supplied by the user on each of the states in the model. In the Dara project we are building a blackbox implementation-level model checker. That is, the checker uses the distributed system implementation as the model. This allows Dara to be applied to existing systems and requires much less effort from a developer than traditional model checking approaches.

Additional Information

Dara implementation

arrow_back Back

Systopia lab is supported by a number of government and industrial sources, including Cisco Systems, the Communications Security Establishment Canada, Intel Research, the National Sciences and Engineering Research Council of Canada (NSERC), Network Appliance, Office of the Privacy Commissioner of Canada, and the National Science Foundation (NSF).