Formal Methods for Incorrectness 2024Incorrectness 2024
About
While bug-finding has long been an important part of industrial static analysis, sound logical theories for incorrectness reasoning were only recently developed. The introduction of Incorrectness Logic in 2019 highlighted the need for specialized formal methods capable of identifying true bugs and doing so more efficiently using under-approximation.
In the ensuing years, incorrectness reasoning has become an active area of research with work to combine it with separation logic, concurrency, bi-abduction, abstract interpretation, Kleene Algebra, security, hyper properties, computational effects, program synthesis, type systems, and quantitative reasoning. In addition, industrial automated reasoning tools based on theories of incorrectness are under active development, particularly in the Infer static analyzer at Meta.
The first workshop on Formal Methods for Incorrectness will provide a venue for disseminating results and insights broadly related to these new forms of program analysis.
Contact
Please direct questions to the workshop organizers, Noam Zilberstein (noamz@cs.cornell.edu) and Azalea Raad (azalea.raad@imperial.ac.uk).
Tue 16 JanDisplayed time zone: London change
09:00 - 10:30 | |||
09:00 5mDay opening | Welcome Incorrectness | ||
09:05 60mKeynote | My Journey to the Dark Side: Under-Approximation, Incorrectness, Proof Incorrectness Peter W. O'Hearn Lacework; University College London | ||
10:05 22mTalk | A Comparison of Program Logics for (In)Correctness Incorrectness Flavio Ascari University of Pisa Pre-print File Attached | ||
10:30 - 11:00 | |||
10:30 - 11:00 | |||
10:30 30mCoffee break | Break Catering | ||
12:30 - 14:00 | |||
12:30 90mLunch | Lunch Catering | ||
12:30 - 14:00 | |||
12:30 90mLunch | Lunch Catering | ||
14:00 - 15:30 | Concurrency, Security, & Hyper-propertiesIncorrectness at Mountbatten Exhibition Chair(s): Azalea Raad Imperial College London | ||
14:00 22mTalk | Quantitative Weakest Hyper Pre Incorrectness Linpeng Zhang University College London, Benjamin Lucien Kaminski Saarland University; University College London File Attached | ||
14:22 23mTalk | A Reachability Logic for a Weak Memory Model with Promises Incorrectness Lara Bargmann University of Oldenburg, Brijesh Dongol University of Surrey, Heike Wehrheim University of Oldenburg File Attached | ||
14:45 22mTalk | Towards Temporal Adversarial Logic Incorrectness Julien Vanegue Bloomberg, USA | ||
15:07 22mTalk | Finding counterexamples to ∀∃ hyperproperties Incorrectness DOI Pre-print | ||
15:30 - 16:00 | |||
15:30 30mCoffee break | Break Catering | ||
15:30 - 16:00 | |||
15:30 30mCoffee break | Break Catering | ||
16:00 - 17:30 | |||
16:00 22mTalk | Type-Based Incorrectness Reasoning Incorrectness Zhe Zhou Purdue University, Benjamin Delaware Purdue University, Suresh Jagannathan Purdue University | ||
16:23 22mTalk | Ill-Typed Programs Don't Evaluate Incorrectness | ||
Accepted Talks
Call for Presentations
We invite the submission of talk proposals on the topic of incorrectness and under-approximation, as applied to program analysis. This workshop will not have formal proceedings, so talks covering in-progress or already published work are welcome. The topics in scope include, but are not limited to:
- Logical foundations for under-approximation and bug-finding
- Applications of under-approximation in other domains (e.g. for binary analysis, generating/detecting security exploits)
- Static analysis techniques for under-approximation and bug-finding (e.g., abstract interpretation, bi-abduction, symbolic execution, etc.)
- Perspectives on what constitutes a bug
- Incorrectness 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 16 Jan 2024 Workshop |
| Mon 20 Nov 2023 Author Notification |
| Mon 30 Oct 2023 Submission Deadline |
