今天开小组会的时候，谈到JPF的扩展和使用，就想总结一下10-11年相关会议上使用JPF的几篇论文，这里简单整理下：
1. P. Joshi, M. Naik, K. Sen, and D. Gay, "An effective dynamic analysis for detecting generalized deadlocks," in Proceedings of the eighteenth ACM SIGSOFT international symposium on Foundations of software engineering, Santa Fe, New Mexico, USA, 2010, pp. 327-336.
这篇文章的主要思想是：将一个多线程的Java程序抽象成一个简单的trace program，再使用JPF作为Model Checker来探索这个trace program的所有的线程交互情况。这篇文章的主要贡献是：去除掉了大部分可能造成state-space explosion的程序逻辑，仅仅在trace program中保留和多线程相关的逻辑。
2. M. Gligoric, T. Gvero, V. Jagannath, S. Khurshid, V. Kuncak, and D. Marinov, "Test generation through programming in UDITA," in Proceedings of the 32nd ACM/IEEE International Conference on Software Engineering - Volume 1, Cape Town, South Africa, 2010, pp. 225-234.
后面这两篇文章实际上都是同一个研究小组写的：由Darko Marinov领导的在UIUC的小组，他们的论文在JPF的论文列表页面中也有介绍，所以，这两篇论文不能说明JPF的影响力，因为作者和他们关系太密切。（上一篇文章是UCBerkeley和Intel Lab的人写的，暂时看不出和JPF这个项目有什么私人关系。）
这篇文章的主要思想是：介绍了一种测试用例生成语言：UDITA，UDITA具有Non-deterministic choice operators和能够生成linked structures的接口，而作者将JPF作为这种语言实现的主要平台。我对non-deterministic program的确切含义也不是很了解。感兴趣的同学可以自己去查查。
3. V. Jagannath, Q. Luo and D. Marinov, "Change-aware preemption prioritization," in Proceedings of the 2011 International Symposium on Software Testing and Analysis, Toronto, Ontario, Canada, 2011, pp. 133-143.
和第2篇文章的作者单位相同。
这篇文章的主要思想是：对于多线程程序，回归测试中测试用例的选择和执行成本都比较高，他们提出了基于软件演化过程中的变动信息，来prioritize多线程回归测试的搜索顺序。他们使用JPF和另外一种自己开发的framework为基础，来实现自己的算法。其中，作者通过修改JPF中已经存在的SimplePrioritySearch 这个模块来prioritize搜索过程。（这个SimplePrioritySearch是个模块还是个什么东西，我们可以接下来搞清楚。）
今天就简单总结下这三篇文章。