About
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, and also to unify it with correctness reasoning. Automated tools based on these theories are under active development at several companies.
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.
Contact
Please direct questions to the workshop organizers, Noam Zilberstein (noamz@cs.cornell.edu), Azalea Raad (azalea.raad@imperial.ac.uk), and Jules Villard (jul@meta.com).
This program is tentative and subject to change.
Tue 21 JanDisplayed time zone: Mountain Time (US & Canada) change
09:00 - 10:30 | |||
09:00 10mDay opening | Introduction TPSA | ||
09:10 60mKeynote | Improving Static Analysis using Information Collected at RuntimeKeynote TPSA Radu Grigore Meta | ||
11:00 - 12:30 | |||
11:00 18mTalk | Data Structure Abstraction and Incorrectness Separation Logic TPSA Andreas Lööw Imperial College London | ||
11:18 18mTalk | Gradual Exact Logic: Unifying Hoare Logic and Incorrectness Logic via Gradual Verification TPSA Pre-print | ||
11:36 18mTalk | Partial Incorrectness Logic TPSA Lena Verscht RWTH Aachen University; Saarland University, Ānrán Wáng Saarland University, Benjamin Lucien Kaminski Saarland University; University College London | ||
11:54 18mTalk | Concurrent Quantum Separation Logic for Fine-Grained Parallelism TPSA Yusuke Matsushita Kyoto University, Kengo Hirata University of Edinburgh, Ryo Wakizaka Kyoto University | ||
12:12 18mTalk | Total Outcome Logic: Termination and Nontermination Proving for Effectful Branching TPSA James Li Cornell University, Noam Zilberstein Cornell University, Alexandra Silva Cornell University | ||
12:30 - 14:00 | |||
12:30 90mLunch | Lunch Catering | ||
12:30 - 14:00 | |||
12:30 90mMeeting | SIGPLAN SC Meeting Catering | ||
14:00 - 15:30 | |||
14:00 18mTalk | Compositional Shape Analysis with Shared Abduction and Biabductive Loop Acceleration (Extended Abstract)Remote TPSA Florian Sextl TU Wien, Austria, Adam Rogalewicz Brno University of Technology, Czechia, Tomáš Vojnar Brno University of Technology, Florian Zuleger TU Vienna Pre-print | ||
14:18 18mTalk | Calculational design of Incorrectness Separation Logic TPSA Lorenzo Gazzella Università di Pisa | ||
14:36 18mTalk | Scalable Bug Detection for Internally Unsafe Libraries: A Logical Approach to Type Refutation TPSA Pedro Carrott Imperial College London, Sacha-Élie Ayoun Imperial College London, Azalea Raad Imperial College London | ||
14:54 18mTalk | Enhancing Infer Compositional Analysis with Summary Specialization TPSA David Pichardie Meta | ||
15:12 18mTalk | Cyclic Message Histories for Automated Safety Verification of Distributed Algorithms TPSA Christian Fontenot University of Colorado Boulder, Gowtham Kaki University of Colorado at Boulder, Bor-Yuh Evan Chang University of Colorado Boulder & Amazon | ||
Accepted Papers
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 should be in the form of extended abstracts and must not exceed three pages (excluding references) in the SIGPLAN two-column format.
| Tue 21 Jan 2025 Workshop |
| Tue 26 Nov 2024 23:59 Author Notification |
| Thu 7 Nov 2024 23:59 Submission Deadline |
Sacha-Élie Ayoun
Imperial College London
United Kingdom
Roberta Gori
University of Pisa
Italy
Benjamin Lucien Kaminski
Saarland University; University College London
Germany
Peter O'Hearn
University College London, UK and Lacework, London, UK
Azalea Raad
Imperial College London
United Kingdom
Julien Vanegue
Imperial College London; Bloomberg
United States
Jules Villard
Meta
United Kingdom
Noam Zilberstein
Cornell University
United States