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.

Compiler diagnostics for type inference failures are notoriously bad, and type classes only make the problem worse. By introducing a complex search process during inference, type classes can lead to wholly inscrutable or useless errors. We describe a system, Argus , for interactively visualizing type class inferences to help programmers debug inference failures, applied specifically to Rust’s trait system. The core insight of Argus is to avoid the traditional model of compiler diagnostics as one-size-fits-all, instead providing the programmer with different views on the search tree corresponding to different debugging goals. Argus carefully uses defaults to improve debugging productivity, including interface design (e.g., not showing full paths of types by default) and heuristics (e.g., sorting obligations based on the expected complexity of fixing them). We evaluated Argus in a user study where N = 25 participants debugged type inference failures in realistic Rust programs, finding that participants using Argus correctly localized 2.2× as many faults and localized 3.3× faster compared to not using Argus .

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.

Problem planning is a fundamental programming skill, and aids students in decomposing tasks into manageable subtasks. While feedback on plans is beneficial for beginners, providing this in a scalable and timely way is an enormous challenge in large courses.

Program planning is the process of splitting a problem description into subtasks that can be solved independently, then composed into a solution. While much has been written about planning since the 1980s, little research looks at modern contexts such as programs to process data tables. Tool support for this sort of planning is even rarer. As part of a project to develop such tools, we have run two studies to try to identify steps, representations, and interactions that would support novice university students in planning and programming multi-task programs that process data tables. This experience report describes our observations so far, while also raising questions about how to make planning useful for students.

Passive documents and active programs now widely comingle. Document languages include Turing-complete programming elements, and programming languages include sophisticated document notations. However, there are no formal foundations that model these languages. This matters because the interaction between document and program can be subtle and error-prone. In this paper we describe several such problems, then taxonomize and formalize document languages as levels of a document calculus. We employ the calculus as a foundation for implementing complex features such as reactivity, as well as for proving theorems about the boundary of content and computation. We intend for the document calculus to provide a theoretical basis for new document languages, and to assist designers in cleaning up the unsavory corners of existing languages.

This paper documents a year-long experiment to “profile” the process of learning a programming language: gathering data to understand what makes a language hard to learn, and using that data to improve the learning process. We added interactive quizzes to The Rust Programming Language, the official textbook for learning Rust. Over 13 months, 62,526 readers answered questions 1,140,202 times. First, we analyze the trajectories of readers. We find that many readers drop-out of the book early when faced with difficult language concepts like Rust’s ownership types. Second, we use classical test theory and item response theory to analyze the characteristics of quiz questions. We find that better questions are more conceptual in nature, such as asking why a program does not compile vs. whether a program compiles. Third, we performed 12 interventions into the book to help readers with difficult questions. We find that on average, interventions improved quiz scores on the targeted questions by +20

Misconceptions about core linguistic concepts like mutable variables, mutable compound data, and their interaction with scope and higher-order functions seem to be widespread. But how do we detect them, given that experts have blind spots and may not realize the myriad ways in which students can misunderstand programs? Furthermore, once identified, what can we do to correct them? In this paper, we present a curated list of misconceptions, and an instrument to detect them. These are distilled from student work over several years and match and extend prior research. We also present an automated, self-guided tutoring system. The tutor builds on strategies in the education literature and is explicitly designed around identifying and correcting misconceptions. We have tested the tutor in multiple settings. Our data consistently show that (a) the misconceptions we tackle are widespread, and (b) the tutor appears to improve understanding.

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.

Programmers learning Rust struggle to understand ownership types, Rust’s core mechanism for ensuring memory safety without garbage collection. This paper describes our attempt to systematically design a pedagogy for ownership types. First, we studied Rust developers’ misconceptions of ownership to create the Ownership Inventory, a new instrument for measuring a person’s knowledge of ownership. We found that Rust learners could not connect Rust’s static and dynamic semantics, such as determining why an ill-typed program would (or would not) exhibit undefined behavior. Second, we created a conceptual model of Rust’s semantics that explains borrow checking in terms of flow-sensitive permissions on paths into memory. Third, we implemented a Rust compiler plugin that visualizes programs under the model. Fourth, we integrated the permissions model and visualizations into a broader pedagogy of ownership by writing a new ownership chapter for The Rust Programming Language , a popular Rust textbook. Fifth, we evaluated an initial deployment of our pedagogy against the original version, using reader responses to the Ownership Inventory as a point of comparison. Thus far, the new pedagogy has improved learner scores on the Ownership Inventory by an average of 9

When novice programming students already know one programming language and have to learn another, what issues do they run into? We specifically focus on one or both languages being functional, varying along two axes: syntax and semantics. We report on problems, especially persistent ones. This work can be of immediate value to educators and also sets up avenues for future research.

Background and Context.

Background and Context. Program planning has been a long-standing and important problem in computing education. Finding useful primitives for planning and assessing whether students are able to understand and use these primitives remain open problems. We make progress on this problem by using higher-order functions (hofs) as planning operations. Not only are hofs increasingly prevalent in computing broadly, some data science programming sources also recommend their use in planning solutions to data-processing pipelines, giving our task additional applicability.

We propose that secondary-school data-science curricula should be based on four key ingredients: two are technical (programming and statistics, with visualization sitting at their intersection), while two are human-facing (meaningful domains, and civic responsibility). We describe their relationship and argue for their importance.

