Zing: A Model Checker for Concurrent Software

The zing project is an effort to build a flexible and scalable model checking infrastructure for concurrent software. The project is divided into four components: (1) a modeling language for expressing concurrent models of software systems, (2) a compiler for translating a zing model into an executable representation of its transition relation, (3) a model checker for exploring the state space of the zing model, and (4) model generators that automatically extract zing models from programs written in common programming languages.