ESP: Path-Sensitive Program Verification in Polynomial Time. - Manuvir Das; Sorin Lerner; Mark Seigle (PLDI, 2002)

Composing dataflow analyses and transformations. - Sorin Lerner; David Grove; Craig Chambers (POPL, 2002)

Speeding Up Dataflow Analysis Using Flow-Insensitive Pointer Analysis. - Stephen Adams 001; Thomas Ball 001; Manuvir Das; Sorin Lerner; Sriram K. Rajamani; Mark Seigle; Westley Weimer (SAS, 2002)

Automatically proving the correctness of compiler optimizations. - Sorin Lerner; Todd D. Millstein; Craig Chambers (PLDI, 2003)

Cobalt: A Language for Writing Provably-Sound Compiler Optimizations. - Sorin Lerner; Todd D. Millstein; Craig Chambers (COCV@ETAPS, 2004)

Automated soundness proofs for dataflow analyses and transformations via local rules. - Sorin Lerner; Todd D. Millstein; Erika Rice; Craig Chambers (POPL, 2005)

Automated refinement checking of concurrent systems. - Sudipta Kundu; Sorin Lerner; Rajesh Gupta 001 (ICCAD, 2007)

OPIUM: Optimal Package Install/Uninstall Manager. - Chris Tucker; David Shuffelton; Ranjit Jhala; Sorin Lerner (ICSE, 2007)

Automatic inference of optimizer flow functions from semantic meanings. - Erika Rice Scherpelz; Sorin Lerner; Craig Chambers (PLDI, 2007)

Beyond refactoring: a framework for modular maintenance of crosscutting design idioms. - Macneil Shonle; William G. Griswold; Sorin Lerner (ESEC/SIGSOFT FSE, 2007)

RELAY: static race detection on millions of lines of code. - Jan Wen Voung; Ranjit Jhala; Sorin Lerner (ESEC/SIGSOFT FSE, 2007)

Validating High-Level Synthesis. - Sudipta Kundu; Sorin Lerner; Rajesh Gupta 001 (CAV, 2008)

When refactoring acts like modularity: keeping options open with persistent condition checking. - Macneil Shonle; William G. Griswold; Sorin Lerner (WRT@OOPSLA, 2008)

Deep typechecking and refactoring. - Zachary Tatlock; Chris Tucker; David Shuffelton; Ranjit Jhala; Sorin Lerner (OOPSLA, 2008)

Addressing common crosscutting problems with Arcum. - Macneil Shonle; William G. Griswold; Sorin Lerner (PASTE, 2008)

Dataflow analysis for concurrent programs using datarace detection. - Ravi Chugh; Jan Wen Voung; Ranjit Jhala; Sorin Lerner (PLDI, 2008)

Staged information flow for javascript. - Ravi Chugh; Jeffrey A. Meister; Ranjit Jhala; Sorin Lerner (PLDI, 2009)

Proving optimizations correct using parameterized program equivalence. - Sudipta Kundu; Zachary Tatlock; Sorin Lerner (PLDI, 2009)

High-Level Verification. - Sudipta Kundu; Sorin Lerner; Rajesh Gupta 001 (IPSJ Trans. Syst. LSI Des. Methodol., 2009)

An empirical study of privacy-violating information flows in JavaScript web applications. - Dongseok Jang; Ranjit Jhala; Sorin Lerner; Hovav Shacham (CCS, 2010)

Latent Variable Models for Predicting File Dependencies in Large-Scale Software Development. - Diane Hu; Laurens van der Maaten; Youngmin Cho; Lawrence K. Saul; Sorin Lerner (NIPS, 2010)

Bringing extensibility to verified compilers. - Zachary Tatlock; Sorin Lerner (PLDI, 2010)

Generating compiler optimizations from proofs. - Ross Tate; Michael Stepp; Sorin Lerner (POPL, 2010)

Translation Validation of High-Level Synthesis. - Sudipta Kundu; Sorin Lerner; Rajesh K. Gupta 001 (IEEE Trans. Comput. Aided Des. Integr. Circuits Syst., 2010)

High-Level Verification - Methods and Tools for Verification of System-Level Designs. - Sudipta Kundu; Sorin Lerner; Rajesh K. Gupta 001 (Springer, 2011)

