X hits on this document

Powerpoint document

Algorithmic Verification of Concurrent Programs - page 70 / 100

217 views

0 shares

0 downloads

0 comments

70 / 100

for each (s 









> 0) {



’’

’



ComputeRTClosure(u, s) {

   if (s, s) 





       Remove (s, s’) from F

       for each u-successor s’’ of s’

           add (s, s’’) to F

       Add (s, s’) to RT(u)

   }

}

Context-bounded reachability (II)

A work item (s, p) indicates that from state s,

p(i) contexts of thread i remain to be explored

Document info
Document views217
Page views217
Page last viewedFri Dec 02 19:01:06 UTC 2016
Pages100
Paragraphs1586
Words3927

Comments