Zing: A model checker for concurrent software - Andrews, Tony; Qadeer, Shaz; Rajamani, Sriram; Rehof, Jakob; Xie, Yichen (Proceedings of the 16th International Conference on Computer Aided Verification (CAV 2004)., 2004)
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. The goal is to preserve as much of the control-structure of the source program as possible. Zing's model checker exploits the structure of the source program, which is preserved in the model, to optimize systematic state space exploration. We believe that such an infrastructure is useful for finding bugs in software at various levels: high-level protocol descriptions, work-flow specifications, web services, device drivers, and protocols in the core of the operating system.