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
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.
Plenary

This program is tentative and subject to change.

You're viewing the program in a time zone which is different from your device's time zone change time zone

Tue 16 Jun

Displayed time zone: Mountain Time (US & Canada) change

09:00 - 10:10
KeynoteSOAP at Flatirons 4
Chair(s): Debasmita Lohar IT University of Copenhagen
09:00
10m
Day opening
Welcome and Opening Remarks
SOAP

09:10
60m
Keynote
How Context-Sensitive Static Analysis Led to the Best Smart Contract Decompiler
SOAP
Yannis Smaragdakis University of Athens
10:10 - 10:40
Coffee BreakCatering at Flatirons Foyer
10:10
30m
Coffee break
Break
Catering

10:40 - 12:00
SOAP 1SOAP at Flatirons 4
Chair(s): Jie Zhou The George Washington University
10:40
20m
Talk
Exploring Locally Bounded Translation Validation
SOAP
Alborz Jelvani Rutgers University, Richard P. Martin Rutgers University, Santosh Nagarakatte Rutgers University
11:00
20m
Talk
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
20m
Talk
Compile-Time Java Stream Fusion via mapMultiRECORDED
SOAP
11:40
20m
Talk
Conditional Execution of Transpiler Passes Based on Per-Script Feature Detection
SOAP
12:20 - 13:40
12:20
80m
Lunch
Lunch
Catering

15:20 - 15:50
Coffee BreakCatering at Flatirons Foyer
15:20
30m
Coffee break
Break
Catering

15:50 - 18:00
SOAP 3SOAP at Flatirons 4
Chair(s): Bozhen Liu Texas A&M University - Corpus Christi
15:50
60m
Keynote
Compiler-assisted Translation Validation
SOAP
Qirun Zhang Georgia Institute of Technology
16:50
20m
Talk
On the Effectiveness of Modular Testing in EvoSuite
SOAP
Elizabeth Dinella Bryn Mawr College
17:10
20m
Talk
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
20m
Talk
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
10m
Day closing
Closing Remarks
SOAP

Hide past events

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).

Yannis Smaragdakis Michael Emmi Qirun Zhang
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.