Equality-Based Translation Validator for LLVM. - Michael Stepp; Ross Tate; Sorin Lerner (CAV, 2011)

Using metaphors from natural discussion to improve the design of arcum. - Macneil Shonle; William G. Griswold; Sorin Lerner (PLATEAU, 2011)

Taming wildcards in Java's type system. - Ross Tate; Alan Leung; Sorin Lerner (PLDI, 2011)

Equality Saturation: A New Approach to Optimization - Ross Tate; Michael Stepp; Zachary Tatlock; Sorin Lerner (Log. Methods Comput. Sci., 2011)

WitchDoctor: IDE support for real-time auto-completion of refactorings. - Stephen R. Foster; William G. Griswold; Sorin Lerner (ICSE, 2012)

Towards Verifying Android Apps for the Absence of No-Sleep Energy Bugs. - Panagiotis Vekris; Ranjit Jhala; Sorin Lerner; Yuvraj Agarwal (HotPower, 2012)

Verifying GPU kernels by test amplification. - Alan Leung; Manish Gupta 010; Yuvraj Agarwal; Rajesh Gupta 001; Ranjit Jhala; Sorin Lerner (PLDI, 2012)

Establishing Browser Security Guarantees through Formal Shim Verification. - Dongseok Jang; Zachary Tatlock; Sorin Lerner (USENIX Security Symposium, 2012)

A framework for the checking and refactoring of crosscutting concepts. - Macneil Shonle; William G. Griswold; Sorin Lerner (ACM Trans. Softw. Eng. Methodol., 2012)

SafeDispatch: Securing C++ Virtual Calls from Memory Corruption Attacks. - Dongseok Jang; Zachary Tatlock; Sorin Lerner (NDSS, 2014)

Automating formal proofs for reactive systems. - Daniel Ricketts 001; Valentin Robert; Dongseok Jang; Zachary Tatlock; Sorin Lerner (PLDI, 2014)

Codespells: how to design quests to teach java concepts. - Sarah Esper; Samantha R. Wood; Stephen R. Foster; Sorin Lerner; William G. Griswold (J. Comput. Sci. Coll., 2014)

Polymorphic Blocks: Formalism-Inspired UI for Structured Connectors. - Sorin Lerner; Stephen R. Foster; William G. Griswold (CHI, 2015)

Seamless Integration of Coding and Gameplay: Writing Code Without Knowing it. - Stephen R. Foster; Sorin Lerner; William G. Griswold (FDG, 2015)

C-to-Verilog translation validation. - Alan Leung; Dimitar Bounov; Sorin Lerner (MEMOCODE, 2015)

Towards verification of hybrid systems in a foundational proof assistant. - Daniel Ricketts 001; Gregory Malecha; Mario M. Alvarez; Vignesh Gowda; Sorin Lerner (MEMOCODE, 2015)

Interactive parser synthesis by example. - Alan Leung; John Sarracino; Sorin Lerner (PLDI, 2015)

On Subnormal Floating Point and Abnormal Timing. - Marc Andrysco; David Kohlbrenner; Keaton Mowery; Ranjit Jhala; Sorin Lerner; Hovav Shacham (IEEE Symposium on Security and Privacy, 2015)

NSF expedition on variability-aware software: Recent results and contributions. - Lucas Francisco Wanner; Liangzhen Lai; Abbas Rahimi; Mark Gottscho; Pietro Mercati; Chu-Hsiang Huang; Frederic Sala; Yuvraj Agarwal; Lara Dolecek; Nikil D. Dutt; Puneet Gupta 001; Rajesh K. Gupta 001; et al. (it Inf. Technol., 2015)

Towards foundational verification of cyber-physical systems. - Gregory Malecha; Daniel Ricketts 001; Mario M. Alvarez; Sorin Lerner (SOSCYPS@CPSWeek, 2016)

Modular deductive verification of sampled-data systems. - Daniel Ricketts 001; Gregory Malecha; Sorin Lerner (EMSOFT, 2016)

Protecting C++ Dynamic Dispatch Through VTable Interleaving. - Dimitar Bounov; Rami Gökhan Kici; Sorin Lerner (NDSS, 2016)

Printing floating-point numbers: a faster, always correct method. - Marc Andrysco; Ranjit Jhala; Sorin Lerner (POPL, 2016)

