Current Projects
Weaving Agentic Software Engineering into Intro Programming
I believe that (a) people need to wrestle with writing code manually to build understanding of how programs work and break, (b) that agents are here to stay and people/students will use them, and (c) that those who teach programming have a responsibility to prepare students to maintain ownership and accountability of the resulting code when they do outsource work to AI-based tools. Fortunately, there's a long history of work in software engineering and formal methods that addresses how to build programs collaboratively. These topics are usually taught in upper-level CS courses, however, not intro courses. I'm thus studying how to bring this content in much earlier, without sacrificing core learning about writing programs.
Shriram Krishnamurthi, Michael Littman, and I have an article forthcoming in CACM about our overall philosophy and approach. In Spring 2026, we ran an experimental course on agentic software engineering with students who had had at least one semester of programming experience. Our experience report has been accepted to SIGCSE 2027 (preprint will be posted soon).
In Fall 2026, I'm piloting an introductory course (CSCI-0111E) that adapts what we learned in the spring to novice programmers. The course is based on our Data-Centric Intro to Computing text, with additional materials for the agentic portions.
Data-Centric Computing Education
With both computing and data science becoming essential across disciplines, it's time to rethink introductory computer science education. We're developing data-centric computing as a blend of computer science, data science, and data engineering that provides skills to students across campus. We have an op-ed summarizing the goal, an introductory collegiate course, and a textbook (released August 2021). Our decisions are driven by our research in computing education. Our Bootstrap:Data Science curriculum provides a high-school pre-cursor for those starting in K-12.
Program Design and Plan Composition in Computing Education
Programming problems typically contain multiple subtasks, solutions to which must be integrated into a single program. This project explores how novice programmers decompose problems and compose subtask implementations. Our work emphasizes both the impact of programming languages and libraries on planning behavior, and pedagogies for teaching program design, planning, and composition.
Cross-Discipline Transfer of Knowledge in Computing Education
Bootstrap produces a family of curricula that integrate computing education for middle- and high-school students with other disciplines (such as algebra, physics, and social sciences). The research components of this project study the pedagogical techniques and curricular conditions under which knowledge gained through computing transfers back to the host discipline (and vice-versa for teachers).
Notional Machines for Computing Education
Notional machines are the abstract machines that programmers are attempting to control when they write programs. Different programming languages afford different notional machines, which in turn allow different misconceptions about language behavior. We are studying tradeoffs among notional machines and pedagogies for avoiding misconceptions in various CS courses, both intro- and upper-level.
Past Projects
Security Policy Analysis
Analysis of Datalog-based policies, such as those used for access-control and privacy. Our Margrave policy analyzer was a SAT-based engine for verifying properties of policies, as well as for verifying and exploring consequences of changes to policies. We also worked on models of how policies interact with underlying software systems.
Feature-Oriented Software Verification
Features are cohesive, user-facing behaviors of systems. Feature-oriented designs (like aspect-oriented design) modularize code around features. Shriram Krishnamurthi and I developed a theory of compositional verification of feature-based software designs; our approach generated logical constraints as interfaces on features used in open systems (in which not all features were known in advance).
Formal Reasoning with Timing Diagrams
Given a semantics, timing diagrams become a formal representation of system behavior. This project explored semantics and analysis techniques for such specifications. I proved that timing diagram verification is decidable, even though timing diagrams capture some non-context-free languages.