Model-finders, such as SAT/SMT-solvers and Alloy, are used widely both directly and embedded in domain-specific tools. They support both conventional verification and, unlike other verification tools, property-free exploration. To do this effectively, they must produce output that helps users with these tasks. Unfortunately, the output of model-finders has seen relatively little rigorous human-factors study. Conventionally, these tools tend to show one satisfying instance at a time. Drawing inspiration from the cognitive science literature, we investigate two aspects of model-finder output: how many instances to show at once, and whether all instances must actually satisfy the input constraints. Using both controlled studies and open-ended talk-alouds, we show that there is benefit to showing negative instances in certain settings; the impact of multiple instances is less clear. Our work is a first step in a theoretically grounded approach to understanding how users engage cognitively with model-finder output, and how those tools might better support users in doing so.

In teaching students to program with compositions of higher-order functions, we have encountered a sharp distinction in the difficulty of problems as perceived by students. This distinction especially matters as growing numbers of programmers learn about functional programming for data processing. We have made initial progress on identifying this distinction, which appears counter-intuitive to some. We describe the phenomenon, provide some preliminary evidence of the difference in difficulty, and suggest consequences for functional programming pedagogy.

Motivation. Higher-order functions are a standard and increasingly central component in many kinds of modern programming, including data science and Web development. Yet little research has been devoted to student learning or understanding of this topic.

Motivation. “Adversarial thinking” (at) is viewed as a central idea in cybersecurity. We believe a similar idea carries over into other critical areas as well, such as understanding the perils of social networks and machine learning.

Integrating computing into other subjects promises to address many challenges to offering standalone CS courses in K-12 contexts. Integrated curricula must be designed carefully, however, to both meet learning objectives of the host discipline and to gain traction with teachers. We describe the multi-year evolution of Bootstrap, a curriculum for integrating computing into middle- and high-school mathematics. We discuss the initial design and the various modifications we have made over the years to better support math instruction, leading to our goal of using integrated curricula to cover standards in both math and CS. We provide advice for others aiming for integration and raise questions for CS educators about how we might better support learning in other disciplines.

We recently renamed our “education” track’s papers from Education Pearl to Education Matters. This would be a good time to explain our vision for the track as a whole, as well as this specific renaming.

Configuring a service mesh often involves multiple parties, each of whom is responsible for separate portions of the overall system. This can result in miscommunication, silent and sudden errors, or a failure to meet goals.

Data that correspond to real-world scenarios can often be organized in several different ways in a database or program. Appreciating the differences between them and choosing an organization that addresses a system's needs are valuable and necessary computing skills. Unfortunately, little of the computing-education literature seems to deal with this topic.

In many universities, Teaching Assistants (TAs) are an important part of students' educational experience. This is especially true in early courses, where students may suffer from inexperience and anxiety, and find fellow students more accessible than professors.

Flawed problem comprehension leads students to produce flawed implementations. However, testing alone is inadequate for checking comprehension: if a student develops both their tests and implementation with the same misunderstanding, running their tests against their implementation will not reveal the issue. As a solution, some pedagogies encourage the creation of input-output examples independent of testing-but seldom provide students with any mechanism to check that their examples are correct and thorough.

Generating questions to engage and measure students is often challenging and time-consuming. Furthermore, these questions do not always transfer well between student populations due to differences in background, course emphasis, or ambiguity in the questions or answers. We introduce a contributing student pedagogy activity facilitated by machine learning that can generate questions with associated answer-reasoning sets. We call this process Adaptive Tool-Driven Conception Generation. A tool implementing this process has been deployed, and it explicitly optimizes the process for questions that divide student opinion. In a study involving arrays in Java, this novel process: generates questions similar to expert-designed questions, produces novel questions that identify potential student misconceptions, and provides statistical estimates of the prevalence of misconceptions. This process allows the generation of quiz and discussion questions with less expert effort, facilitates a subprocess in the creation of concept inventories, and also raises the possibility of running reproduction studies relatively cheaply.

Most programmers rely on visual tools (block-based editors, auto-indentation, bracket matching, syntax highlighting, etc.), which are inaccessible to visually-impaired programmers. While prior language-specific, downloadable tools have demonstrated benefits for the visually-impaired, we lack language-independent, cloud-based tools, both of which are critically needed. We present a new toolkit for building fully-accessible, browser-based programming environments for multiple languages. Given a parser that meets certain specifications, this toolkit will generate a block editor familiar to sighted users that also communicates the structure of a program using spoken descriptions, and allows for navigation using standard (accessible) keyboard shortcuts.

There are several different gradual typing semantics, reflecting different trade-offs between performance and type soundness guarantees. Notably absent, however, are any data on which of these semantics developers actually prefer.

Instructors routinely use automated assessment methods to evaluate the semantic qualities of student implementations and, sometimes, test suites. In this work, we distill a variety of automated assessment methods in the literature down to a pair of assessment models. We identify pathological assessment outcomes in each model that point to underlying methodological flaws. These theoretical flaws broadly threaten the validity of the techniques, and we actually observe them in multiple assignments of an introductory programming course. We propose adjustments that remedy these flaws and then demonstrate, on these same assignments, that our interventions improve the accuracy of assessment. We believe that with these adjustments, instructors can greatly improve the accuracy of automated assessment.

Scores of compilers produce JavaScript, enabling programmers to use many languages on the Web, reuse existing code, and even use Web IDEs. Unfortunately, most compilers inherit the browser's compromised execution model, so long-running programs freeze the browser tab, infinite loops crash IDEs, and so on. The few compilers that avoid these problems suffer poor performance and are difficult to engineer.

