Incorrectness 2024
as the organisers put it
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, computation ...
who it's for
formal methods researchers, program logics researchers, verification tool developers, static analysis engineers, concurrency researchers, security researchers, testing and QA engineers
topics
under-approximation and incorrectness logic; separation logic for exact/under-approximate reasoning; abstract interpretation with abduction summaries; fractional permissions for race detection; compositional symbolic execution (Gillian); weakest hyper pre predicate transformer; Kleene algebra with top and tests; reachability logic for promising weak memory model; temporal adversarial/logical timing reasoning; counterexample search for forall-exists hyperproperties; type-based incorrectness reasoning and coverage types; two-sided type systems / ill-typed-programs-dont-evaluate
| title | author | length |
|---|---|---|
| My Journey to the Dark Side: Under-Approximation, Incorrectness, Proof | Peter W. O'Hearn | 56m |
Talk describes concrete methods and outcomes: an analyzer built with an abstract interpreter and abduction summaries runs in CI, finds 25,000 race bugs in a… | ||
| A Comparison of Program Logics for (In)Correctness | Flavio Ascari | 31m |
Compares program logics by exact approximation direction and shows over/under duality breaks: Hoare-style correctness and necessary-precondition triples map… | ||
| Unified Compositional Formal Methods: Exact Separation Logic and the Gi... | Andreas Lööw, Daniele Nantes-Sobrinho, Sacha-Élie Ayoun, Nat Karmios, Seung Hoon Park, Petar Maksimovic, Philippa Gardner | 23m |
Claims a single exact separation logic (ESL) that is sound for both over‑approximate verification and under‑approximate bug finding, formalizes an… | ||
| The Never-Ending Trace: An Under-Approximate Approach to Divergence Bug... | Caroline Cronjäger | 19m |
Introduces a forward under-approximating triple that expresses “for every prestate there exists an execution that diverges,” with a divergent variant that… | ||
| Work in Progress: Modelling Incorrect Programs in the Open World with D... | James Noble, Tobias Wrigstad, Susan Eisenbach | 24m |
Proposes using Dafny to model open‑world trust assumptions by adding an opaque ghost predicate (a “bay”) to pre/postconditions so specs explicitly record… | ||
| Hoare-Like Triples and Kleene Algebras with Top and Tests | Lena Verscht, Benjamin Lucien Kaminski | 23m |
A taxonomy of program logics uses predicate transformers plus Kleene algebra with top and tests to show which Hoare-like triples are equationally definable… | ||
| Quantitative Weakest Hyper Pre | Linpeng Zhang, Benjamin Lucien Kaminski | 19m |
A novel calculus defines a weakest hyper pre predicate transformer that predicts quantitative properties over initial sets or probability distributions for… | ||
| A Reachability Logic for a Weak Memory Model with Promises | Heike Wehrheim | 23m |
A compositional proof calculus for reachability on a promising weak‑memory model is presented, using flow event structures as assertions to record promised… | ||
| Towards Temporal Adversarial Logic | Julien Vanegue | 22m |
Preliminary system embeds temporal reasoning into an under‑approximate adversarial program logic and defines a time footprint Δ per command plus left/right… | ||
| Finding counterexamples to ∀∃ hyperproperties | T. Nießen, G. Weissenbacher | 23m |
An algorithm searches for counterexamples to ∀∃-safety hyperproperties in infinite-state software by picking symbolic execution paths for the universal… | ||
| Type-Based Incorrectness Reasoning | Zhe Zhou, Benjamin Delaware, Suresh Jagannathan | 18m |
Claims that coverage types extend refinement types to give underapproximate reasoning that verifies completeness of nondeterministic test generators, and shows… | ||
| Ill-Typed Programs Don't Evaluate | Steven Ramsay, Charlie Walpole | 23m |
Introduces two-sided type systems — sequent-calculus judgments that allow arbitrary expressions on the left and lists of typings on the right, plus a top type… | ||
| nothing matches | ||