Zing: Exploiting Program Structure for Model Checking Concurrent Software

摘要: Model checking is a technique for finding bugs in systems by systematically exploring their state spaces. We wish to extract sound models from concurrent programs automatically and check the behaviors of these systematically. The zing project an effort build flexible infrastructure represent model abstractions large software.