This paper presents a compact Petri net representation that is e cient to construct for concurrent programs that use explicit tasking and rendezvous style communication. These Petri nets are based on task interaction graphs and are called TIG-based Petri nets (TPN)s. They form a compact repion by abstracting large regions of program execution with associated summaryinformation that is necessary for performing program analysis. We present a exible framework for checking a variety of properties of concurrent programs using the reachability graph generated from a TPN. We present experimental results that demonstrate the bene t of TPNs over alternate Petri net representations and discuss the applicability of Petri net reduction techniques to TPNs. 1 This work was supported by the Defense Advanced Research Projects Agency under Grant MDA972-91-J-1009
Matthew B. Dwyer, Lori A. Clarke, Kari A. Nies