User-Guided Synthesis of Interactive Diagrams. - John Sarracino; Odaris Barrios-Arciga; Jasmine Zhu; Noah Marcus; Sorin Lerner; Ben Wiedermann (CHI, 2017)

Parsimony: an IDE for example-guided synthesis of lexers and parsers. - Alan Leung; Sorin Lerner (ASE, 2017)

Dead Store Elimination (Still) Considered Harmful. - Zhaomo Yang; Brian Johannesmeyer; Anders Trier Olesen; Sorin Lerner; Kirill Levchenko (USENIX Security Symposium, 2017)

Finding Root Causes of Floating Point Error with Herbgrind. - Alex Sanchez-Stern; Pavel Panchekha; Sorin Lerner; Zachary Tatlock (CoRR, 2017)

Safety Verification Using Barrier Certificates with Application to Double Integrator with Input Saturation and Zero-Order Hold. - Azad Ghaffari; Imoleayo Abel; Daniel Ricketts 001; Sorin Lerner; Miroslav Krstic (ACC, 2018)

Inferring Loop Invariants through Gamification. - Dimitar Bounov; Anthony DeRossi; Massimiliano Menarini; William G. Griswold; Sorin Lerner (CHI, 2018)

Finding root causes of floating point error. - Alex Sanchez-Stern; Pavel Panchekha; Sorin Lerner; Zachary Tatlock (PLDI, 2018)

Targeted Synthesis for Programming with Data Invariants. - John Sarracino; Shraddha Barke; Nadia Polikarpova; Sorin Lerner (CoRR, 2019)

Gobi: WebAssembly as a Practical Path to Library Sandboxing. - Shravan Narayan; Tal Garfinkel; Sorin Lerner; Hovav Shacham; Deian Stefan (CoRR, 2019)

Projection Boxes: On-the-fly Reconfigurable Visualization for Live Programming. - Sorin Lerner (CHI, 2020)

REPLica: REPL instrumentation for Coq analysis. - Talia Ringer; Alex Sanchez-Stern; Dan Grossman; Sorin Lerner (CPP, 2020)

Gamification to Aid the Learning of Test Coverage Concepts. - Eman Sherif; Andy Liu; Brian Nguyen; Sorin Lerner; William G. Griswold (CSEE&T, 2020)

Towards a verified range analysis for JavaScript JITs. - Fraser Brown; John Renner; Andres Nötzli; Sorin Lerner; Hovav Shacham; Deian Stefan (PLDI, 2020)

Generating correctness proofs with neural networks. - Alex Sanchez-Stern; Yousef Alhessi; Lawrence K. Saul; Sorin Lerner (MAPL@PLDI, 2020)

Small-Step Live Programming by Example. - Kasra Ferdowsifard; Allen Ordookhanians; Hila Peleg; Sorin Lerner; Nadia Polikarpova (UIST, 2020)

Focused Live Programming with Loop Seeds. - Sorin Lerner (UIST, 2020)

Retrofitting Fine Grain Isolation in the Firefox Renderer. - Shravan Narayan; Craig Disselkoen; Tal Garfinkel; Nathan Froyd; Eric Rahm; Sorin Lerner; Hovav Shacham; Deian Stefan (USENIX Security Symposium, 2020)

Retrofitting Fine Grain Isolation in the Firefox Renderer (Extended Version). - Shravan Narayan; Craig Disselkoen; Tal Garfinkel; Nathan Froyd; Eric Rahm; Sorin Lerner; Hovav Shacham; Deian Stefan (CoRR, 2020)

Live programming and programming by example: better together (keynote). - Sorin Lerner (GPCE, 2021)

A Computational Stack for Cross-Domain Acceleration. - Sean Kinzer; Joon Kyung Kim; Soroush Ghodrati; Brahmendra Reddy Yatham; Alric Althoff; Divya Mahajan 001; Sorin Lerner; Hadi Esmaeilzadeh (HPCA, 2021)

Доверя'й, но проверя'й: SFI safety for native-compiled Wasm. - Evan Johnson 001; David Thien; Yousef Alhessi; Shravan Narayan; Fraser Brown; Sorin Lerner; Tyler McMullen; Stefan Savage; Deian Stefan (NDSS, 2021)

