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.
