Static and dynamic analysis techniques and tools for mainstream programming languages (such as Java, C, JavaScript) have received widespread attention for a long time. The application domains of these analyses range from core libraries to modern technologies such as web services and mobile applications. Over time, various analysis frameworks have been developed to provide techniques for optimizing programs, ensuring code quality, and assessing security and compliance. SOAP 2026 aims to bring together the members of the program analysis community to share new developments and shape innovations in program analysis. For SOAP 2026, we invite contributions from researchers and practitioners working with program analysis. We are particularly interested in exciting analysis framework ideas, application of existing static analysis techniques to industrial software, adoption of static analysis in software engineering practices (such as DevOps), innovative designs, and analysis techniques, including preliminary results or work in progress. We will also focus on the state of the practice for program analysis by encouraging submissions by industrial participants, including tool demonstration submissions. The workshop agenda will continue its tradition of lively discussions on extensions of existing frameworks, the development of novel analyses and tools, and how program analysis is used in real-world scenarios.
Keynote Speakers
| Yannis Smaragdakis | Michael Emmi | Qirun Zhang |
|
|
|
|
| Bio: Yannis Smaragdakis is a Professor at the University of Athens. He has worked on whatever he thought was cool, for the past 30 years. Among others: static analysis algorithms (expressed declaratively, in Datalog), generics and meta-programming, and systems (virtual memory, multithreading). He has received an NSF Career award, European Research Council (ERC) Advanced and Consolidator grants, and best paper awards at OOPSLA'18, ECOOP'18, ISSTA'12, ASE'07, ISSTA'06, GPCE'04, and USENIX'99. He co-founded Dedaub, a leading company for smart contract security. | Bio: Michael Emmi is a Principal Applied Scientist at Amazon Web Services, where he has spent the past six years leading the development of a compositional static analysis engine used to reason about data flows across Amazon's codebase at scale. His research interests include program verification, static analysis, and concurrency. Previously, he was a researcher at Nokia Bell Labs, SRI International, and the IMDEA Software Institute, and holds a PhD in Computer Science from UCLA. His work has been published at venues including POPL, CAV, and PLDI. | Bio: Qirun Zhang is a Catherine M. and James E. Allchin Early Career Associate Professor in the School of Computer Science at Georgia Tech. His research broadly spans programming languages and software engineering, with a focus on developing new program analysis frameworks to improve software reliability. He has received a PLDI 2020 Distinguished Paper Award, an FSE 2023 Distinguished Paper Award, an NSF CAREER Award, and an Amazon Research Award in Automated Reasoning. He has served on the program committees of FSE, ICSE, ISSTA, OOPSLA, PLDI, and POPL. |
| How Context-Sensitive Static Analysis Led to the Best Smart Contract Decompiler | Compositional Data-Flow Analysis at Industrial Scale | Compiler-assisted Translation Validation |
| Abstract: When you think of a decompiler or binary lifter, do you think of it as a static analyzer? In this talk I'll explain why you should, at least in highly-challenging setups. Specifically, context-sensitive static analysis has been the basis for the most advanced decompiler of Ethereum VM smart contracts. We will see why decompilation can really be a "what will the program do for all inputs?" question and what bizarre forms of static analysis can help us with the problem. | Abstract: Reasoning about data flows across large codebases — to enforce security policies, map sensitive data for privacy and compliance, and support data-governance requirements — demands automated analysis that is simultaneously scalable, precise, and sound. This talk presents our experience building and deploying a static taint analysis engine at Amazon that addresses these competing demands through compositional, bottom-up data-flow summarization: analyzing individual program components in isolation and combining the results modularly. We discuss the key design choices that make this practical at scale, including strategies for modeling un-analyzable code, generating actionable data-flow traces, and providing analysis diagnostics that help both developers and analysis engineers understand and trust the results. We also reflect on where the approach succeeds, where it falls short, and what extensions we are pursuing. | Abstract: Translation validation aims to check the equivalence between an input program P and its translated counterpart P′. Traditional approaches focus on directly proving properties related to P and P′. Recently, we explored a new direction that makes translation validation more scalable and expressive by leveraging the translation records produced by the underlying optimizing compiler during the transformation from P to P′. In this talk, I will illustrate how compiler translation records can be used to improve the validation of various optimization passes in LLVM. |
This program is tentative and subject to change.
Tue 16 JunDisplayed time zone: Mountain Time (US & Canada) change
09:00 - 10:10 | |||
09:00 10mDay opening | Welcome and Opening Remarks SOAP | ||
09:10 60mKeynote | How Context-Sensitive Static Analysis Led to the Best Smart Contract Decompiler SOAP Yannis Smaragdakis University of Athens | ||
10:10 - 10:40 | |||
10:10 30mCoffee break | Break Catering | ||
10:40 - 12:00 | |||
10:40 20mTalk | Exploring Locally Bounded Translation Validation SOAP Alborz Jelvani Rutgers University, Richard P. Martin Rutgers University, Santosh Nagarakatte Rutgers University | ||
11:00 20mTalk | Ravencheck: Effectively-Propositional Reasoning for Rust SOAP Kunha Kim University of Colorado Boulder, Nicholas V. Lewchenko University of Colorado Boulder, Bor-Yuh Evan Chang University of Colorado Boulder & Amazon, Gowtham Kaki University of Colorado at Boulder | ||
11:20 20mTalk | Compile-Time Java Stream Fusion via mapMultiRECORDED SOAP | ||
11:40 20mTalk | Conditional Execution of Transpiler Passes Based on Per-Script Feature Detection SOAP Rishipal Singh Bhatia Google | ||
12:20 - 13:40 | |||
12:20 80mLunch | Lunch Catering | ||
14:00 - 15:20 | |||
14:00 60mKeynote | Compositional Data-Flow Analysis at Industrial Scale SOAP Michael Emmi Amazon Web Services | ||
15:00 20mTalk | Scaling Static Code Analysis Adoption at WhatsApp iOS SOAP Ákos Hajdu Meta, Jorge Mendez Meta, Sander van Valkenburg Meta, Artem Kupriianets Meta, Matteo Marescotti Meta, Dulma Churchill Meta, Sopot Cela Meta | ||
15:20 - 15:50 | |||
15:20 30mCoffee break | Break Catering | ||
15:50 - 18:00 | |||
15:50 60mKeynote | Compiler-assisted Translation Validation SOAP Qirun Zhang Georgia Institute of Technology | ||
16:50 20mTalk | On the Effectiveness of Modular Testing in EvoSuite SOAP Elizabeth Dinella Bryn Mawr College | ||
17:10 20mTalk | LLM-Integrated Declarative Program Analysis SOAP Sara Baradaran University of Southern California, Amirmohammad Nazari University of Southern California, Mukund Raghothaman University of Southern California | ||
17:30 20mTalk | Detecting Data Leaks in Multi-User LLM Apps via Automated User-Scoped Taint Analysis SOAP Sanjib Kumar Sen Texas A&M University - Corpus Christi, Bozhen Liu Texas A&M University - Corpus Christi | ||
17:50 10mDay closing | Closing Remarks SOAP | ||
Accepted Papers
Call for Papers
The 15th ACM SIGPLAN International Workshop on the State Of the Art in Program Analysis (SOAP 2026) aims to bring together the members of the program analysis community to share new developments and shape new innovations in program analysis.
For SOAP 2026, we invite contributions from researchers and practitioners working with program analysis. We are particularly interested in exciting analysis framework ideas, innovative designs and analysis techniques, including preliminary results or work in progress. We will also focus on the state of the practice for program analysis by encouraging submissions by industrial participants, including tool demonstration submissions. The workshop agenda will continue its tradition of lively discussions on extensions of existing frameworks, the development of novel analyses and tools, and how program analysis is used in real-world scenarios.
Important Dates
- Submission: Mar 10, 2026
- Notification: April 15, 2026
- Camera Ready: May 3, 2026
- Workshop: June 16, 2026
Possible submissions include, but are not limited to:
- A report on a novel implementation of a program analysis, with a focus on practical details or optimization techniques for obtaining precision and performance.
- A new research tool, data, and other artifacts that showcase early implementations of novel program analysis concepts, as well as mature prototypes.
- A description of a novel analysis component, for example, front-ends or abstract domains.
- A report describing an innovative tool built on top of an existing framework.
- A compelling use case for a feature that is not yet supported by existing analysis tools, with good examples and an informal design of the proposed feature.
- An idea paper proposing the integration of existing program analyses to answer interesting novel questions about programs, for example, in IDEs and DevOps practices.
- An experience report on the use of an existing program analysis framework.
- A description of a program analysis tool and screenshots of the main parts of the demo.
Submissions should be four to six-page papers and should be formatted according to the two-column ACM proceedings format. Each reference must list all authors of the paper. The citations should be in numerical style, e.g., [52]. Templates for ACM format are available for Microsoft Word and LaTeX at http://www.sigplan.org/Resources/Author. The ACM class \documentclass[sigplan, screen]{acmart} should be used to ensure the expected default settings and correct colors.
We strongly encourage authors to make their tool and experimental evaluation public and reproducible, through Docker or virtual machines archived on Zenodo.org. There will be no formal artifact evaluation to keep the review process lightweight.
Similar to SOAP 2024 and 2025, the Program Committee of SOAP 2026 plans to invite a selection of accepted papers to submit extended versions to a special issue of the International Journal on Software Tools for Technology Transfer (STTT).
Keynote Speakers
| Yannis Smaragdakis | Michael Emmi | Qirun Zhang |
|
|
|
|
| Bio: Yannis Smaragdakis is a Professor at the University of Athens. He has worked on whatever he thought was cool, for the past 30 years. Among others: static analysis algorithms (expressed declaratively, in Datalog), generics and meta-programming, and systems (virtual memory, multithreading). He has received an NSF Career award, European Research Council (ERC) Advanced and Consolidator grants, and best paper awards at OOPSLA'18, ECOOP'18, ISSTA'12, ASE'07, ISSTA'06, GPCE'04, and USENIX'99. He co-founded Dedaub, a leading company for smart contract security. | Bio: Michael Emmi is a Principal Applied Scientist at Amazon Web Services, where he has spent the past six years leading the development of a compositional static analysis engine used to reason about data flows across Amazon's codebase at scale. His research interests include program verification, static analysis, and concurrency. Previously, he was a researcher at Nokia Bell Labs, SRI International, and the IMDEA Software Institute, and holds a PhD in Computer Science from UCLA. His work has been published at venues including POPL, CAV, and PLDI. | Bio: Qirun Zhang is a Catherine M. and James E. Allchin Early Career Associate Professor in the School of Computer Science at Georgia Tech. His research broadly spans programming languages and software engineering, with a focus on developing new program analysis frameworks to improve software reliability. He has received a PLDI 2020 Distinguished Paper Award, an FSE 2023 Distinguished Paper Award, an NSF CAREER Award, and an Amazon Research Award in Automated Reasoning. He has served on the program committees of FSE, ICSE, ISSTA, OOPSLA, PLDI, and POPL. |
| How Context-Sensitive Static Analysis Led to the Best Smart Contract Decompiler | Compositional Data-Flow Analysis at Industrial Scale | Compiler-assisted Translation Validation |
| Abstract: When you think of a decompiler or binary lifter, do you think of it as a static analyzer? In this talk I'll explain why you should, at least in highly-challenging setups. Specifically, context-sensitive static analysis has been the basis for the most advanced decompiler of Ethereum VM smart contracts. We will see why decompilation can really be a "what will the program do for all inputs?" question and what bizarre forms of static analysis can help us with the problem. | Abstract: Reasoning about data flows across large codebases — to enforce security policies, map sensitive data for privacy and compliance, and support data-governance requirements — demands automated analysis that is simultaneously scalable, precise, and sound. This talk presents our experience building and deploying a static taint analysis engine at Amazon that addresses these competing demands through compositional, bottom-up data-flow summarization: analyzing individual program components in isolation and combining the results modularly. We discuss the key design choices that make this practical at scale, including strategies for modeling un-analyzable code, generating actionable data-flow traces, and providing analysis diagnostics that help both developers and analysis engineers understand and trust the results. We also reflect on where the approach succeeds, where it falls short, and what extensions we are pursuing. | Abstract: Translation validation aims to check the equivalence between an input program P and its translated counterpart P′. Traditional approaches focus on directly proving properties related to P and P′. Recently, we explored a new direction that makes translation validation more scalable and expressive by leveraging the translation records produced by the underlying optimizing compiler during the transformation from P to P′. In this talk, I will illustrate how compiler translation records can be used to improve the validation of various optimization passes in LLVM. |