Scooter & Sidecar: a domain-specific approach to writing secure database migrations. - John Renner; Alex Sanchez-Stern; Fraser Brown; Sorin Lerner; Deian Stefan (PLDI, 2021)

Synthesis of web layouts from examples. - Dylan Lukes; John Sarracino; Cora Coleman; Hila Peleg; Sorin Lerner; Nadia Polikarpova (ESEC/SIGSOFT FSE, 2021)

LooPy: interactive program synthesis with control structures. - Kasra Ferdowsifard; Shraddha Barke; Hila Peleg; Sorin Lerner; Nadia Polikarpova (Proc. ACM Program. Lang., 2021)

Investigating the Impact of Using a Live Programming Environment in a CS1 Course. - Ruanqianqian (Lisa) Huang; Kasra Ferdowsi; Ana Selvaraj; Adalbert Gerald Soosai Raj; Sorin Lerner (SIGCSE (1), 2022)

Data-driven lemma synthesis for interactive proofs. - Aishwarya Sivaraman; Alex Sanchez-Stern; Bretton Chen; Sorin Lerner; Todd D. Millstein (Proc. ACM Program. Lang., 2022)

Live Exploration of AI-Generated Programs. - Kasra Ferdowsi; Ruanqianqian (Lisa) Huang; Michael B. James; Nadia Polikarpova; Sorin Lerner (CoRR, 2023)

Learn from Failure: Fine-tuning LLMs with Trial-and-Error Data for Intuitionistic Propositional Logic Proving. - Chenyang An; Zhibo Chen 009; Qihao Ye; Emily First; Letian Peng; Jiayun Zhang; Zihan Wang 001; Sorin Lerner; Jingbo Shang (ACL (1), 2024)

Validating AI-Generated Code with Live Programming. - Kasra Ferdowsi; Ruanqianqian (Lisa) Huang; Michael B. James; Nadia Polikarpova; Sorin Lerner (CHI, 2024)

CoqPyt: Proof Navigation in Python in the Era of LLMs. - Pedro Carrott; Nuno Saavedra; Kyle Thompson; Sorin Lerner; João F. Ferreira 001; Emily First (SIGSOFT FSE Companion, 2024)

UNFOLD: Enabling Live Programming for Debugging GUI Applications. - Ruanqianqian (Lisa) Huang; Philip J. Guo; Sorin Lerner (VL/HCC, 2024)

Cobblestone: Iterative Automation for Formal Verification. - Saketh Ram Kasibatla; Arpan Agarwal; Yuriy Brun; Sorin Lerner; Talia Ringer; Emily First (CoRR, 2024)

How Scientists Use Jupyter Notebooks: Goals, Quality Attributes, and Opportunities. - Ruanqianqian (Lisa) Huang; Savitha Ravi; Michael He; Boyu Tian; Sorin Lerner; Michael Coblenz (ICSE, 2025)

Rango: Adaptive Retrieval-Augmented Proving for Automated Software Verification. - Kyle Thompson; Nuno Saavedra; Pedro Carrott; Kevin Fisher; Alex Sanchez-Stern; Yuriy Brun; João F. Ferreira 001; Sorin Lerner; Emily First (ICSE, 2025)

Deriving Representative Structure from Music Corpora. - Ilana Shapiro; Ruanqianqian (Lisa) Huang; Zachary Novack; Cheng-i Wang; Hao-Wen Dong; Taylor Berg-Kirkpatrick; Shlomo Dubnov; Sorin Lerner (CoRR, 2025)

Lemmanaid: Neuro-Symbolic Lemma Conjecturing. - Yousef Alhessi; Sólrún Halla Einarsdóttir; George Granberry; Emily First; Moa Johansson; Sorin Lerner; Nicholas Smallbone (CoRR, 2025)

HiLDe: Intentional Code Generation via Human-in-the-Loop Decoding. - Emmanuel Anaya Gonzalez; Raven Rothkopf; Sorin Lerner; Nadia Polikarpova (CoRR, 2025)

Z3Guide: A Scalable, Student-Centered, and Extensible Educational Environment for Logic Modeling. - Ruanqianqian (Lisa) Huang; Ayana Monroe; Peli de Halleux; Sorin Lerner; Nikolaj S. Bjørner (CoRR, 2025)