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

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.