Type systems and syntactic sugar are both valuable to programmers, but sometimes at odds. While sugar is a valuable mechanism for implementing realistic languages, the expansion process obscures program source structure. As a result, type errors can reference terms the programmers did not write (and even constructs they do not know), baffling them. The language developer must also manually construct type rules for the sugars, to give a typed account of the surface language. We address these problems by presenting a process for automatically reconstructing type rules for the surface language using rules for the core. We have implemented this theory, and show several interesting case studies.

Data Science is at the center of many current curricular efforts. It is emerging as an integrated field that has far-reaching and important applications, from news media to policy making to business. While these applications can provide compelling uses of computer science techniques, an introduction to one is not an introduction to the other. How do topics like data structures and program design emerge from data science applications? How do we transition from data science applications to computer science topics? How can data science be integrated into other contexts with little overhead? This workshop presents assignments and curricula designed to answer these questions, and tools that support them.

Bootstrap:Algebra is a curricular module designed to integrate introductory computing into an algebra class; the module aims to help students improve on various essential learning outcomes from state and national algebra standards. In prior work, we published initial findings about student performance gains on algebra problems after taking Bootstrap. While the results were promising, the dataset was not large, and had students working on algebra problems that had been scaffolded with Bootstrap's pedagogy. This paper reports on a more detailed study with (a) data from more than three times as many students, (b) analysis of performance changes in incorrect answers, (c) some problems in which the Bootstrap scaffolds have been removed, and (d) an IRT analysis across the elements of Bootstrap's program-design pedagogy. Our results confirm that students improve on algebraic word problems after completing the module, even on unscaffolded problems. The nature of incorrect answers to symbolic-form questions also appears to improve after Bootstrap.

Game programming projects are concrete and motivational for students, especially when used to teach more abstract concepts such as algebra. These projects must have open-ended elements to allow for creativity, but too much freedom makes it hard to reach specific learning outcomes. How many degrees of freedom do students need to make a game feel like one they genuinely designed? What kinds of personalization do they undertake of their games? And how do these factors correlate with their prior game-playing experience or with their identified gender? This paper studies these questions in the concrete setting of the Bootstrap:Algebra curriculum. In this curriculum, students are only given four parameters they can customize and only a few minutes in which to do so. Our study shows that despite this very limited personalization, students still feel a strong sense of ownership, originality, and pride in their creations. We also find that females find videogame creation just as satisfying as males, which contradicts some prior research but may also reflect the nature of games created in this curriculum and the opportunities it offers for self-expression.

We evaluate a notional machine for recursion based on algebraic substitution. To do this, we decompose recursion into a progression of function call patterns, parameter name reuse, and data structure complexity. At each stage, we test students' ability to trace programs using substitution. We evaluate the correctness of their traces along multiple dimensions, finding that students generally do well, and also observe shortcuts and identify misconceptions. For comparison, we also have students trace two problems using a traditional, imperative notional machine. Even though the substitution model is unwieldy to use with compound data, students still perform better with it than with the traditional notional machine.

Scope, aliasing, mutation, and parameter passing are fundamental programming concepts that interact in subtle ways, especially in complex programs. Research has shown that students have substantial misconceptions on these topics. But this research has been done largely in CS1 courses, when students' programming experience is limited and problems are necessarily simple. What happens later in the curriculum? Does more programming experience iron out these misconceptions naturally, or are interventions required?

Scenario-finding tools like the Alloy Analyzer are widely used in numerous concrete domains like security, network analysis, UML analysis, and so on. They can help to verify properties and, more generally, aid in exploring a system's behavior.

Many languages use syntactic sugar to define parts of their surface language in terms of a smaller core. Thus some properties of the surface language, like its scoping rules , are not immediately evident. Nevertheless, IDEs, refactorers, and other tools that traffic in source code depend on these rules to present information to users and to soundly perform their operations. In this paper, we show how to lift scoping rules defined on a core language to rules on the surface, a process of scope inference . In the process we introduce a new representation of binding structure---scope as a preorder---and present a theoretical advance: proving that a desugaring system preserves α-equivalence even though scoping rules have been provided only for the core language. We have also implemented the system presented in this paper.

Testing and debugging networks /in situ/ is notoriously difficult. Many vital correctness properties involve histories over multiple packets (e.g., prior established connections). Checking such properties requires /cross-packet state/, which cannot be fully captured on stateless switch hardware.

Plan composition is an important but under-studied topic in programming education. Most studies were done three decades ago, under assumptions that miss important issues that today's students must confront. This paper presents rationale and details for a modernized study of plan composition that accommodates a broader range of programming languages and problem features. Our study design has two novelties: the problems require students to deal with data-processing challenges (such as noisy data), and the questions ask students to not only produce but also evaluate programs. We present preliminary results from using our study in multiple courses from different linguistic paradigms. We discuss several future studies that are prompted by these results.

In in-flow peer review, students provide feedback to one another on intermediate artifacts on their way to a final submission. Prior work has studied examples and tests as a potentially useful initial artifact for review. Unfortunately, large test suites are onerous to produce and especially to review. We instead propose the notion of a sweep, an artificially constrained set of tests that illustrates common and interesting behavior. We present experimental data across several courses that show that sweeps have reasonable quality, and are also a good target for peer review; for example, students usually (over half the time) suggest new tests to one another in a review.

Syntactic sugar is widely used in language implementation. Its benefits are, however, offset by the comprehension problems it presents to programmers once their program has been transformed. In particular, after a transformed program has begun to evaluate (or otherwise be altered by a black-box process), it can become unrecognizable. We present a new approach to _resugaring_ programs, which is the act of reflecting evaluation steps in the core language in terms of the syntactic sugar that the programmer used. Relative to prior work, our approach has two important advances: it handles hygiene, and it allows almost arbitrary rewriting rules (as opposed to restricted patterns). We do this in the context of a DAG representation of programs, rather than more traditional trees.

