Multi-pushdown automata (MPDA) are a classic computational model that can be used to capture the behavior of multithreaded recursive programs. Here, each parallel thread is simply modeled by a single stack, and there is a fixed number of them. Due to the well known fact that most verification problems are undecidable for MPDA, even with just two stacks, the literature contains many different ways to restrict the runs of this model, in such a manner as to recover decidability. A popular restriction of this kind is known as bounded context-switching: For a fixed bound k, every parallel thread (or stack) may only be interrupted by another thread up to k times.

We consider an extended setting, where the number of parallel threads is not fixed, and more of them can be spawned dynamically during execution. This gives rise to the model of dynamic networks of concurrent pushdown systems (DCPS), which we still restrict with bounded context-switching. In this setting, we consider various verification questions, that have been asked for similar models in the past. These include state reachability, non-termination (with and without assumptions on fairness), and boundedness of the thread buffer. Moreover we consider the novel verification problem of Dyck inclusion: Given a model with action sequences over some alphabet of bracket pairs, are all its executions well-bracketed? Our results close a preexisting complexity gap for state reachability, and settle the complexity of several other verification problems, where in many cases even decidability was unknown before

Software is what turns quantum hardware into technology everyone can use. In this talk we focus on the quantum communication networks, with the first metropolitan scale quantum networks being built and the technologies to connect them over long distances advancing. We begin with the first operating system for quantum networks (QNodeOS), allowing applications to be programmed and executed on arbitrary quantum processors connected to a quantum network. Demonstrated on two different types of quantum hardware, QNodeOS now provides a framework for experimenting with software systems for quantum networks. We then turn to a specific kind of quantum network application, in which entanglement is harnessed for coordination between distant parties. We explore this through a recent example in radio spectrum allocation, opening the door to a new domain of quantum network applications.

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.