9320992 Tai Concurrent software systems are becoming more common and generally require very high reliability. Software analysis and testing techniques are critical for reducing software development cost and improving software quality. This project will investigate efficient techniques for reachability analysis of concurrent information not only for the verification of safety and liveness properties, but also for the generation of tests. The proposed approach to reachability analysis is a combination of incremental and partial-order analysis. For a concurrent program, sequences of synchronization events will be generated from the specification and implementation of this program and will be used to force deterministic executions of this program. This project will implement analysis and testing tools for concurrent software and will carry out experimental studies. ***
