Assertions in Java programs, if available, are useful for many program analysis problems (e.g., as test oracles, or correctness properties for program verification). The trouble is that writing assertions is often inadequately practiced. In this work, we develop a method which automatically generates likely assertions through a combination of testing and active learning. An initial set of assertions are first generated based the assumption that RuntimeException signals erroneous behaviors and necessary conditions must be asserted so as to prevent them. Next, we propagate the initial assertions through the programs by learning conditions which are likely necessary to guarantee not failing the initial assertions. In order to overcome the lack of user-provided test cases and limitation of random testing, we apply actively learning techniques with selective sampling so as to learn more accurate assertions. Our method is related to existing work on dynamic invariant generation with important differences, e.g., we learn from both test cases which satisfy or fail the initial assertions; we generate “artificial” test cases to overcome the lack of test cases; we learn conjunctive or even disjunctive assertions, etc. We have implemented our method as a self-contained tool called ALEARNER. ALEARNER is evaluated using benchmark programs from the software verification competition to show that we could learn useful assertions for program verification, as well as popular Java projects from Github to show that our method is scalable.
Pham Hong Long is currently a Ph.D. student at Singapore University of Technology and Design. He received Bachelor’s degree and Master’s degree in Computer Science from Hochiminh City University of Technology, Vietnam in 2012 and 2014 respectively. His current research interests include program analysis and program verification.