This program is tentative and subject to change.

Mon 16 Jan 2023 14:00 - 15:30 at Scollay - Tutorials 5A
Mon 16 Jan 2023 16:00 - 17:30 at Scollay - Tutorials 5B

In computing practice methods for showing the presence of bugs are pervasive and have major impact. But scientific research in program logic and (static) program analysis has overwhelmingly concentrated on meth- ods for proving the absence of bugs rather than their presence. Incor- rectness Logic (IL) has recently been advanced by O’Hearn as a logical under-approximate theory for proving the presence of bug compositionally – the flipside of Hoare Logic, which is an over-approximate compositional theory for proving the absence of bugs. To facilitate scalable bug detec- tion, Raad, O’Hearn and others later developed incorrectness separation logic (ISL) by marrying the under-approximate reasoning of IL with the local reasoning of separation logic and its frame rule. This locality leads to techniques that are compositional both in code (concentrating on a pro- gram component) and in the resources accessed (spatial locality), without tracking the entire global state or the global program within which a com- ponent sits. This enables reasoning to scale to large teams and codebases: reasoning can be done even when a global program is not present. Le, O’Hearn, Raad and others then developed Pulse-X, an automatic program analysis for catching memory safety errors, underpinned by ISL. Pulse-X found a number of real bugs in codebases such as OpenSSL, which were subsequently confirmed and fixed. They have compared the performance of Pulse-X against the state-of-the-art tool Infer on a number of large programs; these comparisons show that Pulse-X is comparable with Infer in terms of performance, and in certain cases its fix-rate surpasses that of Infer.

This program is tentative and subject to change.

Mon 16 Jan

Displayed time zone: Eastern Time (US & Canada) change

14:00 - 15:30
Tutorials 5ATutorialFest at Scollay
14:00
90m
Tutorial
Incorrectness Logic and Under-approximation: Foundations of Bug Catching
TutorialFest
Quang Loc Le University College London, Peter O'Hearn Facebook, Azalea Raad Imperial College London
16:00 - 17:30
Tutorials 5BTutorialFest at Scollay
16:00
90m
Tutorial
Incorrectness Logic and Under-approximation: Foundations of Bug Catching
TutorialFest
Quang Loc Le University College London, Peter O'Hearn Facebook, Azalea Raad Imperial College London