15 citations · 61 across the 12 of their papers we have counts for
14 papers
Teaching Geometric Proof with Tech: Pitfalls and Possibilities
Hwei-Shin Harriman, Wode Ni, Yuchen Jin +2
Geometric proof is a foundational yet challenging topic in mathematics, requiring students to integrate visual, logical, and notational skills. While technology has enhanced learni…
A Study of Undefined Behavior Across Foreign Function Boundaries in Rust Libraries
Ian McCormack, Joshua Sunshine, Jonathan Aldrich
Developers rely on the static safety guarantees of the Rust programming language to write secure and performant applications. However, Rust is frequently used to interoperate with…
A Mixed-Methods Study on the Implications of Unsafe Rust for Interoperation, Encapsulation, and Tooling
Ian McCormack, Tomas Dougan, Sam Estep +3
The Rust programming language restricts aliasing to provide static safety guarantees. However, in certain situations, developers need to bypass these guarantees by using a set of u…
Rose: Composable Autodiff for the Interactive Web
Sam Estep, Wode Ni, Raven Rothkopf +1
Reverse-mode automatic differentiation (autodiff) has been popularized by deep learning, but its ability to compute gradients is also valuable for interactive use cases such as bid…
Can Large Language Models Write Good Property-Based Tests?
Vasudev Vikram, Caroline Lemieux, Joshua Sunshine +1
Property-based testing (PBT), while an established technique in the software testing research community, is still relatively underused in real-world software. Pain points in writin…
Gradual C0: Symbolic Execution for Gradual Verification
Jenna DiVincenzo, Ian McCormack, Hemant Gouni +7
Current static verification techniques support a wide range of programs. However, such techniques only support complete and detailed specifications, which places an undue burden on…
Gradual Program Analysis for Null Pointers
Sam Estep, Jenna Wise, Jonathan Aldrich +3
Static analysis tools typically address the problem of excessive false positives by requiring programmers to explicitly annotate their code. However, when faced with incomplete ann…
Containing Malicious Package Updates in npm with a Lightweight Permission System
Gabriel Ferreira, Limin Jia, Joshua Sunshine +1
The large amount of third-party packages available in fast-moving software ecosystems, such as Node.js/npm, enables attackers to compromise applications by pushing malicious update…
Can Advanced Type Systems Be Usable? An Empirical Study of Ownership, Assets, and Typestate in Obsidian
Michael Coblenz, Jonathan Aldrich, Joshua Sunshine +1
Some blockchain programs (smart contracts) have included serious security vulnerabilities. Obsidian is a new typestate-oriented programming language that uses a strong type system…
PLIERS: A Process that Integrates User-Centered Methods into Programming Language Design
Michael Coblenz, Gauri Kambhatla, Paulette Koronkevich +5
Programming language design requires making many usability-related design decisions. However, existing HCI methods can be impractical to apply to programming languages: they have h…
Obsidian: Typestate and Assets for Safer Blockchain Programming
Michael Coblenz, Reed Oei, Tyler Etzel +6
Blockchain platforms are coming into broad use for processing critical transactions among participants who have not established mutual trust. Many blockchains are programmable, sup…
Design Dimensions for Software Certification: A Grounded Analysis
Gabriel Ferreira, Christian Kästner, Joshua Sunshine +2
In many domains, software systems cannot be deployed until authorities judge them fit for use in an intended operating environment. Certification standards and processes have been…
Debugging Framework Applications: Benefits and Challenges
Zack Coker, David Gray Widder, Claire Le Goues +2
Aspects of frameworks, such as inversion of control and the structure of framework applications, require developers to adjust their debugging strategies as compared to debugging se…
Toward Semantic Foundations for Program Editors
Cyrus Omar, Ian Voysey, Michael Hilton +4
Programming language definitions assign formal meaning to complete programs. Programmers, however, spend a substantial amount of time interacting with incomplete programs -- progra…