Many APIs enable cross-platform system development by abstracting over the details of a platform, allowing application developers to write one implementation that will run on a wide variety of platforms. Unfortunately, subtle differences in the behavior of the underlying platforms make cross-platform behavior difficult to achieve. As a result, applications using these APIs can be plagued by bugs difficult to observe before deployment. These portability bugs can be particularly difficult to diagnose and fix because they arise from the API implementation, the operating system, or hardware, rather than application code. This paper describes CheckAPI, a technique for detecting violations of cross-platform portability. CheckAPI compares an application's interactions with the API implementation to its interactions with a partial specification-based API implementation, and does so efficiently enough to be used in real production systems and at runtime. CheckAPI finds latent errors that escape pre-release testing. This paper discusses the subtleties of different kinds of API calls and strategies for effectively producing the partial implementations. Validating CheckAPI on JavaScript, the Seattle project's Repy VM, and POSIX detects dozens of violations that are confirmed bugs in widely-used software.

Desugaring, a key form of program manipulation, is a vital tool in the practical study of programming languages. Its use enables pragmatic solutions to the messy problems of dealing with real languages, but it also introduces problems that need addressing. By listing some of these challenges, this paper and talk aim to serve as a call to arms to the community to give the topic more attention.

Many educators have tried to leverage computing or programming to help improve students' achievement in mathematics. However, several hopes of performance gains---particularly in algebra---have come up short. In part, these efforts fail to align the computing and mathematical concepts at the level of detail typically required to achieve transfer of learning. This paper describes Bootstrap, an early-programming curriculum that is designed to teach key algebra topics as students build their own videogames. We discuss the curriculum, explain how it aligns with algebra, and present initial data showing student performance gains on standard algebra problems after completing Bootstrap.

Test-first development and peer review have been studied independently in computing courses, but their combination has not. We report on an experiment in which students in two courses conducted peer review of test suites while assignments were in progress. We find strong correlation between review ratings and staff-assessed work quality, as well as evidence that test suites improved during the review process. Student feedback suggests that reviewing had some causal impact on these improvements. We describe several lessons learned about administering and assessing peer-review within test-first development.

Peer review is effective for teaching students to evaluate approaches to problems, fostering collaboration, and assessing other students' work. Peer review often happens after assignments are turned in, on complete artifacts that other students have created. We've been experimenting with a different style of peer review, which we call in-flow reviewing, in which programming assignments are broken into reviewable stages. After students complete each stage they review one anothers' work, allowing for feedback early on in the assignment. We've built a system, dubbed Captain Teach, for exploring in-flow reviewing for both programming and written assignments. In our demonstration and tutorial, we will show what the student experience looks like for a Captain Teach assignment, explain the interface that instructors have for creating assignments in Captain Teach, outline some of the mechanisms for anonymously assigning reviews and distributing feedback, and discuss future directions for the tool.

Computing educators have used peer review in various ways in courses at many levels. Few of these efforts have applied peer review to multiple deliverables (such as specifications, tests, and code) within the same programming problem, or to assignments that are still in progress (as opposed to completed). This paper describes CaptainTeach, a programming environment enhanced with peer-review capabilities at multiple stages within assignments in progress. Multi-stage, in-flow peer review raises many logistical and pedagogical issues. This paper describes CaptainTeach and our experience using it in two undergraduate courses (one first-year and one upper-level); our analysis emphasizes issues that arise from the conjunction of multiple stages and in-flow reviewing, rather than peer review in general.

Syntactic sugar is pervasive in language technology. It is used to shrink the size of a core language; to define domain-specific languages; and even to let programmers extend their language. Unfortunately, syntactic sugar is eliminated by transformation, so the resulting programs become unfamiliar to authors. Thus, it comes at a price: it obscures the relationship between the user's source program and the program being evaluated.

Web pages routinely incorporate JavaScript code from third-party sources. However, all code in a page runs in the same security context, regardless of provenance. When Web pages incorporate third-party JavaScript without any checks, as many do, they open themselves to attack. A third-party can triv ially inject malicious JavaScript into such a page, causing all manner of harm. Several such attacks have occurred in the wild on prominent, commercial Web sites. A Web sandbox mitigates the threat of malicious JavaScript. Several Web sandboxes employ closely related language-based techniques to maintain backward-compatibility with old browsers and to provide fine-grained control. Unfortunately, due to the size and complexity of the Web platform and several subtleties of JavaScript, language-based sandboxing is hard and the Web sandboxes currently deployed on major Web sites do not come with any formal guarantees. Instead, they are routinely affected by bugs that violate their intended sandboxing properties. This article presents a type-based approach to verifying Web sandboxes, using a JavaScript type-checker to encode and verify sandboxing properties. We demonstrate our approach by applying it to the ADsafe Web sandbox. Specifically, we verify several key properties of ADsafe, falsify one intended property, and find and fix several vulnerabilities, ultimately providing a proof of ADsafe's safety.

JavaScript programs vary widely in functionality, complexity, and use, and analyses of these programs must accommodate such variations. Type-based analyses are typically the simplest such analyses, but due to the language's subtle idioms and many application-specific needs---such as ensuring general-purpose type correctness, security properties, or proper library usage---we have found that a single type system does not suffice for all purposes. However, these varied uses still share many reusable common elements.

