Publications by Jonathan Aldrich

Preprint

A Mixed-Methods Study on the Implications of Unsafe Rust for Interoperation, Encapsulation, and Tooling

2026
McCormack I, Dougan T, Estep S, Hibshi H, Aldrich J, Sunshine J

Conference

Alethiometer - A Debugger for Program Verification

2026
Nguyen LT, Aldrich J

Conference

Barista: Synthesizing Typestate Specifications with LLM Agents

2026 1221-1233
Gamboa C, Canelas P, Costa R, Caetano M, Aldrich J, Fonseca A

Conference

Customizable Type-Checking for Language Extensions in Wyvern: Enforcing Secure Architectural Constraints in Enterprise Software

2026 0562-0567
Anandani S, Aldrich J

Journal Article

Gradual Verification: Assuring Software Incrementally

2026 • Journal of Object Technology • 25(1):
Aldrich J

Preprint

Gradually Verifying Unfolding Expressions & Pure Functions

2026
Torek H, Nguyen LT, Gupta P, DiVincenzo J, Aldrich J

Journal Article

LTIS: A Real-Time Trajectory Integrity Metric for Agentic Loop Engineering

2026
Sheriff A, Aldrich J

Journal Article

Security Reasoning via Substructural Dependency Tracking

2026 • Proceedings of the ACM on Programming Languages • 10(POPL):
Gouni H, Pfenning F, Aldrich J

Preprint

The Duality of Information Flow: Reconciling Robust Downgrading with Non-Interference

2026
Gouni H, Pfenning F, Aldrich J

Preprint

A Study of Undefined Behavior Across Foreign Function Boundaries in Rust Libraries

2025
McCormack I, Sunshine J, Aldrich J

Conference

A Study of Undefined Behavior Across Foreign Function Boundaries in Rust Libraries

2025 • Proceedings - International Conference on Software Engineering • 2075-2086
McCormack I, Sunshine J, Aldrich J

Conference

An Exploratory Study of ML Sketches and Visual Code Assistants

2025 • Proceedings - International Conference on Software Engineering • 1653-1664
Gomes LF, Hellendoorn VJ, Aldrich J, Abreu R

Journal Article

Preface

2025 • Leibniz International Proceedings in Informatics • 333:ix-x
Aldrich J, Silva A

Journal Article

Structural Information Flow: A Fresh Look at Types for Non-interference

2025 • Proceedings of the ACM on Programming Languages • 9(OOPSLA2):
Gouni H, Pfenning F, Aldrich J

Journal Article

Usability Barriers for Liquid Types

2025 • Proceedings of the ACM on Programming Languages • 9(PLDI):
Gamboa C, Reese A, Fonseca A, Aldrich J

Conference

A Comparative Study of Traditional versus Capability-Based Module Systems for Modern Programming Languages

2024
Goyal A, Potanin A, Aldrich J

Preprint

An Exploratory Study of ML Sketches and Visual Code Assistants

2024
Gomes LF, Hellendoorn VJ, Aldrich J, Abreu R

Preprint

Gradual C0: Symbolic Execution for Gradual Verification

2024
DiVincenzo J, McCormack I, Gouni H, Gorenburg J, Ramos-Dávila J-P, Zhang M, Zimmerman C, Sunshine J, Tanter É, Aldrich J

Journal Article

Gradual C0: Symbolic Execution for Gradual Verification

2024 • ACM Transactions on Programming Languages and Systems • 46(4):
Divincenzo J, Mccormack I, Zimmerman C, Gouni H, Gorenburg J, Ramos-davila J-P, Zhang M, Sunshine J, Tanter E, Aldrich J

Preprint

Gradual Verification for Smart Contracts

2024
Sun H, Singh K, Ramos-Dávila J-P, Aldrich J, DiVincenzo J

Journal Article

Message from the Program Chairs

2024 • Leibniz International Proceedings in Informatics • 313:
Aldrich J, Salvaneschi G

Journal Article

Sound Gradual Verification with Symbolic Execution

2024 • Proceedings of the ACM on Programming Languages • 8(POPL):
Zimmerman C, Divincenzo J, Aldrich J

Conference

The Meerkat Vision: Language Support for Live, Scalable, Reactive Web Apps

2024 • PROCEEDINGS OF THE 2024 ACM SIGPLAN INTERNATIONAL SYMPOSIUM ON NEW IDEAS, NEW PARADIGMS, AND REFLECTIONS ON PROGRAMMING AND SOFTWARE, ONWARD! 2024 • 54-67
Seco JC, Aldrich J

Preprint

Sound Gradual Verification with Symbolic Execution

2023
Zimmerman C, DiVincenzo J, Aldrich J

Journal Article

Bounded Abstract Effects

2022 • ACM Transactions on Programming Languages and Systems • 44(1):
Melicher D, Xu A, Zhao V, Potanin A, Aldrich J