Sorin Lerner

101 papers A* 44A 2B 6C 4Misc 1Journal 27Unranked 15
YearRankTypeTitle / Venue / Authors
2026 A* conf
Tidynote: Always-Clear Notebook Authoring.
CHI
Ruanqianqian (Lisa) Huang, Brian Hempel, Yining Cao, James D. Hollan, Haijun Xia, Sorin Lerner
2026 J jnl
Tidynote: Always-Clear Notebook Authoring.
CoRR
Ruanqianqian (Lisa) Huang, Brian Hempel, Yining Cao, James D. Hollan, Haijun Xia, Sorin Lerner
2025 J jnl
Deriving Representative Structure from Music Corpora.
CoRR
Ilana Shapiro, Ruanqianqian (Lisa) Huang, Zachary Novack, Cheng-i Wang, Hao-Wen Dong, Taylor Berg-Kirkpatrick, Shlomo Dubnov, Sorin Lerner
2025 B conf
HiLDE: Intentional Code Generation via Human-in-the-Loop Decoding.
VL/HCC
Emmanuel Anaya Gonzalez, Raven Rothkopf, Sorin Lerner, Nadia Polikarpova
2025 J jnl
HiLDe: Intentional Code Generation via Human-in-the-Loop Decoding.
CoRR
Emmanuel Anaya Gonzalez, Raven Rothkopf, Sorin Lerner, Nadia Polikarpova
2025 A* conf
How Scientists Use Jupyter Notebooks: Goals, Quality Attributes, and Opportunities.
ICSE
Ruanqianqian (Lisa) Huang, Savitha Ravi, Michael He, Boyu Tian, Sorin Lerner, Michael Coblenz
2025 J jnl
How Scientists Use Jupyter Notebooks: Goals, Quality Attributes, and Opportunities.
CoRR
Ruanqianqian (Lisa) Huang, Savitha Ravi, Michael He, Boyu Tian, Sorin Lerner, Michael Coblenz
2025 J jnl
Lemmanaid: Neuro-Symbolic Lemma Conjecturing.
CoRR
Yousef Alhessi, Sólrún Halla Einarsdóttir, George Granberry, Emily First, Moa Johansson, Sorin Lerner, Nicholas Smallbone
2025 J jnl
Professional Software Developers Don't Vibe, They Control: AI Agent Use for Coding in 2025.
CoRR
Ruanqianqian (Lisa) Huang, Avery Reyna, Sorin Lerner, Haijun Xia, Brian Hempel
2025 A* conf
Rango: Adaptive Retrieval-Augmented Proving for Automated Software Verification.
ICSE
Kyle Thompson, Nuno Saavedra, Pedro Carrott, Kevin Fisher, Alex Sanchez-Stern, Yuriy Brun, João F. Ferreira, Sorin Lerner, Emily First
2025 A* conf
Synthesizing Composite Hierarchical Structure from Symbolic Music Corpora.
IJCAI
Ilana Shapiro, Ruanqianqian (Lisa) Huang, Zachary Novack, Cheng-i Wang, Hao-Wen Dong, Taylor Berg-Kirkpatrick, Shlomo Dubnov, Sorin Lerner
2025 B conf
The Command Line GUIde: Graphical Interfaces from Man Pages via AI.
VL/HCC
Saketh Ram Kasibatla, Kiran Medleri Hiremath, Raven Rothkopf, Sorin Lerner, Haijun Xia, Brian Hempel
2025 J jnl
The Command Line GUIde: Graphical Interfaces from Man Pages via AI.
CoRR
Saketh Ram Kasibatla, Kiran Medleri Hiremath, Raven Rothkopf, Sorin Lerner, Haijun Xia, Brian Hempel
2025 J jnl
Z3Guide: A Scalable, Student-Centered, and Extensible Educational Environment for Logic Modeling.
CoRR
Ruanqianqian (Lisa) Huang, Ayana Monroe, Peli de Halleux, Sorin Lerner, Nikolaj S. Bjørner
2024 J jnl
Cobblestone: Iterative Automation for Formal Verification.
CoRR
Saketh Ram Kasibatla, Arpan Agarwal, Yuriy Brun, Sorin Lerner, Talia Ringer, Emily First
2024 — conf
CoqPyt: Proof Navigation in Python in the Era of LLMs.
SIGSOFT FSE Companion
Pedro Carrott, Nuno Saavedra, Kyle Thompson, Sorin Lerner, João F. Ferreira, Emily First
2024 J jnl
CoqPyt: Proof Navigation in Python in the Era of LLMs.
CoRR
Pedro Carrott, Nuno Saavedra, Kyle Thompson, Sorin Lerner, João F. Ferreira, Emily First
2024 J jnl
Learn from Failure: Fine-Tuning LLMs with Trial-and-Error Data for Intuitionistic Propositional Logic Proving.
CoRR
Chenyang An, Zhibo Chen, Qihao Ye, Emily First, Letian Peng, Jiayun Zhang, Zihan Wang, Sorin Lerner, Jingbo Shang
2024 — conf
Learn from Failure: Fine-tuning LLMs with Trial-and-Error Data for Intuitionistic Propositional Logic Proving.
ACL (1)
Chenyang An, Zhibo Chen, Qihao Ye, Emily First, Letian Peng, Jiayun Zhang, Zihan Wang, Sorin Lerner, Jingbo Shang
2024 J jnl
Rango: Adaptive Retrieval-Augmented Proving for Automated Software Verification.
CoRR
Kyle Thompson, Nuno Saavedra, Pedro Carrott, Kevin Fisher, Alex Sanchez-Stern, Yuriy Brun, João F. Ferreira, Sorin Lerner, Emily First
2024 B conf
UNFOLD: Enabling Live Programming for Debugging GUI Applications.
VL/HCC
Ruanqianqian (Lisa) Huang, Philip J. Guo, Sorin Lerner
2024 A* conf
Validating AI-Generated Code with Live Programming.
CHI
Kasra Ferdowsi, Ruanqianqian (Lisa) Huang, Michael B. James, Nadia Polikarpova, Sorin Lerner
2023 J jnl
Live Exploration of AI-Generated Programs.
CoRR
Kasra Ferdowsi, Ruanqianqian (Lisa) Huang, Michael B. James, Nadia Polikarpova, Sorin Lerner
2022 J jnl
Data-driven lemma synthesis for interactive proofs.
Proc. ACM Program. Lang.
Aishwarya Sivaraman, Alex Sanchez-Stern, Bretton Chen, Sorin Lerner, Todd D. Millstein
2022 — conf
Investigating the Impact of Using a Live Programming Environment in a CS1 Course.
SIGCSE (1)
Ruanqianqian (Lisa) Huang, Kasra Ferdowsi, Ana Selvaraj, Adalbert Gerald Soosai Raj, Sorin Lerner
2021 A* conf
A Computational Stack for Cross-Domain Acceleration.
HPCA
Sean Kinzer, Joon Kyung Kim, Soroush Ghodrati, Brahmendra Reddy Yatham, Alric Althoff, Divya Mahajan, Sorin Lerner, Hadi Esmaeilzadeh
2021 B conf
Live programming and programming by example: better together (keynote).
GPCE
Sorin Lerner
2021 J jnl
LooPy: interactive program synthesis with control structures.
Proc. ACM Program. Lang.
Kasra Ferdowsifard, Shraddha Barke, Hila Peleg, Sorin Lerner, Nadia Polikarpova
2021 A* conf
Scooter & Sidecar: a domain-specific approach to writing secure database migrations.
PLDI
John Renner, Alex Sanchez-Stern, Fraser Brown, Sorin Lerner, Deian Stefan
2021 — conf
Synthesis of web layouts from examples.
ESEC/SIGSOFT FSE
Dylan Lukes, John Sarracino, Cora Coleman, Hila Peleg, Sorin Lerner, Nadia Polikarpova
2021 A* conf
Доверя'й, но проверя'й: SFI safety for native-compiled Wasm.
NDSS
Evan Johnson, David Thien, Yousef Alhessi, Shravan Narayan, Fraser Brown, Sorin Lerner, Tyler McMullen, Stefan Savage, Deian Stefan
2020 A* conf
Focused Live Programming with Loop Seeds.
UIST
Sorin Lerner
2020 — conf
Gamification to Aid the Learning of Test Coverage Concepts.
CSEE&T
Eman Sherif, Andy Liu, Brian Nguyen, Sorin Lerner, William G. Griswold
2020 — conf
Generating correctness proofs with neural networks.
MAPL@PLDI
Alex Sanchez-Stern, Yousef Alhessi, Lawrence K. Saul, Sorin Lerner
2020 A* conf
Projection Boxes: On-the-fly Reconfigurable Visualization for Live Programming.
CHI
Sorin Lerner
2020 B conf
REPLica: REPL instrumentation for Coq analysis.
CPP
Talia Ringer, Alex Sanchez-Stern, Dan Grossman, Sorin Lerner
2020 J jnl
Retrofitting Fine Grain Isolation in the Firefox Renderer (Extended Version).
CoRR
Shravan Narayan, Craig Disselkoen, Tal Garfinkel, Nathan Froyd, Eric Rahm, Sorin Lerner, Hovav Shacham, Deian Stefan
2020 A* conf
Retrofitting Fine Grain Isolation in the Firefox Renderer.
USENIX Security Symposium
Shravan Narayan, Craig Disselkoen, Tal Garfinkel, Nathan Froyd, Eric Rahm, Sorin Lerner, Hovav Shacham, Deian Stefan
2020 A* conf
Small-Step Live Programming by Example.
UIST
Kasra Ferdowsifard, Allen Ordookhanians, Hila Peleg, Sorin Lerner, Nadia Polikarpova
2020 A* conf
Towards a verified range analysis for JavaScript JITs.
PLDI
Fraser Brown, John Renner, Andres Nötzli, Sorin Lerner, Hovav Shacham, Deian Stefan
2019 J jnl
Generating Correctness Proofs with Neural Networks.
CoRR
Alex Sanchez-Stern, Yousef Alhessi, Lawrence K. Saul, Sorin Lerner
2019 J jnl
Gobi: WebAssembly as a Practical Path to Library Sandboxing.
CoRR
Shravan Narayan, Tal Garfinkel, Sorin Lerner, Hovav Shacham, Deian Stefan
2019 J jnl
Targeted Synthesis for Programming with Data Invariants.
CoRR
John Sarracino, Shraddha Barke, Nadia Polikarpova, Sorin Lerner
2018 A* conf
Finding root causes of floating point error.
PLDI
Alex Sanchez-Stern, Pavel Panchekha, Sorin Lerner, Zachary Tatlock
2018 A* conf
Inferring Loop Invariants through Gamification.
CHI
Dimitar Bounov, Anthony DeRossi, Massimiliano Menarini, William G. Griswold, Sorin Lerner
2018 C conf
Safety Verification Using Barrier Certificates with Application to Double Integrator with Input Saturation and Zero-Order Hold.
ACC
Azad Ghaffari, Imoleayo Abel, Daniel Ricketts, Sorin Lerner, Miroslav Krstic
2017 A* conf
Dead Store Elimination (Still) Considered Harmful.
USENIX Security Symposium
Zhaomo Yang, Brian Johannesmeyer, Anders Trier Olesen, Sorin Lerner, Kirill Levchenko
2017 J jnl
Finding Root Causes of Floating Point Error with Herbgrind.
CoRR
Alex Sanchez-Stern, Pavel Panchekha, Sorin Lerner, Zachary Tatlock
2017 A* conf
Parsimony: an IDE for example-guided synthesis of lexers and parsers.
ASE
Alan Leung, Sorin Lerner
2017 A* conf
User-Guided Synthesis of Interactive Diagrams.
CHI
John Sarracino, Odaris Barrios-Arciga, Jasmine Zhu, Noah Marcus, Sorin Lerner, Ben Wiedermann
2016 Misc conf
Modular deductive verification of sampled-data systems.
EMSOFT
Daniel Ricketts, Gregory Malecha, Sorin Lerner
2016 A* conf
Printing floating-point numbers: a faster, always correct method.
POPL
Marc Andrysco, Ranjit Jhala, Sorin Lerner
2016 A* conf
Protecting C++ Dynamic Dispatch Through VTable Interleaving.
NDSS
Dimitar Bounov, Rami Gökhan Kici, Sorin Lerner
2016 — conf
Towards foundational verification of cyber-physical systems.
SOSCYPS@CPSWeek
Gregory Malecha, Daniel Ricketts, Mario M. Alvarez, Sorin Lerner
2015 C conf
C-to-Verilog translation validation.
MEMOCODE
Alan Leung, Dimitar Bounov, Sorin Lerner
2015 A* conf
Interactive parser synthesis by example.
PLDI
Alan Leung, John Sarracino, Sorin Lerner
2015 J jnl
NSF expedition on variability-aware software: Recent results and contributions.
it Inf. Technol.
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, Rajesh K. Gupta, Ranjit Jhala, Rakesh Kumar, Sorin Lerner, Subhasish Mitra, Alexandru Nicolau, Tajana Simunic Rosing, Mani B. Srivastava, Steven Swanson, Dennis Sylvester, Yuanyuan Zhou
2015 A* conf
On Subnormal Floating Point and Abnormal Timing.
IEEE Symposium on Security and Privacy
Marc Andrysco, David Kohlbrenner, Keaton Mowery, Ranjit Jhala, Sorin Lerner, Hovav Shacham
2015 A* conf
Polymorphic Blocks: Formalism-Inspired UI for Structured Connectors.
CHI
Sorin Lerner, Stephen R. Foster, William G. Griswold
2015 C conf
Seamless Integration of Coding and Gameplay: Writing Code Without Knowing it.
FDG
Stephen R. Foster, Sorin Lerner, William G. Griswold
2015 C conf
Towards verification of hybrid systems in a foundational proof assistant.
MEMOCODE
Daniel Ricketts, Gregory Malecha, Mario M. Alvarez, Vignesh Gowda, Sorin Lerner
2014 A* conf
Automating formal proofs for reactive systems.
PLDI
Daniel Ricketts, Valentin Robert, Dongseok Jang, Zachary Tatlock, Sorin Lerner
2014 J jnl
Codespells: how to design quests to teach java concepts.
J. Comput. Sci. Coll.
Sarah Esper, Samantha R. Wood, Stephen R. Foster, Sorin Lerner, William G. Griswold
2014 A* conf
SafeDispatch: Securing C++ Virtual Calls from Memory Corruption Attacks.
NDSS
Dongseok Jang, Zachary Tatlock, Sorin Lerner
2012 J jnl
A framework for the checking and refactoring of crosscutting concepts.
ACM Trans. Softw. Eng. Methodol.
Macneil Shonle, William G. Griswold, Sorin Lerner
2012 A* conf
Establishing Browser Security Guarantees through Formal Shim Verification.
USENIX Security Symposium
Dongseok Jang, Zachary Tatlock, Sorin Lerner
2012 — conf
Towards Verifying Android Apps for the Absence of No-Sleep Energy Bugs.
HotPower
Panagiotis Vekris, Ranjit Jhala, Sorin Lerner, Yuvraj Agarwal
2012 A* conf
Verifying GPU kernels by test amplification.
PLDI
Alan Leung, Manish Gupta, Yuvraj Agarwal, Rajesh Gupta, Ranjit Jhala, Sorin Lerner
2012 A* conf
WitchDoctor: IDE support for real-time auto-completion of refactorings.
ICSE
Stephen R. Foster, William G. Griswold, Sorin Lerner
2011 J jnl
Equality Saturation: A New Approach to Optimization
Log. Methods Comput. Sci.
Ross Tate, Michael Stepp, Zachary Tatlock, Sorin Lerner
2011 A* conf
Equality-Based Translation Validator for LLVM.
CAV
Michael Stepp, Ross Tate, Sorin Lerner
2011 — book
High-Level Verification - Methods and Tools for Verification of System-Level Designs.
Sudipta Kundu, Sorin Lerner, Rajesh K. Gupta
2011 A* conf
Taming wildcards in Java's type system.
PLDI
Ross Tate, Alan Leung, Sorin Lerner
2011 — conf
Using metaphors from natural discussion to improve the design of arcum.
PLATEAU
Macneil Shonle, William G. Griswold, Sorin Lerner
2010 A* conf
An empirical study of privacy-violating information flows in JavaScript web applications.
CCS
Dongseok Jang, Ranjit Jhala, Sorin Lerner, Hovav Shacham
2010 A* conf
Bringing extensibility to verified compilers.
PLDI
Zachary Tatlock, Sorin Lerner
2010 A* conf
Generating compiler optimizations from proofs.
POPL
Ross Tate, Michael Stepp, Sorin Lerner
2010 — conf
Latent Variable Models for Predicting File Dependencies in Large-Scale Software Development.
NIPS
Diane Hu, Laurens van der Maaten, Youngmin Cho, Lawrence K. Saul, Sorin Lerner
2010 — ed.
Proceedings of the 9th ACM SIGPLAN-SIGSOFT Workshop on Program Analysis for Software Tools and Engineering, PASTE'10, Toronto, Ontario, Canada, June 5-6, 2010
PASTE
Sorin Lerner, Atanas Rountev
2010 J jnl
Translation Validation of High-Level Synthesis.
IEEE Trans. Comput. Aided Des. Integr. Circuits Syst.
Sudipta Kundu, Sorin Lerner, Rajesh K. Gupta
2009 A* conf
Equality saturation: a new approach to optimization.
POPL
Ross Tate, Michael Stepp, Zachary Tatlock, Sorin Lerner
2009 J jnl
High-Level Verification.
Inf. Media Technol.
Sudipta Kundu, Sorin Lerner, Rajesh Gupta
2009 J jnl
High-Level Verification.
IPSJ Trans. Syst. LSI Des. Methodol.
Sudipta Kundu, Sorin Lerner, Rajesh Gupta
2009 A* conf
Proving optimizations correct using parameterized program equivalence.
PLDI
Sudipta Kundu, Zachary Tatlock, Sorin Lerner
2009 A* conf
Staged information flow for javascript.
PLDI
Ravi Chugh, Jeffrey A. Meister, Ranjit Jhala, Sorin Lerner
2008 — conf
Addressing common crosscutting problems with Arcum.
PASTE
Macneil Shonle, William G. Griswold, Sorin Lerner
2008 A* conf
Dataflow analysis for concurrent programs using datarace detection.
PLDI
Ravi Chugh, Jan Wen Voung, Ranjit Jhala, Sorin Lerner
2008 A conf
Deep typechecking and refactoring.
OOPSLA
Zachary Tatlock, Chris Tucker, David Shuffelton, Ranjit Jhala, Sorin Lerner
2008 A* conf
Validating High-Level Synthesis.
CAV
Sudipta Kundu, Sorin Lerner, Rajesh Gupta
2008 — conf
When refactoring acts like modularity: keeping options open with persistent condition checking.
WRT@OOPSLA
Macneil Shonle, William G. Griswold, Sorin Lerner
2007 A conf
Automated refinement checking of concurrent systems.
ICCAD
Sudipta Kundu, Sorin Lerner, Rajesh Gupta
2007 A* conf
Automatic inference of optimizer flow functions from semantic meanings.
PLDI
Erika Rice Scherpelz, Sorin Lerner, Craig Chambers
2007 — conf
Beyond refactoring: a framework for modular maintenance of crosscutting design idioms.
ESEC/SIGSOFT FSE
Macneil Shonle, William G. Griswold, Sorin Lerner
2007 A* conf
OPIUM: Optimal Package Install/Uninstall Manager.
ICSE
Chris Tucker, David Shuffelton, Ranjit Jhala, Sorin Lerner
2007 — conf
RELAY: static race detection on millions of lines of code.
ESEC/SIGSOFT FSE
Jan Wen Voung, Ranjit Jhala, Sorin Lerner
2005 A* conf
Automated soundness proofs for dataflow analyses and transformations via local rules.
POPL
Sorin Lerner, Todd D. Millstein, Erika Rice, Craig Chambers
2004 — conf
Cobalt: A Language for Writing Provably-Sound Compiler Optimizations.
COCV
Sorin Lerner, Todd D. Millstein, Craig Chambers
2003 A* conf
Automatically proving the correctness of compiler optimizations.
PLDI
Sorin Lerner, Todd D. Millstein, Craig Chambers
2002 A* conf
Composing dataflow analyses and transformations.
POPL
Sorin Lerner, David Grove, Craig Chambers
2002 A* conf
ESP: Path-Sensitive Program Verification in Polynomial Time.
PLDI
Manuvir Das, Sorin Lerner, Mark Seigle
2002 B conf
Speeding Up Dataflow Analysis Using Flow-Insensitive Pointer Analysis.
SAS
Stephen Adams, Thomas Ball, Manuvir Das, Sorin Lerner, Sriram K. Rajamani, Mark Seigle, Westley Weimer