JavaScript is the language of the ubiquitous Web, but it only poorly supports event-driven functional programs due to its single-threaded, asynchronous nature and lack of rich control flow operators. We present Whalesong, a compiler from Racket that generates JavaScript code that masks these problems. We discuss the implementation strategy using delimited continuations, an interface to the DOM, and an FFI for adapting JavaScript libraries to add new platform-dependent reactive features. In the process, we also describe extensions to Racket's functional event-driven programming model. We also briefly discuss the implementation details.

Scenario-finding tools such as Alloy are widely used to understand the consequences of specifications, with applications to software modeling, security analysis, and verification. This paper focuses on the exploration of scenarios: which scenarios are presented first, and how to traverse them in a well-defined way. We present Aluminum, a modification of Alloy that presents only minimal scenarios: those that contain no more than is necessary. Aluminum lets users explore the scenario space by adding to scenarios and backtracking. It also provides the ability to find what can consistently be used to extend each scenario. We describe the semantic basis of Aluminum in terms of minimal models of first-order logic formulas. We show how this theory can be implemented atop existing SAT-solvers and quantify both the benefits of minimality and its small computational overhead. Finally, we offer some qualitative observations about scenario exploration in Aluminum.

We present a small-step operational semantics for the Python programming language. We present both a core language for Python, suitable for tools and proofs, and a translation process for converting Python source to this core. We have tested the composition of translation and evaluation of the core for conformance with the primary Python implementation, thereby giving confidence in the fidelity of the semantics. We briefly report on the engineering of these components. Finally, we examine subtle aspects of the language, identifying scope as a pervasive concern that even impacts features that might be considered orthogonal.

No abstract available.

We present the design, implementation, and evaluation of an API for applications to control a software-defined network (SDN). Our API is implemented by an OpenFlow controller that delegates read and write authority from the network's administrators to end users, or applications and devices acting on their behalf. Users can then work with the network, rather than around it, to achieve better performance, security, or predictable behavior. Our API serves well as the next layer atop current SDN stacks. Our design addresses the two key challenges: how to safely decompose control and visibility of the network, and how to resolve conflicts between untrusted users and across requests, while maintaining baseline levels of fairness and security. Using a real OpenFlow testbed, we demonstrate our API's feasibility through microbenchmarks, and its usefulness by experiments with four real applications modified to take advantage of it.

Given the widespread use of memory-safe languages, students must understand garbage collection well. Following a constructivist philosophy, an effective approach would be to have them implement garbage collectors. Unfortunately, a full implementation depends on substantial knowledge of compilers and runtime systems, which many courses do not cover or cannot assume.

We present S5, a semantics for the strict mode of the ECMAScript 5.1 (JavaScript) programming language. S5 shrinks the large source language into a manageable core through an implemented transformation. The resulting specification has been tested against real-world conformance suites for the language. This paper focuses on two aspects of S5: accessors (getters and setters) and eval. Since these features are complex and subtle in JavaScript, they warrant special study. Variations on both features are found in several other programming languages, so their study is likely to have broad applicability.

We performed a study of Facebook users to examine how they coped with limitations of the Facebook privacy settings interface. Students graduating and joining the workforce create significant problems for all but the most basic privacy settings on social networking websites. We therefore created realistic scenarios exploiting work/play boundaries that required users to specify access control policies that were impossible due to various limitations. We examined whether users were aware of these problems without being prompted, and once given feedback, what their coping strategies were. Overall, we found that simply alerting participants to potential errors was ineffective, but when choices were also presented, participants introduced significantly fewer errors. Based on our findings, we designed a privacy settings interface based on Venn diagrams, which we validated with a usability study. We conclude that this interface may be more effective than the current privacy settings interface.

We posit that functional programmers employ a notion called expression integrity to understand programs. We attempt to study the extent to which both novices and experts use this notion as they program, discuss the difficulties that arise in measuring this, and offer some observational findings.

We present a programming environment called WeScheme that runs in the Web browser and supports interactive development. WeScheme programmers can save programs directly on the Web, making them accessible from everywhere. As a result, sharing of programs is a central focus that WeScheme supports seamlessly. The environment also leverages the existing presentation media and program run-time support found in Web browsers, thus making these easily accessible to students and leveraging their rapid engineering improvements. WeScheme is being used successfully by students, and is especially valuable in schools that have prohibitions on installing new software or lack the computational demands of more intensive programming environments.

Good error messages are critical for novice programmers. Re-cognizing this, the DrRacket programming environment provides a series of pedagogically-inspired language subsets with error messages customized to each subset. We apply human-factors research methods to explore the effectiveness of these messages. Unlike existing work in this area, we study messages at a fine-grained level by analyzing the edits students make in response to various classes of errors. We present a rubric (which is not language specific) to evaluate student responses, apply it to a course-worth of student lab work, and describe what we have learned about using the rubric effectively. We also discuss some concrete observations on the effectiveness of these messages.

Policy authors typically reconcile several different mental models and goals, such as enabling collaboration, securing information, and conveying trust in colleagues. The data underlying these models, such as which roles are more trusted than others, isn't generally used to define policy rules. As a result, policy-management environments don't gather this information; in turn, they fail to exploit it to help users check policy decisions against their multiple perspectives. We present a model of triangulating authoring environments that capture the data underlying these different perspectives, and iteratively sanity-check policy decisions against this information while editing. We also present a tool that consumes instances of the model and automatically generates prototype authoring tools for the described domain.

