Block-based visual programming initiatives such as Hour of Code by code.org and Intro to Programming with Karel by CodeHS.com, have transformed introductory computer science education by making programming more accessible to K-8 learners. Despite their accessibility, students often struggle with multi-step reasoning and conceptual abstraction when solving open-ended tasks. Quizzes (such as fill-in-the-gap exercises, and multiple-choice conceptual questions based on code debugging and task design) offer interactive practice and targeted feedback that can promote active learning and scaffold novice programmers. However, manually designing such quizzes is time-consuming and difficult to scale. This thesis tackles these challenges by developing automated synthesis techniques for programming tasks and quizzes, and evaluates their pedagogical utility.

The first part of the thesis introduces algorithmic methods for synthesizing programming tasks and quizzes in block-based environments. Specifically, we develop methods for the following : (i) synthesizing conceptually similar and yet visually dissimilar write-code tasks; and (ii) synthesizing adaptive multiple-choice programming quizzes that address student-specific misconceptions; Each method leverages symbolic execution, sketch-based code mutation, and search-guided generation to ensure pedagogical utility, relevance, and technical correctness. Empirical evaluations conducted through controlled user studies demonstrate the efficacy of these approaches, showing that they not only support novice learners effectively but also outperform existing methods, including next-step code edit based feedback methods.

The second part of the thesis empirically evaluates the pedagogical utility of programming quizzes in these environments via user studies and classroom deployments with K-8 learners. Specifically, we examine: (i) the design, validation, and classification of quiz types using cognitive frameworks such as Bloom's Revised Taxonomy; (ii) the impact of embedding quizzes within programming curricula on post-learning outcomes; and (iii) the effectiveness of quiz-based feedback scaffolds with different quiz-types. Our findings show that quizzes designed using metacognitive strategies and adapted to learners’ attempts significantly enhance engagement and task performance. Moreover, we observe that richer and more diverse quiz types—when integrated into the curriculum—lead to improved post-learning outcomes, while simpler, less cognitively demanding quizzes may hinder post-learning performance.

Overall, this thesis contributes novel synthesis methods for programming quizzes and empirical evidence of their effectiveness in elementary-level programming education. These findings provide a foundation for scalable and adaptive support in elementary computing curricula.

Critical autonomous systems, such as robots operating amongst humans or a rover navigating on a remote planet, must continuously react to environments they do not control while provably satisfying their specifications. Designing a correct controller for such machines manually is impossible as a human cannot foresee every environmental possibility. Reactive synthesis provides an alternative approach of automatically building correct-by-construction controllers from formal specifications. Although this is a well-studied field, it almost entirely focuses on finding a single controller that satisfies the specification. The real world, however, is transient, and a single controller is rarely sufficient in practical applications. When an action proposed by the controller becomes unavailable (e.g., due to a component failure), the system immediately stalls, forcing an expensive re-synthesis.

This thesis addresses this problem by introducing a concise data-structure, called the strategy template, which represents infinitely many controllers. Strategy templates localize a given specification by local guidelines for a controller to choose the next action. In the first part of the thesis, we define the notion of strategy templates for major classes of specifications and models of interaction of the system and the environment. We then provide algorithms for computing the templates, and prove soundness (i.e., a controller following the template satisfies the specification) and completeness (i.e., if there is a controller that satisfies the specification, we compute a strategy template). We show that the strategy templates enable us to compose various specification online, and make controllers more robust to changes in the environment at runtime. In the second part, we utilize the resulting permissiveness (i.e., capturing infinitely many controllers) of the templates to shield learned policies which usually lack formal guarantees of correctness. The templates allow us to monitor and nudge the policies to ensure that they satisfy liveness (i.e., some progress is made), which until now had eluded the shielding literature. Furthermore, we implement all the algorithms proposed and show that they outperform the state-of-the-art in terms of composibility, robustness and scalability.