Put yourself in the shoes of an algorithm designer working on some computational problem. You have found an algorithm running in time O(n^2), say, but after months of effort no faster algorithm is in sight. Perhaps your algorithm is already optimal – but how could you show this? This is the central challenge of fine-grained complexity theory. In the spirit of classical NP-hardness, this theory starts from the assumption that certain canonical problems are hard, and then uses so-called fine-grained reductions to show that many other problems are conditionally hard as well.

In this talk, I will first describe the basic concepts of fine-grained complexity along with some illustrative examples, before turning to more recent developments, including some of my own work. I will discuss some questions that resisted the basic theory for a long time, and how progress on them has required a more sophisticated method – the celebrated structure-versus-randomness paradigm.

Generative AI holds great promise in enhancing programming education by automatically generating personalized feedback for students. However, ensuring that this feedback is both technically accurate and pedagogically effective remains a critical challenge before these systems can be safely deployed in real-world classrooms. This thesis investigates the end-to-end integration of generative AI in programming education, divided into two main parts.

The first part focuses on the optimization of AI-generated feedback quality. We introduce novel techniques that not only enhance the generated feedback but also perform automatic validation of the feedback before returning it. Specifically, to improve feedback quality, our techniques contextualize the prompt with similar examples from the database and uses symbolic information of failing test cases and fixes. Next, to validate the quality of AI-generated feedback, they leverage another AI agent as simulated students in a run-time validation mechanism. These techniques achieve high-precision, human tutor-style feedback.

The second part transitions to the deployment of the feedback systems in real-world classroom settings, focusing on student-instructor-AI interaction. Specifically, to ensure feedback meets both expert educators' and students' quality standards, we investigate the discrepancies between expert-created rubrics and student perceptions of hint helpfulness. To understand how to position AI-generated hints with traditional pedagogical practices, we examine the interplay between AI-generated hints and student reflection. To address the problem of students being over-reliant on AI support, we base our design on metacognitive theory to introduce different hint types with quotas to require students' critical engagement during interaction with the system. Finally, to ensure students receive relevant support in difficult cases when AI is insufficient, we propose a hybrid instructor-in-the-loop escalation mechanism, allowing instructors to efficiently involve and support students when most needed.

Ultimately, this thesis provides a foundational framework for deploying LLMs that balance automated efficiency with established pedagogical standards and human oversight.

Floating-point numbers often represent real numbers in computer systems. They are applicable in many domains, including embedded systems, machine learning, and scientific computing. Despite their widespread use, they pose some difficulties. Floating-point numbers and operations typically suffer from roundoff errors, making computations over floating-points inaccurate with respect to a real-valued specification. Moreover, the IEEE 754 floating-point standard, a fundamental element in formalizing floating-point arithmetic for today’s computers, presents additional challenges due to special values and resulting unintuitive behaviors. This thesis has three main contributions that address existing gaps in automated reasoning about floating-point arithmetic, making it easier for developers and researchers to understand, verify, and trust the floating-point computations in their programs. First, we introduce the first floating-point support in a deductive verifier for the Java programming language. Our support in the KeY verifier automatically handles floating-point arithmetic and transcendental functions. We achieve this with a combination of delegation to external SMT solvers on one hand, and rule-based reasoning within KeY on the other, exploiting the complementary strengths of both approaches. As a result, this approach can prove functional floating-point properties for realistic programs. Second, inspired by KeY’s treatment of method calls and the need for a scalable roundoff error analysis, we present the first modular optimization-based roundoff error analysis for non-recursive procedural floating-point programs. Our key idea is to achieve modularity while maintaining reasonable accuracy by automatically computing procedure summaries that are a function of the input parameters. Technically, we extend an existing optimization-based roundoff error analysis and show how to effectively use first-order Taylor approximations to compute precise procedure summaries, and how to integrate those to obtain end-to-end roundoff error bounds. Third, our experience using SMT solvers to discharge KeY’s floating-point verification conditions revealed unexpected performance behavior, motivating a systematic study of floating-point reasoning in SMT solvers. We propose a metamorphic testing approach that uses semantics-preserving rewrite rules, focusing on floating-point special values, to uncover unexpected performance behavior in SMT solvers’ handling of floating-point formulas, such as an increase in solving time when the SMT queries are simplified. Using real-world test inputs, our approach can identify such performance bugs for every SMT solver tested.

The synthesis of logical controllers that guarantee desired specifications is a central problem in the design of cyber-physical systems (CPS). In practice, such guarantees rely on assumptions about how the controller interacts with its environment. These assumptions restrict environment behavior to make synthesis feasible, but in existing approaches they are often overly restrictive, leading to conservative designs and limiting the range of behaviors that systems can safely accommodate.

This thesis rethinks the role of assumptions in logical controller synthesis by emphasizing their \emph{permissiveness}---the ability to capture a wide range of admissible environment behaviors. We study permissive assumptions in two key settings: (a) interactions among multiple discrete components in distributed systems, and (b) interactions between high-level logical controllers and low-level physical dynamics in hybrid systems. In both settings, we develop theoretical and algorithmic foundations for computing and exploiting permissive assumptions to enable new design paradigms for logical controller synthesis.

For distributed systems, we define permissiveness as capturing all cooperative behaviors of other components that enable a controller to satisfy its specification. We present an algorithm for computing such assumptions in monolithic systems and extend it to distributed systems via a negotiation-based framework that iteratively constructs permissive assume-guarantee contracts for each component. These contracts enable decentralized synthesis and are applied to human-robot interaction, allowing robots to cooperate with humans whenever possible and request cooperation only when necessary.

For hybrid systems, we utilize permissive assumptions on the plant model---the abstract representation of physical dynamics---to address three key challenges. To enable seamless adaptation of controllers to changing logical contexts, i.e., changes in high-level goals or tasks, we introduce a novel synthesis framework that utilizes \emph{persistent live groups}, a class of assumptions capturing liveness properties of continuous dynamics. To improve scalability to large or uncertain plant models, we develop \emph{universal controllers} where decisions are conditioned on branching-time assumptions called \emph{prophecies}, which are learned from representative models and efficiently verified at runtime on unseen plant models. Finally, to enhance robustness under uncertainty or partial violations of assumptions on the plant model, we introduce a robust semantics for branching-time temporal logics, enabling formal reasoning about controller behavior under such violations.

Overall, this work enables correctness-by-construction synthesis while avoiding unnecessary conservatism, resulting in CPS that are more robust, scalable, and responsive.