并发程序分析验证

难点在于线程交错执行带来的巨大状态空间。

一类组合方法：compositional concurrent program verification (sample-generalize-check)

Liveness: Liveness of Concurrent Program