Brown CS News

Only weeks after earning the European Conference on Object-Oriented Programming (ECOOP) Distinguished Paper and Distinguished Artifact Awards for work in formal methods visualization, Brown University Programming Languages Team (Brown PLT) has received an International Conference on Computer-Aided Verification (CAV) Distinguished Paper Award for an unrelated project: a new misconception-based automated Linear Temporal Logic tutoring system. The research is the work of Brown CS doctoral student Siddhartha Prasad, Ben Greenman of the University of Utah (formerly a Brown CS postdoctoral researcher), and Brown CS faculty members Tim Nelson and Shriram Krishnamurthi.

“We’ve been engaged in a multi-year project to improve education in Linear Temporal Logic (LTL),” Siddhartha explains, “and we’ve arrived at a detailed understanding of typical misconceptions that learners and even experts have. When they make mistakes, they need explanations of what went wrong, additional drill problems, and checks regarding whether they got the additional ones right. We’ve distilled our group’s expertise in LTL into a free online tutor.”

In contrast to traditional tutoring systems, which are often tied to a specific curriculum or course, LTL Tutor adaptively generates multiple-choice question-sets, responding to wrong answers with feedback that includes visual metaphors, counterexamples, or an interactive trace-stepper that shows the evaluation of an LTL formula across time. When a mistake recurs, it provides further insight in the form of tailored text grounded in previous research. LTL Tutor also meets practical instructor needs by being curriculum agnostic, offering detailed reporting, and being fully self-hostable.

You can try the LTL Tutor yourself here, read the paper here, or read Brown PLT’s blog post about it here.

For more information, click the link that follows to contact Brown CS Communications Manager Jesse C. Polhemus.