科研之友
微信
新浪微博
Facebook
分享链接
摘要
In this paper, we present Checkmate, the first generic static analyzer of multithreaded Java programs based on abstract interpretation. Checkmate can be tuned at different levels of precision and efficiency in order to prove various properties (e.g., absence of divisions by zero and data races), and it is sound for multithreaded programs. It supports all the most relevant features of Java multithreading, such as dynamic thread creation, runtime creation of monitors, and dynamic allocation of memory. The experimental results demonstrate that Checkmate is accurate and efficient enough to analyze programs with some thousands of statements and a potentially infinite number of threads.
- 出版日期2013-6
