Title: Eventually, Understanding: Operationalizing Misconceptions in LTL

Speaker: Siddhartha Prasad    (bio) (bio)

Siddhartha Prasad is a PhD student in Computer Science at Brown University, advised by Shriram Krishnamurthi. His research takes a programming-languages approach to improving how people express intent and reason about program behavior, drawing on ideas from formal methods, human-computer interaction, and cognitive science. He is especially interested in how models of human cognition can inform the design of languages, semantics, and interactive tools for understanding complex computational structures.

Previously, he was a software engineer at Microsoft, where he worked both on Windows and Azure. He says that his research interests are informed by his time as an engineer. In his own words, "I have written code that doesn't do what I want it to, and I want to spare everyone else the indignity."

When: Tuesday, 10 March 2026 at 1900 hrs (IST)  

Meeting Details: Zoom link, ID: 891 6409 4870, Passcode: 082194

Abstract:
Linear Temporal Logic (LTL) sits at the heart of verification and synthesis, yet even experienced users routinely misunderstand what formulas actually say. Over several years, we have studied LTL from a human-factors perspective across classrooms and controlled experiments, building instruments to surface the misconceptions people hold about its semantics and use. These studies show that misconceptions are not isolated mistakes but systematic misunderstandings that persist across levels of expertise and directly affect specification quality.

This talk centers those misconceptions as the object of design. We present LTL Tutor, a lightweight, curriculum-agnostic system that operationalizes these insights into targeted practice with immediate, actionable feedback. The tutor generates exercises grounded in common misconceptions, explains errors in terms of the learner's answer versus the correct semantics, and uses a concept-based mutation engine to adaptively drill the ideas each learner struggles with. It is designed to fit into existing courses without requiring changes to teaching style, while also supporting independent learners with minimal prior instruction. By tying feedback to concrete errors and surfacing the underlying misconceptions over time, the tutor turns several years of research on how people misunderstand LTL into a practical, deployable tool for both classrooms and self-guided study.