While decades of research in program logics, abstract interpretation, and separation logic provide a strong foundation for automated static analysis, new challenges have arisen in recent years, spurring accelerated innovation in both the underlying theory and practical implementation of static analysis systems.
One such example is the challenge of incorrectness reasoning. Bug-finding has long been an important part of industrial static analysis, but sound logical theories for incorrectness were only recently explored, motivated by the need for tools that efficiently identify true bugs. Subsequently, incorrectness reasoning has become an active area of research with work to combine it with separation logic, concurrency, abstract interpretation, security and hyperproperties, and type systems. Automated reasoning tools based on these theories are under active development at companies such as Meta and Bloomberg.
Another example is reasoning about computational effects, which is notoriously difficult to automate. Such effects include concurrency, randomization, exceptions, and nontermination. Recent work has been done to develop theories and tools for detecting deadlocks, race conditions, and programs with divergent behavior. In addition, automation techniques are under development for randomized programs, to reason about programs in terms of expectations.
This workshop provides a venue where researchers and practitioners can present speculative ideas about new analysis techniques. Since it is very hard to implement and validate these systems, we encourage the sharing of early stage ideas and emerging trends that are not yet ready for publication in conferences like POPL.
This program is tentative and subject to change.
Mon 12 JanDisplayed time zone: Brussels, Copenhagen, Madrid, Paris change
10:30 - 11:00 | |||
10:30 30mCoffee break | Break POPL Catering | ||
11:00 - 12:30 | |||
11:00 45mKeynote | Keynote: Subarno Barnerjee AWS TPSA Subarno Banerjee Amazon Web Services | ||
11:45 22mTalk | Tracking Dynamically Bound Variable Dependencies TPSA | ||
12:07 23mTalk | Gradually Retrofitting Assurance into Systems Software: A Separation-Logic Approach TPSA Rini Banerjee University of Cambridge, Zain K Aamer University of Pennsylvania, Hiroyuki Katsura University of Cambridge, David Kaloper-Meršinjak University of Cambridge, Dimitrios J. Economou University of Cambridge, Kayvan Memarian University of Cambridge, Dhruv Makwana University of Cambridge, Neel Krishnaswami University of Cambridge, Benjamin C. Pierce University of Pennsylvania, Christopher Pulte University of Cambridge, Peter Sewell University of Cambridge | ||
12:30 - 14:00 | |||
12:30 90mLunch | Lunch POPL Catering | ||
14:00 - 15:30 | |||
14:00 22mTalk | Soteria Rust: Efficient Symbolic Execution for Rust TPSA Opale Sjöstedt Imperial College London, Sacha-Élie Ayoun Imperial College London, Azalea Raad Imperial College London | ||
14:22 22mTalk | Towards automatic functional correctness in the Mopsa static analyzer TPSA Milla Valnet Sorbonne Université, Raphaël Monat Inria and University of Lille, Antoine Miné Sorbonne Université | ||
14:45 22mTalk | An LLVM frontend for Infer for Swift analysis TPSA Dulma Churchill Meta | ||
15:07 22mTalk | Specialisation: Context-Dependent Reasoning in Incorrectness Separation Logic TPSA Raquel Fernandes da Silva Imperial College London, Sacha-Élie Ayoun Imperial College London, Azalea Raad Imperial College London, David Pichardie Meta | ||
15:30 - 16:00 | |||
15:30 30mCoffee break | Break POPL Catering | ||
16:00 - 17:30 | |||
16:00 22mTalk | How to identify security vulnerabilities in Node.js packages? TPSA José Fragoso Santos INESC-ID; Instituto Superior Técnico - University of Lisbon | ||
16:22 22mTalk | Modeling Incorrectness and Unknown Functions with Angelic and Demonic Nondeterminism TPSA Noam Zilberstein Cornell University | ||
16:45 22mTalk | A logic for all reasons TPSA Flavio Ascari University of Konstanz, Roberto Bruni University of Pisa, Lorenzo Gazzella Università di Pisa, Roberta Gori Diaprtimento di Informatica, Universita' di Pisa, Italy | ||
17:07 22mTalk | AMPLE: Fine-grained File Access Policies for Server Applications TPSA | ||
Accepted Talks
Call for Presentations
We invite the submission of talk proposals in topics related to both the mathematical foundations and practical implementations of static analysis. This workshop will not have formal proceedings, so talks covering in-progress or already published work are welcome. Since analysis tools and algorithms are difficult to implement, we also welcome speculative presentations about techniques that are not yet validated. The topics in scope include, but are not limited to:
- Logical foundations for analysis algorithms (e.g. program logics, abstract interpretation, separation logic, etc)
- Emerging problems and use cases for static analysis (with or without proposed solutions)
- Prototype analysis tools
- Incorrectness, under-approximation, and bug-finding
- Analysis with computational effects (e.g., probabilistic, quantum, or concurrent programming)
- Industrial experience reports
Submissions
Submissions should be in the form of extended abstracts and must not exceed three pages (excluding references) in the SIGPLAN two-column format.
The submission website is: https://tpsa26.hotcrp.com