Automated Analysis of Concurrent and Real-Time Software

This paper surveys the current status of our work on automated anal-ysis of the logical and timing properties of concurrent software based on the constrained expression approach. It describes our analysis toolset, reports some extremely encouraging results of using the toolset to ana-lyze logical properties of nontrivial concurrent systems, and discusses the modifications we have made to the toolset to apply it to analyzing tim-ing properties. It then outlines ongoing and planned research directed at further improving these methods