Functional programming languages ought to play a central role in mathematics education for middle schools (age range: 10-14). After all, functional programming is a form of algebra and programming is a creative activity about problem solving. Introducing it into mathematics courses would make pre-algebra course come alive. If input and output were invisible, students could implement fun simulations, animations, and even interactive and distributed games all while using nothing more than plain mathematics. We have implemented this vision with a simple framework for purely functional I/O. Using this framework, students design, implement, and test plain mathematical functions over numbers, booleans, string, and images. Then the framework wires them up to devices and performs all the translation from external information to internal data (and vice versa)--just like every other operating system. Once middle school students are hooked on this form of programming, our curriculum provides a smooth path for them from pre-algebra to freshman courses in college on object-oriented design and theorem proving.

This paper presents Flapjax, a language designed for contemporary Web applications. These applications communicate with servers and have rich, interactive interfaces. Flapjax provides two key features that simplify writing these applications. First, it provides event streams, a uniform abstraction for communication within a program as well as with external Web services. Second, the language itself is reactive: it automatically tracks data dependencies and propagates updates along those dataflows. This allows developers to write reactive interfaces in a declarative and compositional style.

We present a preference aggregation algorithm designed for situations in which a limited number of users each review a small subset of a large (but finite) set of candidates. This algorithm aggregates scores by using users' relative preferences to search for a Kemeny-optimal ordering of items, and then uses this ordering to identify good and bad items, as well as those that are the subject of reviewer conflict. The algorithm uses variable-neighborhood local search, allowing the efficient discovery of high-quality consensus orderings while remaining computationally feasible. It provides a significant increase in solution quality over existing systems. We discuss potential applications of this algorithm in group recommender systems for a variety of scenarios, including program committees and faculty searches.

No abstract available.

We present a static control-flow analysis for JavaScript programs running in a web browser. Our analysis tackles numerous challenges posed by modern web applications including asynchronous communication, frameworks, and dynamic code generation. We use our analysis to extract a model of expected client behavior as seen from the server, and build an intrusion-prevention proxy for the server: the proxy intercepts client requests and disables those that do not meet the expected behavior. We insert random asynchronous requests to foil mimicry attacks. Finally, we evaluate our technique against several real applications and show that it protects against an attack in a widely-used web application.

Alloy specifications are used to define lightweight models of systems. We present Alchemy, which compiles Alloy specifications into implementations that execute against persistent databases. Alchemy translates a subset of Alloy predicates into imperative update operations, and it converts facts into database integrity constraints that it maintains automatically in the face of these imperative actions.

The analogy between types and contracts raises the question of how many features of static type systems can be expressed as dynamic contracts. An important feature missing in prior work on contracts is parametricity, as represented by the polymorphic types in languages like Standard ML.

Functional Reactive Programming (FRP) extends traditional functional programming with dataflow evaluation, making it possible to write interactive programs in a declarative style. An FRP language creates a dynamic graph of data dependencies and reacts to changes by propagating updates through the graph. In a transparent FRP language, the primitive operators are implicitly lifted, so they construct graph nodes when they are applied to time-varying values. This model has some attractive properties, but it tends to produce a large graph that is costly to maintain. In this paper, we develop a transformation we call lowering, which improves performance by reducing the size of the graph. We present a static analysis that guides the sound application of this optimization, and we present benchmark results that demonstrate dramatic improvements in both speed and memory usage for real programs.

Cryptographic protocols are useful for trust engineering in Web transactions. The Cryptographic Protocol Programming Language (CPPL) provides a model wherein trust management annotations are attached to protocol actions, and are used to constrain the behavior of a protocol participant to be compatible with its own trust policy.

Programs are increasingly organized around features, which are encapsulated using aspects and other linguistic mechanisms. Despite their growing popularity amongst developers, there is a dearth of techniques for computer-aided verification of programs that employ these mechanisms. We present the theoretical underpinnings for applying model checking to programs (expressed as state machines) written using these mechanisms. The analysis is incremental, examining only components that change rather than verifying the entire system every time one part of it changes. Our technique assumes that the set of pointcut designators is known statically, but the actual advice can vary. It handles both static and dynamic pointcut designators. We present the algorithm, prove it sound, and address several subtleties that arise, including cascading advice application and problems of circular reasoning.

The growing importance of access control has led to the definition of numerous languages for specifying policies. Since these languages are based on different foundations, language users and designers would benefit from formal means to compare them. We present a set of properties that examine the behavior of policies under enlarged requests, policy growth, and policy decomposition. They therefore suggest whether policies written in these languages are easier or harder to reason about under various circumstances. We then evaluate multiple policy languages, including XACML and Lithium, using these properties.

As GPU-powered special effects become more sophisticated, it becomes harder to create and manage effect interaction using the fairly primitive shading languages. This difficulty also introduces a workflow problem: artists design effects but only programmers can implement them, making it impossible for them to work asynchronously.To address these problems we present abstract shade trees and heuristic algorithms that operate over them. The trees allow designers to easily create effects by connecting primitives such as cube mapping and modulation. These primitives publish semantically rich types that encapsulate notions like vector basis and normalization. The algorithms employ these published types to automatically infer atomic and compound connectors between the primitives, and generate code for the tree. We also describe a visual editing environment for specifying the trees.Our data structure and algorithms spare designers from having to specify low-level programming details, enabling them to experiment without depending on programmers. The algorithms ensure that the generated code will be free of type-mismatches, a problem in previous shade trees. The abstract shade tree can also naturally express high-level features like shadows and reflections whose implementations overlap; that cross-cutting has made them difficult to modularize in more traditional ways. In experiments, the generated shaders are as efficient as handwritten code.

