SEJun 30, 2021
Verifix: Verified Repair of Programming AssignmentsUmair Z. Ahmed, Zhiyu Fan, Jooyong Yi et al.
Automated feedback generation for introductory programming assignments is useful for programming education. Most works try to generate feedback to correct a student program by comparing its behavior with an instructor's reference program on selected tests. In this work, our aim is to generate verifiably correct program repairs as student feedback. The student assignment is aligned and composed with a reference solution in terms of control flow, and differences in data variables are automatically summarized via predicates to relate the variable names. Failed verification attempts for the equivalence of the two programs are exploited to obtain a collection of maxSMT queries, whose solutions point to repairs of the student assignment. We have conducted experiments on student assignments curated from a widely deployed intelligent tutoring system. Our results indicate that we can generate verified feedback in up to 58% of the assignments. More importantly, our system indicates when it is able to generate a verified feedback, which is then usable by novice students with high confidence.
SEApr 24, 2018
Toward a Better Understanding of How to Develop Software Under Stress - Drafting the Lines for Future ResearchJoseph Alexander Brown, Vladimir Ivanov, Alan Rogers et al.
The software is often produced under significant time constraints. Our idea is to understand the effects of various software development practices on the performance of developers working in stressful environments, and identify the best operating conditions for software developed under stressful conditions collecting data through questionnaires, non-invasive software measurement tools that can collect measurable data about software engineers and the software they develop, without intervening their activities, and biophysical sensors and then try to recreated also in different processes or key development practices such conditions.
PLSep 20, 2013
A Case for Dynamic Reverse-code Generation to Debug Non-deterministic ProgramsJooyong Yi
Backtracking (i.e., reverse execution) helps the user of a debugger to naturally think backwards along the execution path of a program, and thinking backwards makes it easy to locate the origin of a bug. So far backtracking has been implemented mostly by state saving or by checkpointing. These implementations, however, inherently do not scale. Meanwhile, a more recent backtracking method based on reverse-code generation seems promising because executing reverse code can restore the previous states of a program without state saving. In the literature, there can be found two methods that generate reverse code: (a) static reverse-code generation that pre-generates reverse code through static analysis before starting a debugging session, and (b) dynamic reverse-code generation that generates reverse code by applying dynamic analysis on the fly during a debugging session. In particular, we espoused the latter one in our previous work to accommodate non-determinism of a program caused by e.g., multi-threading. To demonstrate the usefulness of our dynamic reverse-code generation, this article presents a case study of various backtracking methods including ours. We compare the memory usage of various backtracking methods in a simple but nontrivial example, a bounded-buffer program. In the case of non-deterministic programs such as this bounded-buffer program, our dynamic reverse-code generation outperforms the existing backtracking methods in terms of memory efficiency.