![](https://dblp.dagstuhl.de/img/logo.ua.320x120.png)
![](https://dblp.dagstuhl.de/img/dropdown.dark.16x16.png)
![](https://dblp.dagstuhl.de/img/peace.dark.16x16.png)
Остановите войну!
for scientists:
![search dblp search dblp](https://dblp.dagstuhl.de/img/search.dark.16x16.png)
![search dblp](https://dblp.dagstuhl.de/img/search.dark.16x16.png)
default search action
Sorin Lerner
Person information
- affiliation: University of California, San Diego, USA
Refine list
![note](https://dblp.dagstuhl.de/img/note-mark.dark.12x12.png)
refinements active!
zoomed in on ?? of ?? records
view refined list in
export refined list as
Books and Theses
- 2011
- [b1]Sudipta Kundu, Sorin Lerner, Rajesh K. Gupta:
High-Level Verification - Methods and Tools for Verification of System-Level Designs. Springer 2011, ISBN 978-1-4419-9358-8, pp. I-XII, 1-167
Journal Articles
- 2022
- [j7]Aishwarya Sivaraman
, Alex Sanchez-Stern
, Bretton Chen
, Sorin Lerner
, Todd D. Millstein
:
Data-driven lemma synthesis for interactive proofs. Proc. ACM Program. Lang. 6(OOPSLA2): 505-531 (2022) - 2021
- [j6]Kasra Ferdowsifard
, Shraddha Barke
, Hila Peleg
, Sorin Lerner
, Nadia Polikarpova
:
LooPy: interactive program synthesis with control structures. Proc. ACM Program. Lang. 5(OOPSLA): 1-29 (2021) - 2015
- [j5]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:
NSF expedition on variability-aware software: Recent results and contributions. it Inf. Technol. 57(3): 181-198 (2015) - 2012
- [j4]Macneil Shonle, William G. Griswold
, Sorin Lerner:
A framework for the checking and refactoring of crosscutting concepts. ACM Trans. Softw. Eng. Methodol. 21(3): 15:1-15:47 (2012) - 2011
- [j3]Ross Tate
, Michael Stepp, Zachary Tatlock
, Sorin Lerner:
Equality Saturation: A New Approach to Optimization. Log. Methods Comput. Sci. 7(1) (2011) - 2010
- [j2]Sudipta Kundu, Sorin Lerner, Rajesh K. Gupta:
Translation Validation of High-Level Synthesis. IEEE Trans. Comput. Aided Des. Integr. Circuits Syst. 29(4): 566-579 (2010) - 2009
- [j1]Sudipta Kundu, Sorin Lerner, Rajesh Gupta:
High-Level Verification. IPSJ Trans. Syst. LSI Des. Methodol. 2: 131-144 (2009)
Conference and Workshop Papers
- 2024
- [c65]Chenyang An, Zhibo Chen, Qihao Ye, Emily First, Letian Peng, Jiayun Zhang, Zihan Wang, Sorin Lerner, Jingbo Shang:
Learn from Failure: Fine-tuning LLMs with Trial-and-Error Data for Intuitionistic Propositional Logic Proving. ACL (1) 2024: 776-790 - [c64]Kasra Ferdowsi
, Ruanqianqian (Lisa) Huang
, Michael B. James
, Nadia Polikarpova
, Sorin Lerner
:
Validating AI-Generated Code with Live Programming. CHI 2024: 143:1-143:8 - [c63]Pedro Carrott
, Nuno Saavedra
, Kyle Thompson
, Sorin Lerner
, João F. Ferreira
, Emily First
:
CoqPyt: Proof Navigation in Python in the Era of LLMs. SIGSOFT FSE Companion 2024: 637-641 - 2022
- [c62]Ruanqianqian (Lisa) Huang
, Kasra Ferdowsi
, Ana Selvaraj
, Adalbert Gerald Soosai Raj, Sorin Lerner:
Investigating the Impact of Using a Live Programming Environment in a CS1 Course. SIGCSE (1) 2022: 495-501 - 2021
- [c61]Sorin Lerner
:
Live programming and programming by example: better together (keynote). GPCE 2021: 1 - [c60]Sean Kinzer, Joon Kyung Kim, Soroush Ghodrati, Brahmendra Reddy Yatham, Alric Althoff, Divya Mahajan
, Sorin Lerner, Hadi Esmaeilzadeh:
A Computational Stack for Cross-Domain Acceleration. HPCA 2021: 54-70 - [c59]Evan Johnson, David Thien, Yousef Alhessi, Shravan Narayan, Fraser Brown, Sorin Lerner, Tyler McMullen, Stefan Savage, Deian Stefan:
Доверя'й, но проверя'й: SFI safety for native-compiled Wasm. NDSS 2021 - [c58]John Renner, Alex Sanchez-Stern, Fraser Brown, Sorin Lerner, Deian Stefan:
Scooter & Sidecar: a domain-specific approach to writing secure database migrations. PLDI 2021: 710-724 - [c57]Dylan Lukes
, John Sarracino, Cora Coleman, Hila Peleg, Sorin Lerner, Nadia Polikarpova
:
Synthesis of web layouts from examples. ESEC/SIGSOFT FSE 2021: 651-663 - 2020
- [c56]Sorin Lerner:
Projection Boxes: On-the-fly Reconfigurable Visualization for Live Programming. CHI 2020: 1-7 - [c55]Talia Ringer, Alex Sanchez-Stern, Dan Grossman, Sorin Lerner:
REPLica: REPL instrumentation for Coq analysis. CPP 2020: 99-113 - [c54]Eman Sherif, Andy Liu, Brian Nguyen, Sorin Lerner, William G. Griswold
:
Gamification to Aid the Learning of Test Coverage Concepts. CSEE&T 2020: 1-5 - [c53]Alex Sanchez-Stern, Yousef Alhessi, Lawrence K. Saul, Sorin Lerner:
Generating correctness proofs with neural networks. MAPL@PLDI 2020: 1-10 - [c52]Fraser Brown, John Renner, Andres Nötzli, Sorin Lerner, Hovav Shacham, Deian Stefan:
Towards a verified range analysis for JavaScript JITs. PLDI 2020: 135-150 - [c51]Sorin Lerner:
Focused Live Programming with Loop Seeds. UIST 2020: 607-613 - [c50]Kasra Ferdowsifard
, Allen Ordookhanians, Hila Peleg, Sorin Lerner, Nadia Polikarpova:
Small-Step Live Programming by Example. UIST 2020: 614-626 - [c49]Shravan Narayan, Craig Disselkoen, Tal Garfinkel, Nathan Froyd, Eric Rahm, Sorin Lerner, Hovav Shacham, Deian Stefan:
Retrofitting Fine Grain Isolation in the Firefox Renderer. USENIX Security Symposium 2020: 699-716 - 2018
- [c48]Azad Ghaffari, Imoleayo Abel
, Daniel Ricketts, Sorin Lerner, Miroslav Krstic:
Safety Verification Using Barrier Certificates with Application to Double Integrator with Input Saturation and Zero-Order Hold. ACC 2018: 4664-4669 - [c47]Dimitar Bounov, Anthony DeRossi, Massimiliano Menarini, William G. Griswold
, Sorin Lerner:
Inferring Loop Invariants through Gamification. CHI 2018: 231 - [c46]Alex Sanchez-Stern, Pavel Panchekha, Sorin Lerner, Zachary Tatlock
:
Finding root causes of floating point error. PLDI 2018: 256-269 - 2017
- [c45]John Sarracino, Odaris Barrios-Arciga, Jasmine Zhu, Noah Marcus, Sorin Lerner, Ben Wiedermann:
User-Guided Synthesis of Interactive Diagrams. CHI 2017: 195-207 - [c44]Alan Leung, Sorin Lerner:
Parsimony: an IDE for example-guided synthesis of lexers and parsers. ASE 2017: 815-825 - [c43]Zhaomo Yang, Brian Johannesmeyer, Anders Trier Olesen, Sorin Lerner, Kirill Levchenko:
Dead Store Elimination (Still) Considered Harmful. USENIX Security Symposium 2017: 1025-1040 - 2016
- [c42]Gregory Malecha
, Daniel Ricketts, Mario M. Alvarez, Sorin Lerner:
Towards foundational verification of cyber-physical systems. SOSCYPS@CPSWeek 2016: 1-5 - [c41]Daniel Ricketts, Gregory Malecha
, Sorin Lerner:
Modular deductive verification of sampled-data systems. EMSOFT 2016: 17:1-17:10 - [c40]Dimitar Bounov, Rami Gökhan Kici, Sorin Lerner:
Protecting C++ Dynamic Dispatch Through VTable Interleaving. NDSS 2016 - [c39]Marc Andrysco, Ranjit Jhala, Sorin Lerner:
Printing floating-point numbers: a faster, always correct method. POPL 2016: 555-567 - 2015
- [c38]Sorin Lerner, Stephen R. Foster, William G. Griswold
:
Polymorphic Blocks: Formalism-Inspired UI for Structured Connectors. CHI 2015: 3063-3072 - [c37]Stephen R. Foster, Sorin Lerner, William G. Griswold:
Seamless Integration of Coding and Gameplay: Writing Code Without Knowing it. FDG 2015 - [c36]Alan Leung, Dimitar Bounov, Sorin Lerner:
C-to-Verilog translation validation. MEMOCODE 2015: 42-47 - [c35]Daniel Ricketts, Gregory Malecha
, Mario M. Alvarez, Vignesh Gowda, Sorin Lerner:
Towards verification of hybrid systems in a foundational proof assistant. MEMOCODE 2015: 248-257 - [c34]Alan Leung, John Sarracino, Sorin Lerner:
Interactive parser synthesis by example. PLDI 2015: 565-574 - [c33]Marc Andrysco, David Kohlbrenner, Keaton Mowery, Ranjit Jhala, Sorin Lerner, Hovav Shacham:
On Subnormal Floating Point and Abnormal Timing. IEEE Symposium on Security and Privacy 2015: 623-639 - 2014
- [c32]Dongseok Jang, Zachary Tatlock, Sorin Lerner:
SafeDispatch: Securing C++ Virtual Calls from Memory Corruption Attacks. NDSS 2014 - [c31]Daniel Ricketts, Valentin Robert
, Dongseok Jang, Zachary Tatlock
, Sorin Lerner:
Automating formal proofs for reactive systems. PLDI 2014: 452-462 - 2012
- [c30]Stephen R. Foster, William G. Griswold
, Sorin Lerner:
WitchDoctor: IDE support for real-time auto-completion of refactorings. ICSE 2012: 222-232 - [c29]Panagiotis Vekris, Ranjit Jhala, Sorin Lerner, Yuvraj Agarwal:
Towards Verifying Android Apps for the Absence of No-Sleep Energy Bugs. HotPower 2012 - [c28]Alan Leung, Manish Gupta, Yuvraj Agarwal, Rajesh Gupta, Ranjit Jhala, Sorin Lerner:
Verifying GPU kernels by test amplification. PLDI 2012: 383-394 - [c27]Dongseok Jang, Zachary Tatlock, Sorin Lerner:
Establishing Browser Security Guarantees through Formal Shim Verification. USENIX Security Symposium 2012: 113-128 - 2011
- [c26]Michael Stepp, Ross Tate, Sorin Lerner:
Equality-Based Translation Validator for LLVM. CAV 2011: 737-742 - [c25]Macneil Shonle, William G. Griswold
, Sorin Lerner:
Using metaphors from natural discussion to improve the design of arcum. PLATEAU 2011: 39-44 - [c24]Ross Tate, Alan Leung, Sorin Lerner:
Taming wildcards in Java's type system. PLDI 2011: 614-627 - 2010
- [c23]Dongseok Jang, Ranjit Jhala, Sorin Lerner, Hovav Shacham:
An empirical study of privacy-violating information flows in JavaScript web applications. CCS 2010: 270-283 - [c22]Diane Hu, Laurens van der Maaten, Youngmin Cho, Lawrence K. Saul, Sorin Lerner:
Latent Variable Models for Predicting File Dependencies in Large-Scale Software Development. NIPS 2010: 865-873 - [c21]Zachary Tatlock
, Sorin Lerner:
Bringing extensibility to verified compilers. PLDI 2010: 111-121 - [c20]Ross Tate, Michael Stepp, Sorin Lerner:
Generating compiler optimizations from proofs. POPL 2010: 389-402 - 2009
- [c19]Ravi Chugh, Jeffrey A. Meister, Ranjit Jhala, Sorin Lerner:
Staged information flow for javascript. PLDI 2009: 50-62 - [c18]Sudipta Kundu, Zachary Tatlock
, Sorin Lerner:
Proving optimizations correct using parameterized program equivalence. PLDI 2009: 327-337 - [c17]Ross Tate
, Michael Stepp, Zachary Tatlock
, Sorin Lerner:
Equality saturation: a new approach to optimization. POPL 2009: 264-276 - 2008
- [c16]Sudipta Kundu, Sorin Lerner, Rajesh Gupta:
Validating High-Level Synthesis. CAV 2008: 459-472 - [c15]Macneil Shonle, William G. Griswold
, Sorin Lerner:
When refactoring acts like modularity: keeping options open with persistent condition checking. WRT@OOPSLA 2008: 3 - [c14]Zachary Tatlock
, Chris Tucker, David Shuffelton, Ranjit Jhala, Sorin Lerner:
Deep typechecking and refactoring. OOPSLA 2008: 37-52 - [c13]Macneil Shonle, William G. Griswold
, Sorin Lerner:
Addressing common crosscutting problems with Arcum. PASTE 2008: 64-69 - [c12]Ravi Chugh, Jan Wen Voung, Ranjit Jhala, Sorin Lerner:
Dataflow analysis for concurrent programs using datarace detection. PLDI 2008: 316-326 - 2007
- [c11]Sudipta Kundu, Sorin Lerner, Rajesh Gupta:
Automated refinement checking of concurrent systems. ICCAD 2007: 318-325 - [c10]Chris Tucker, David Shuffelton, Ranjit Jhala, Sorin Lerner:
OPIUM: Optimal Package Install/Uninstall Manager. ICSE 2007: 178-188 - [c9]Erika Rice Scherpelz, Sorin Lerner, Craig Chambers:
Automatic inference of optimizer flow functions from semantic meanings. PLDI 2007: 135-145 - [c8]Macneil Shonle, William G. Griswold
, Sorin Lerner:
Beyond refactoring: a framework for modular maintenance of crosscutting design idioms. ESEC/SIGSOFT FSE 2007: 175-184 - [c7]Jan Wen Voung, Ranjit Jhala, Sorin Lerner:
RELAY: static race detection on millions of lines of code. ESEC/SIGSOFT FSE 2007: 205-214 - 2005
- [c6]Sorin Lerner, Todd D. Millstein
, Erika Rice, Craig Chambers:
Automated soundness proofs for dataflow analyses and transformations via local rules. POPL 2005: 364-377 - 2004
- [c5]Sorin Lerner, Todd D. Millstein, Craig Chambers:
Cobalt: A Language for Writing Provably-Sound Compiler Optimizations. COCV@ETAPS 2004: 5-17 - 2003
- [c4]Sorin Lerner, Todd D. Millstein
, Craig Chambers:
Automatically proving the correctness of compiler optimizations. PLDI 2003: 220-231 - 2002
- [c3]Manuvir Das, Sorin Lerner, Mark Seigle:
ESP: Path-Sensitive Program Verification in Polynomial Time. PLDI 2002: 57-68 - [c2]Sorin Lerner, David Grove
, Craig Chambers:
Composing dataflow analyses and transformations. POPL 2002: 270-282 - [c1]Stephen Adams, Thomas Ball, Manuvir Das, Sorin Lerner, Sriram K. Rajamani, Mark Seigle, Westley Weimer:
Speeding Up Dataflow Analysis Using Flow-Insensitive Pointer Analysis. SAS 2002: 230-246
Editorship
- 2010
- [e1]Sorin Lerner, Atanas Rountev:
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. ACM 2010, ISBN 978-1-4503-0082-7 [contents]
Informal and Other Publications
- 2024
- [i8]Chenyang An, Zhibo Chen, Qihao Ye, Emily First, Letian Peng, Jiayun Zhang, Zihan Wang, Sorin Lerner, Jingbo Shang:
Learn from Failure: Fine-Tuning LLMs with Trial-and-Error Data for Intuitionistic Propositional Logic Proving. CoRR abs/2404.07382 (2024) - [i7]Pedro Carrott, Nuno Saavedra, Kyle Thompson, Sorin Lerner, João F. Ferreira, Emily First:
CoqPyt: Proof Navigation in Python in the Era of LLMs. CoRR abs/2405.04282 (2024) - 2023
- [i6]Kasra Ferdowsi, Ruanqianqian (Lisa) Huang, Michael B. James, Nadia Polikarpova, Sorin Lerner:
Live Exploration of AI-Generated Programs. CoRR abs/2306.09541 (2023) - 2020
- [i5]Shravan Narayan, Craig Disselkoen, Tal Garfinkel, Nathan Froyd, Eric Rahm, Sorin Lerner, Hovav Shacham, Deian Stefan:
Retrofitting Fine Grain Isolation in the Firefox Renderer (Extended Version). CoRR abs/2003.00572 (2020) - 2019
- [i4]John Sarracino, Shraddha Barke, Nadia Polikarpova, Sorin Lerner:
Targeted Synthesis for Programming with Data Invariants. CoRR abs/1904.13049 (2019) - [i3]Alex Sanchez-Stern, Yousef Alhessi, Lawrence K. Saul, Sorin Lerner:
Generating Correctness Proofs with Neural Networks. CoRR abs/1907.07794 (2019) - [i2]Shravan Narayan, Tal Garfinkel, Sorin Lerner, Hovav Shacham, Deian Stefan:
Gobi: WebAssembly as a Practical Path to Library Sandboxing. CoRR abs/1912.02285 (2019) - 2017
- [i1]Alex Sanchez-Stern, Pavel Panchekha, Sorin Lerner, Zachary Tatlock:
Finding Root Causes of Floating Point Error with Herbgrind. CoRR abs/1705.10416 (2017)
Coauthor Index
![](https://dblp.dagstuhl.de/img/cog.dark.24x24.png)
manage site settings
To protect your privacy, all features that rely on external API calls from your browser are turned off by default. You need to opt-in for them to become active. All settings here will be stored as cookies with your web browser. For more information see our F.A.Q.
Unpaywalled article links
Add open access links from to the list of external document links (if available).
Privacy notice: By enabling the option above, your browser will contact the API of unpaywall.org to load hyperlinks to open access articles. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the Unpaywall privacy policy.
Archived links via Wayback Machine
For web page which are no longer available, try to retrieve content from the of the Internet Archive (if available).
Privacy notice: By enabling the option above, your browser will contact the API of archive.org to check for archived content of web pages that are no longer available. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the Internet Archive privacy policy.
Reference lists
Add a list of references from ,
, and
to record detail pages.
load references from crossref.org and opencitations.net
Privacy notice: By enabling the option above, your browser will contact the APIs of crossref.org, opencitations.net, and semanticscholar.org to load article reference information. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the Crossref privacy policy and the OpenCitations privacy policy, as well as the AI2 Privacy Policy covering Semantic Scholar.
Citation data
Add a list of citing articles from and
to record detail pages.
load citations from opencitations.net
Privacy notice: By enabling the option above, your browser will contact the API of opencitations.net and semanticscholar.org to load citation information. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the OpenCitations privacy policy as well as the AI2 Privacy Policy covering Semantic Scholar.
OpenAlex data
Load additional information about publications from .
Privacy notice: By enabling the option above, your browser will contact the API of openalex.org to load additional information. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the information given by OpenAlex.
last updated on 2024-08-22 19:40 CEST by the dblp team
all metadata released as open data under CC0 1.0 license
see also: Terms of Use | Privacy Policy | Imprint