Lisp programmers have long used macros to extend their language. Indeed, their success has inspired macro notations for a variety of other languages, such as C and Java. There is, however, a paucity of effective pedagogic examples of macro use. This paper presents a short, non-trivial example that implements a construct not already found in mainstream languages. Furthermore, it motivates the need for tail-calls, as opposed to mere tail-recursion, and illustrates how support for tail-call optimization is crucial to support a natural style of macro-based language extension.

Implementing first-class continuations can pose a challenge if the target machine makes no provisions for accessing and re-installing the run-time stack. In this paper, we present a novel translation that overcomes this problem. In the first half of the paper, we introduce a theoretical model that shows how to eliminate the capture and the use of first-class continuations in the presence of a generalized stack inspection mechanism. The second half of the paper explains how to translate this model into practice in two different contexts. First, we reformulate the servlet interaction language in the PLT Web server, which heavily relies on first-class continuations. Using our technique, servlet programs can be run directly under the control of non-cooperative web servers such as Apache. Second, we show how to use our new technique to copy and reconstitute the stack on MSIL.Net using exception handlers. This establishes that Scheme's first-class continuations can exist on non-cooperative virtual machines.

Sensitive data are increasingly available on-line through the Web and other distributed protocols. This heightens the need to carefully control access to data. Control means not only preventing the leakage of data but also permitting access to necessary information. Indeed, the same datum is often treated differently depending on context.System designers create policies to express conditions on the access to data. To reduce source clutter and improve maintenance, developers increasingly use domain-specific, declarative languages to express these policies. In turn, administrators need to analyze policies relative to properties, and to understand the effect of policy changes even in the absence of properties.This paper presents Margrave, a software suite for analyzing role-based access-control policies. Margrave includes a verifier that analyzes policies written in the XACML language, translating them into a form of decision-diagram to answer queries. It also provides semantic differencing information between versions of policies. We have implemented these techniques and applied them to policies from a working software application.

Financial companies, engineering firms and even scientists create increasingly larger spreadsheets and spreadsheet programs. The creators of large spreadsheets make errors and must track them down. One common class of errors concerns unit errors, because spreadsheets often employ formulas with physical or monetary units. In this paper, we describe XeLda, our tool for unit checking Excel spreadsheets. The tool highlights cells if their formulas process values with incorrect units and if derived units clash with unit annotations. In addition, it draws arrows to the sources of the formulas for debugging. The tool is sensitive to many of the intricacies of Excel spreadsheets including tables, matrices, and even circular references. Using XeLda, we have detected errors in some published scientific spreadsheets.

Aspect-oriented programming has become an increasingly important means of expressing cross-cutting program abstractions. Despite this, aspects lack support for computer-aided verification. We present a technique for verifying aspect-oriented programs (expressed as state machines). Our technique assumes that the set of pointcut designators is known statically, but that the actual advice can vary. This calls for a modular technique that does not require repeated analysis of the entire system every time a developer changes advice. We present such an analysis, addressing several subtleties that arise. We also present an important optimization for handling multiple pointcut designators. We have implemented a prototype verifier and applied it to some simple but interesting cases.

Twenty years ago Abelson and Sussman's Structure and Interpretation of Computer Programs radically changed the intellectual landscape of introductory computing courses. Instead of teaching some currently fashionable programming language, it employed Scheme and functional programming to teach important ideas. Introductory courses based on the book showed up around the world and made Scheme and functional programming popular. Unfortunately, these courses quickly disappeared again due to shortcomings of the book and the whimsies of Scheme. Worse, the experiment left people with a bad impression of Scheme and functional programming in general. In this pearl, we propose an alternative role for functional programming in the first-year curriculum. Specifically, we present a framework for discussing the first-year curriculum and, based on it, the design rationale for our book and course, dubbed How to Design Programs . The approach emphasizes the systematic design of programs. Experience shows that it works extremely well as a preparation for a course on object-oriented programming.

We are building a software development environment that uses constraints to ensure the consistency of the different artifacts associated with software. This approach to software development makes the environment responsible for detecting most inconsistencies between software design, specifications, documentation, source code, and test cases. The environment provides facilities to ensure that these various dimensions remain consistent as the software is written and evolves. The environment works with the wide variety of artifacts typically associated with a large software system. It handles both the static and dynamic aspects of software. Moreover, it works incrementally so that consistency information is readily available to the developer as the system changes. The demonstration will show this environment and its capabilities.

We describe a methodology for detecting user errors in spreadsheets, using the notion of units as our basic elements of checking. We define the concept of a header and discuss two types of relationships between headers, namely is-a and has-a relationships. With these, we develop a set of rules to assign units to cells in the spreadsheet. We check for errors by ensuring that every cell has a well-formed unit. We describe an implementation of the system that allows the user to check Microsoft Excel spreadsheets. We have run our system on practical examples, and even found errors in published spreadsheets.

As programs evolve, their code increasingly becomes tangled by programmers and requirements. This mosaic quality complicated program comprehension and maintenance. Many of these activities can benefit from viewing the program as a collection of features. We introduce an inexpensive and easily comprehensible summary of program changes called the feature signature and investigate its properties. We find a remarkable similarity in the nature of feature signatures across multiple nontrivial programs, developers and magnitude changes. This indicates that feature signatures are a meaningful notion worth studying. We then show numerous applications of feature signatures to software evolution, establishing their utility.

Web and GUI programs represent two extremely common and popular modes of human-computer interaction. Many GUI programs share the Web's notion of browsing through data- and decision-trees. This paper compares the user's browsing power in the two cases and illustrates that many GUI programs fall short of the Web's power to clone windows and bookmark applications. It identifies a key implementation problem that GUI programs must overcome to provide this power. It then describes a theoretically well-founded programming pattern, which we have automated, that endows GUI programs with these capabilities. The paper provides concrete examples of the transformation in action.

