SOAP 2024
as the organisers put it
SOAP 2024 Best Presentation Award goes to Giovanna Kobus Conrado and Andreas Pavlogiannis for their work on “A Better Approximation for Interleaved Dyck Reachability”. Congratulations! 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 program ...
who it's for
program analysis researchers, static analysis engineers, compiler developers, language runtime engineers, software security engineers, tool builders, verification engineers
topics
exact value analysis for Java; Android taint reachability approximation; interleaved Dyck reachability; context-sensitive static analysis; source-to-source C optimizations; static resource leak verification; LLM-assisted static analysis; typed C extensions for dynamic languages; CHERI-specific static checks; floating-point rounding-error analysis
| title | author | length |
|---|---|---|
| Closing and Best Presentation Award | Raphaël Monat, Cindy Rubio-Gonzalez | 03m |
Thanks to 11 program committee members and to session chairs Luca and Helmut for last minute handling, the conference closes after a full day of papers and… | ||
| ValBench: Benchmarking exact value analysis | Marc Miltenberger, Steven Arzt | 18m |
ValBench provides 372 Java, 59 Android tests and an evaluator that generates ground truth by execution on JVM or emulator, then runs and compares seven… | ||
| A Better Approximation for Interleaved Dyck Reachability | Giovanna Kobus Conrado, Andreas Pavlogiannis | 17m |
Proposes a concrete overapproximation that extends mutual refinement by adding refined CFLs (grammars that encode parity and endpoint constraints) and an… | ||
| Misconceptions About Loops in C | Martin Brain, Mahdi Malkawi | 20m |
Static analysis for C loops fails on many surprising edge cases: examples include Duff's device, macros that build reentrant state machines, do‑while loops… | ||
| When to Stop Going Down the Rabbit Hole: Taming Context-Sensitivity on the Fly | Julian Erhard, Johanna Franziska Schinabeck, Michael Schwarz, Helmut Seidl | 24m |
Provides a framework and three generic lifters implemented as decorators around Goblint and evaluated on SV-COMP recursive benchmarks. Limits contexts on the… | ||
| Interactive Source-to-Source Optimizations Validated using Static Resource Analysis | Guillaume Bertholon, Arthur Charguéraud, Thomas Kœhler, Begatim Bytyqi, Damien Rouhling | 22m |
OptiTrust is an interactive source-to-source optimizer for C that uses a lightweight Separation-Logic-based static resource analysis to verify each… | ||
| Lightweight Resource Leak Verification and Inference | Manu Sridharan | 53m |
Presents a modular, type-based verifier that proves resource-leak absence without whole-program alias analysis by treating leaks as an accumulation property… | ||
| Interleaving Static Analysis and LLM Prompting | Patrick J. Chapman, Cindy Rubio-Gonzalez, Aditya V. Thakur | 23m |
A static analyzer (EESI) calls an LLM whenever a function’s error-specification lattice value is bottom, and the LLM output is converted to EESI’s abstract… | ||
| Specializing dynamic language C extensions using type information | Dr Wenowdis | 16m |
Introduces typed methods metadata for C extension functions so a runtime can call them with unboxed C types instead of boxing to PyObject, implemented as a… | ||
| Static Analysis for CHERI | Irina Dudina, Ian Stark | 19m |
Custom Clang Static Analyzer checkers target CHERI portability problems rather than memory exploits: four CHERI-specific checkers detect capability alignment… | ||
| Recent Advances in Floating-point (Static) Analyses | Eva Darulova | 50m |
Presents a modular extension of optimization‑based rounding‑error analysis implemented inside the Daisy framework as Hugo and a functional DSL called DS2l over… | ||
| nothing matches | ||