انتزاع های موثر برای تایید تحت مدل های حافظه آرام

We implemented our approach and evaluated it on a set of finite and infinite-state concurrent algorithms under two memory models: Intel׳s x86 TSO and PSO. Experimental results indicate that our technique achieves better precision and efficiency than prior work: we can automatically verify algorithms with fewer fences, faster and with lower memory consumption.