9402415 Avrunin The major obstacle to developing automated tools for the detection of faults in concurrent software systems is the state explosion problem: the number of possible states of a concurrenet system is, in general, exponential in the number of processes making up the system. but most real concurrent software systems remain beyond the reach of existing approaches to analysis. This project would continue the development of an approach to analysis based on generating necessary conditions for the existence of certain executions of a concurrent system and using integer programming to check the consistency of those conditions. This approach does not require enumeration or explicit representation of the states of the system being analyzed, and can be used to check such properties as deadlock, starvation, mutual exlusion, and minimum and maximum elapsed time between events. This project includes research intended to take advantage of the compositional structure and symmetries of a concurrent system and investigates connections with other automated analysis methods. ***