Feature-oriented programming organizes programs around features rather than objects, thus better supporting extensible, product-line architectures. Programming languages increasingly support this style of programming, but programmers get little support from verification tools. Ideally, programmers should be able to verify features independently of each other and use automated compositional reasoning techniques to infer properties of a system from properties of its features. Achieving this requires carefully designed interfaces: they must hold sufficient information to enable compositional verification, yet tools should be able to generate this information automatically because experience indicates programmers cannot or will not provide it manually. We present a model of interfaces that supports automated, compositional, feature-oriented model checking. To demonstrate their utility, we automatically detect the feature-interaction problems originally found manually by R. Hall in an email suite case study.

Feature-oriented software designs capture many interesting notions of cross-cutting, and offer a powerful method for building product-line architectures. Each cross-cutting feature is an independent module that fundamentally yields an open system from a verification perspective. We describe desiderata for verifying such modules through model checking and find that existing work on the verification of open systems fails to address most of the concerns that arise from feature-oriented systems. We therefore provide a new methodology for verifying such systems. To validate this new methodology, we have implemented it and applied it to a suite of modules that exhibit feature interaction problems. Our model checker was able to automatically locate ten problems previously found through a laborious simulation-based effort.

DrScheme is a programming environment for Scheme. It fully integrates a graphics-enriched editor, a parser for multiple variants of Scheme, a functional read-eval-print loop, and an algebraic printer. The environment is especially useful for students, because it has a tower of syntactically restricted variants of Scheme that are designed to catch typical student mistakes and explain them in terms the students understand. The environment is also useful for professional programmers, due to its sophisticated programming tools, such as the static debugger, and its advanced language features, such as units and mixins. Beyond the ordinary programming environment tools, DrScheme provides an algebraic stepper, a context-sensitive syntax checker, and a static debugger. The stepper reduces Scheme programs to values, according to the reduction semantics of Scheme. It is useful for explaining the semantics of linguistic facilities and for studying the behavior of small programs. The syntax checker annotates programs with font and color changes based on the syntactic structure of the program. On demand, it draws arrows that point from bound to binding occurrences of identifiers. It also supports α-renaming. Finally, the static debugger provides a type inference system that explains specific inferences in terms of a value-flow graph, selectively overlaid on the program text.

The construction of interactive server-side Web applications differs substantially from the construction of traditional interactive programs. In contrast, existing Web programming paradigms force programmers to save and restore control state between user interactions. We present an automated transformation that converts traditional interactive programs into standard CGI programs. This enables reuse of existing software development methodologies. Furthermore, an adaptation of existing programming environments supports the development of Web programs.

Most existing modular model checking techniques betray their hardware roots: they assume that modules compose in parallel. In contrast, collaboration-based software designs, which have proven very successful in several domains, are sequential in the simplest case. Most interesting collaboration-based designs are really quasi-sequential compositions of parallel compositions. These designs demand and inspire new verification techniques. This paper presents algorithms that exploit the software's modular decomposition to verify collaboration-based designs. Our technique can verify most properties locally in the collaborations; we also characterize when a global state space construction is unavoidable. We have validated our proposal by testing it on several designs.

The MrEd virtual machine serves both as the implementation platform for the DrScheme programming environment, and as the underlying Scheme engine for executing expressions and programs entered into DrScheme's read-eval-print loop. We describe the key elements of the MrEd virtual machine for building a programming environment, and we step through the implementation of a miniature version of DrScheme in MrEd. More generally, we show how MrEd defines a high-level operating system for graphical programs.

While class-based object-oriented programming languages provide a flexible mechanism for re-using and managing related pieces of code, they typically lack linguistic facilities for specifying a uniform extension of many classes with one set of fields and methods. As a result, programmers are unable to express certain abstractions over classes.In this paper we develop a model of class-to-class functions that we refer to as mixins. A mixin function maps a class to an extended class by adding or overriding fields and methods. Programming with mixins is similar to programming with single inheritance classes, but mixins more directly encourage programming to interfaces.The paper develops these ideas within the context of Java. The results are 1. an intuitive model of an essential Java subset; 2. an extension that explains and models mixins; and 3. type soundness theorems for these languages.

As software projects continue to grow in scale and scope, it becomes important to reuse software. An important kind of reuse is extensibility, i.e., the extension of software without accessing existing code to edit or copy it. In this paper, we propose a rigorous, semantics-based definition of software extensibility. Then we illustrate the utility of our definitions by applying them to several programs. The examination shows how programming style affects extensibility and also drives the creation of a variant of an existing design pattern. We consider programs in both object-oriented and functional languages to prove the robustness of our definitions. 1 Introduction As software projects have continued to grow in scale and scope, it has become increasingly important to reuse program components. Reuse lowers software development costs by reducing development time, decreasing the number of errors, and increasing the consistency of software systems. In short, there are compelling reasons...

MrSpidey is a user-friendly, interactive static debugger for Scheme. A static debugger supplements the standard debugger by analyzing the program and pinpointing those program operations that may cause run-time errors such as dereferencing the null pointer or applying non-functions. The program analysis of MrSpidey computes value set descriptions for each term in the program and constructs a value flow graph connecting the set descriptions. Using the set descriptions, MrSpidey can identify and highlight potentially erroneous program operations, whose cause the programmer can then explore by selectively exposing portions of the value flow graph.