Use of symbolic execution as automated grading tool for introductory programming courses

The use of automated grading tools to provide feedback to students is common in Computer Science education. The first step of automated grading is to find defects in the student program. However, finding bugs in code has never been easy. Current automated grading tools do not focus on identifying defects inside student code. Instead, the most common way to determine correctness is to compare computation results for a fixed set of test cases. It takes time and effort to design a set of test cases that test the student code thoroughly. In practice, the tests used for grading are often insufficient for accurate diagnosis. Meanwhile, automated testing tools for commercial code have been developing for some time. Using these tools, we can deliver scalable, high-quality feedback. We believe that with some modifications, automated testing tools for commercial code can also improve Computer Science education. In this thesis, we present our modification and utilization of automated testing on student assignments in an introductory programming course. We implemented a framework to collect student codes and to apply industrial automated testing to their codes. To enable scalable feedback generation by the tools, we integrated I/O functions into our tool, developed an algorithm to speed up execution through loops and implemented a cross-execution cache for queries. We also implemented interpretation of the results of the tools in a way that students can understand easily. In order to provide timely feedback to students, we modified the current state-of-the-art symbolic execution tool KLEE. Because the I/O functions are used heavily by students, we integrated them into our tool. We implemented a new path exploration algorithm that reduces the number of paths needed to achieve high coverage. We have tested our Loop Reduction algorithm with 235 student-generated versions of a classroom assignment. We demonstrate how our algorithm helps to achieve the same coverage with speedup of 11.8X for 117 out of the 235 programs, while adding 15% max observed and 2% average overhead over the 50% of programs not benefiting from the technique. The maximum speedup for a single program is 52.3X. We also implemented a cross-execution cache for the SMT queries. We found that the transmission and translation of query creates an overhead of about 20% coupled with the fact that query solving time only takes about 60% of overall analysis time. We find that we can achieve a speedup of 1.5x. We deployed our framework on eight different introductory C programming assignments here at the University of Illinois at Urbana-Champaign for over four years. The setup work takes a senior undergraduate student about 5-10 hours for each assignment. The results show that the automated feedback generation framework can detect more bugs inside student programs, as well as errors in the assignment specification, released tests, and released gold program. We can generate helpful feedback to students that helps them to learn from their own mistakes, and help instructors to identify misunderstood concepts. We can also grade more thoroughly and more fairly. We believe that automated testing tools based on symbolic execution are the future of improving Computer Science education