Developers routinely use GenAI tools (large language models enriched in various ways) to generate useful components of programs, such as regular expressions. While pleasant and often effective, this can easily lead to subtle bugs. The developer may have been unclear in their specification, they may not fully understand the language of the output, there may be systematic misconceptions suffered by the user and perhaps even embedded in the language model, and so on. Responsible use of GenAI requires humans in the loop. To be effective, the human interaction must be both meaningful and moderate. We accomplish this as follows. First, we generate multiple candidate expressions instead of one. We then use formal language containment properties to generate distinguishing concrete scenarios that illustrate the differences between the candidates. We then have users rate these concrete scenarios. This process converges in a few steps, while also giving the user insight into any lack of clarity on their part. We have built a tool, pick, that implements this iterative process. We apply it to three formal languages with the necessary properties: regexes, linear temporal logic, and access-control policies. We show through experiments that pick is a significant improvement over showing users the candidate expressions, and also helps catch situations where no output is a match.

Diagrams enable programmers to reason, debug, and communicate. However, constructing diagrams for programming language data is unnecessarily hard. We present a declarative DSL, Spytial, that captures the essential spatial features of data. We endow Spytial with a spatial semantics, mapping values to the 2D plane, and prove key properties. Spytial uses constraint-solving to make interactive renderings. We show how Spytial can be embedded in three very different languages: Python, Rust, and Pyret. We present a novel counterfactual debugging aid for diagramming errors, combining textual and visual output. We evaluate the language and system for expressiveness, performance, and diagnostic quality. Finally, we also show how Spytial can be used to construct values interactively and visually while preserving spatial constraints.

Abstract Linear Temporal Logic (LTL) is used widely in verification, planning, and more. Unfortunately, users often struggle to learn it. To improve their learning, they need drill, instruction, and adaptation to their strengths and weaknesses. Furthermore, this should fit into whatever learning process they are already part of (such as a course). In response, we have built a misconception-based automated tutoring system. It assumes learners have a basic understanding of logic, and focuses on their understanding of LTL operators. Crucially, it takes advantage of multiple years of research (by our team, with collaborators) into misconceptions about LTL amongst both novices and experts. The tutor generates questions using these known learner misconceptions; this enables the tutor to determine which concepts learners are strong and weak on. When learners get a question wrong, they are offered immediate feedback in terms of the concrete error they made. If they consistently demonstrate similar errors, the tool offers them feedback in terms of more general misconceptions, and tailors subsequent question sets to exercise those misconceptions. The tool is hosted for free on-line, is available open source for self-hosting, and offers instructor-friendly features.

Much of early literacy education happens at home with caretakers reading books to young children. Prior research demonstrates how having dialogue with children during co-reading can develop critical reading readiness skills, but most adult readers are unsure if and how to lead effective conversations. We present ContextQ, a tablet-based reading application to unobtrusively present auto-generated dialogic questions to caretakers to support this dialogic reading practice. An ablation study demonstrates how our method of encoding educator expertise into the question generation pipeline can produce high-quality output; and through a user study with 12 parent-child dyads (child age: 4–6), we demonstrate that this system can serve as a guide for parents in leading contextually meaningful dialogue, leading to significantly more conversational turns from both the parent and the child and deeper conversations with connections to the child’s everyday life.

Abstract With the growing use of temporal logics in areas ranging from robot planning to runtime verification, it is critical that users have a clear understanding of what a specification means. Toward this end, we have been developing a catalog of semantic errors and a suite of test instruments targeting various user-groups. The catalog is of interest to educators, to logic designers, to formula authors, and to tool builders, e.g., to identify mistakes. The test instruments are suitable for classroom teaching or self-study. This paper reports on five sets of survey data collected over a three-year span. We study misconceptions about finite-trace $$\textsc {ltl}_{f}$$ L T L f in three ltl-aware audiences, and misconceptions about standard ltl in novices. We find several mistakes, even among experts. In addition, the data supports several categories of errors in both $$\textsc {ltl}_{f}$$ L T L f and ltl that have not been identified in prior work. These findings, based on data from actual users, offer insights into what specific ways temporal logics are tricky and provide a groundwork for future interventions.

This paper presents the design of Forge , a tool for teaching formal methods gradually. Forge is based on the widely-used Alloy language and analysis tool, but contains numerous improvements based on more than a decade of experience teaching Alloy to students. Although our focus has been on the classroom, many of the ideas in Forge likely also apply to training in industry. Forge offers a progression of languages that improve the learning experience by only gradually increasing in expressive power. Forge supports custom visualization of its outputs, enabling the use of widely-understood domain-specific representations. Finally, Forge provides a variety of testing features to ease the transition from programming to formal modeling. We present the motivation for and design of these aspects of Forge, and then provide a substantial evaluation based on multiple years of classroom use.

Deploying Machine Learning (ML) algorithms within databases is a challenge due to the varied computational footprints of modern ML algorithms and the myriad of database technologies each with their own restrictive syntax. We introduce an Apache Spark-based micro-service orchestration framework that extends database operations to include web service primitives. Our system can orchestrate web services across hundreds of machines and takes full advantage of cluster, thread, and asynchronous parallelism. Using this framework, we provide large scale clients for intelligent services such as speech, vision, search, anomaly detection, and text analysis. This allows users to integrate ready-to-use intelligence into any datastore with an Apache Spark connector. To eliminate the majority of overhead from network communication, we also introduce a low-latency containerized version of our architecture. Finally, we demonstrate that the services we investigate are competitive on a variety of benchmarks, and present two applications of this framework to create intelligent search engines, and real time auto race analytics systems.