Code quality is an important component of programming practice, so it is essential to teach it to programming learners. Conditional statements, one of the first programming constructs novices encounter, can already exhibit numerous issues. However, identifying these issues manually and explaining them to novices is time-consuming, and many of their variations lack automatic detection methods. In this work, we introduce five issues found in novice code and present automatic detectors for each. Our detectors leverage a satisfiability-modulo-theory solver called Z3 to determine whether a set of conditions is satisfiable, enabling the identification of unnecessary or redundant conditions. Lastly, we analyze the prevalence of these issues in a large dataset of novice code.

Learning to write high-quality code is a critical skill for novice programmers, but manual code reviews are resource-intensive and do not scale well. Existing automated tools may fail to provide feedback that is relevant to novices, and even many educational tools overlook some novice-specific code quality defects or are difficult to adapt to new settings. To address these limitations, we developed EduLint, a customizable educational linter. It detects a wide range of novice-specific defects -- many of which are not addressed by other tools -- and is easy to adapt to diverse educational settings. To demonstrate this, we describe its deployments in several different courses and seminars, including a large CS1 course where students were required to fix issues EduLint identified. In a quasi-experiment, we observed that students were better at avoiding some of the defects several months after the CS1 course ended. Students also rated EduLint as clear and easy to use. Across all the deployments, EduLint has already delivered code quality feedback on hundreds of thousands of defects to thousands of users.

Clear, well-chosen names for variables and functions significantly enhance code readability and maintainability. In computer science education, teaching students to select appropriate identifiers is a critical task, especially in CS1. This study explores how large language models (LLMs) could assist in teaching this skill. While prior research has explored the use of LLMs in programming education, their precision and consistency in teaching code quality, particularly identifier selection, remains largely unexplored. For this purpose, this study investigated how well different LLMs can detect and report misleading identifiers. In a dataset of 33 code samples, we manually labeled misleading identifiers. On this dataset, we then tested five different LLMs on their ability to detect these misleading identifiers, measuring the overall accuracy, precision, recall, and f-score. Results revealed that the most successful model, GPT-4o, was able to correctly detect most of the manually flagged misleading variable names. However, it also tended to flag issues with variable identifiers in cases where the human evaluators would not, and refined prompting was not able to discourage this behavior.

Code quality is an important aspect of programming education, with duplicate code being a common issue. To help students learn to avoid code duplication, it is useful to provide them with actionable, specific feedback, not just a generic code duplication warning. In this paper, we introduce the concept of diagnosable code duplication, provide an overview of its various types, and propose a framework for automatic detection. We apply the framework to an introductory programming dataset to demonstrate its ability to provide specific feedback and reveal non-trivial differences in detected cases compared to simpler detectors.

Teaching code quality through manual code reviews scales poorly. Existing automated tools still miss relevant code quality defects and not all defects they report are relevant; they are also sometimes hard to adopt. The goal of my dissertation will be to identify relevant defects, develop new precise detectors for them and integrate those into an open-source automatic tool. This will improve the quality and availability of automatic code quality feedback.

Code quality is an important aspect of programming, as quality code is easier to maintain, and code maintenance makes up the majority of software cost. For that reason, code quality should be emphasized in programming education. Previous work has identified many code quality defects commonly made by students. However, the current state lacks a clear organization and prioritization of these defects. In this paper, we propose an organization framework for code quality defects, presenting a catalog that describes 80 defects, with a specific focus on defects frequently encountered in code by novice programmers. To determine which defects are worth pointing out to students, we conducted a survey among 72 educators, who rated the priority with which each defect should be reported to a student. These presented results serve multiple purposes: they facilitate comparison across various research studies, support the advancement of software tools, and offer inspiration for programming education.

Abstract The development of Symbiotic 9 focused mainly on two components. One is the symbolic executor Slowbeast, which newly supports backward symbolic execution including its extension called loop folding. This technique can infer inductive invariants from backward symbolic execution states. Thanks to these invariants, Symbiotic 9 is able to produce non-trivial correctness witnesses, which is a feature that is missing in previous versions of Symbiotic. We have also extended forward symbolic execution in Slowbeast with a basic support for parallel programs. The second component with significant improvements is the instrumentation module. In particular, we have extended the static analysis of accesses to arrays with features designed for programs that manipulate C strings. Symbiotic 9 is the Overall winner of SV-COMP 2022. Moreover, it won also the categories MemSafety and SoftwareSystems, and placed third in FalsificationOverall.

Abstract Symbiotic 8 extends the traditional combination of static analyses, instrumentation, program slicing, and symbolic execution with one substantial novelty, namely a technique mixing symbolic execution with k-induction. This technique can prove the correctness of programs with possibly unbounded loops, which cannot be done by classic symbolic execution.Symbiotic 8 delivers also several other improvements. In particular, we have modified our fork of the symbolic executorKleeto support the comparison of symbolic pointers. Further, we have tuned the shape analysis toolPredator(integrated already inSymbiotic 7) to perform better onllvmbitcode. We have also developed a light-weight analysis of relations between variables that can prove the absence of out-of-bound accesses to arrays.