CSR---SMA: Improving Software System Reliability via Mining Properties for Software Verification

许多软件系统可靠性问题是由应用程序编程接口（API）的不正确使用引起的。但是，API开发人员通常不会记录静态验证所需的API的细节或使用属性，因为指定大量API属性用于静态验证通常不准确或不完整，而且繁琐。本研究开发了新的技术和工具，用于从系统代码库上应用模型检查器生成的静态跟踪中挖掘API属性。这些挖掘的属性可用于静态验证和其他软件开发任务。这项研究从根本上推进了对应用软件工程和挖掘技术提高系统可靠性的认识和理解。该研究探索了新的方法，并将先进的挖掘算法应用于从系统代码库中挖掘属性。这项研究对社会的好处是双重的。首先，研究应该导致验证的做法，挖掘软件工件数据，提高软件系统的可靠性。其次，新的挖掘和软件分析的创新往往会在软件工程或系统学科内部甚至外部的应用程序或任务领域中迅速传播。

Many software system reliability issues are caused by incorrect usage of application programming interfaces (APIs). But API developers often do not document details or usage properties of APIs required by static verification, because specifying a large number of API properties for static verification is often inaccurate or incomplete besides being tedious. This research develops new techniques and tools for mining API properties from static traces generated by applying a model checker on system code repositories. These mined properties can be used for static verification and other software development tasks. The research fundamentally advances knowledge and understanding of applying software engineering and mining techniques in improving system reliability. The research explores new approaches with novel applications of advanced mining algorithms for mining properties from system code repositories. The benefits of this research to society are two-fold. First, the research should lead to verified practices for mining software-artifact data in improving software system reliability. Second, innovations in new mining and software analysis tend to propagate quickly across application or task domains within or even beyond the software engineering or systems discipline.