ICFP 2023
Mon 4 - Sat 9 September 2023 Seattle, Washington, United States
Wed 6 Sep 2023 10:30 - 11:00 at A - Grand Ballroom 2 - Verification 1 Chair(s): Tahina Ramananandro

For all the successes in verifying low-level, efficient, security-critical code,
little has been said or studied about the structure, architecture
and engineering of such large-scale proof developments.

We present the design, implementation and evaluation of a set of
language-based techniques that allow the programmer to modularly write and
verify code at a high level of abstraction, while retaining control over the
compilation process and producing high-quality, zero-overhead, low-level code
suitable for integration into mainstream software.

We implement our techniques within the F* proof assistant, and
specifically its shallowly-embedded Low* toolchain that compiles to C.
Through our evaluation, we establish that our techniques were critical in
scaling the popular HACL* library past 100,000 lines of verified source
code, and brought about significant gains in proof engineer productivity.

The exposition of our methodology converges on one final, novel case study:
the streaming API, a finicky API that has historically caused many bugs in
high-profile software. Using our approach, we manage to capture the streaming
semantics in a generic way, and apply it ``for free'' to over a dozen
use-cases. Six of those have made it into the reference implementation of the
Python programming language, replacing the previous CVE-ridden code.

Wed 6 Sep

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

10:30 - 12:00
Verification 1ICFP Papers and Events at A - Grand Ballroom 2
Chair(s): Tahina Ramananandro Microsoft Research
10:30
30m
Talk
Modularity, Code Specialization, and Zero-Cost Abstractions for Program Verification
ICFP Papers and Events
Son Ho INRIA, Aymeric Fromherz Inria, Jonathan Protzenko Microsoft Research, Redmond
DOI
11:00
30m
Talk
Higher-Order Property-Directed Reachability
ICFP Papers and Events
Hiroyuki Katsura University of Tokyo, Naoki Kobayashi University of Tokyo, Ryosuke Sato University of Tokyo
DOI
11:30
30m
Talk
Verifying Reliable Network Components in a Distributed Separation Logic with Dependent Separation ProtocolsRemote
ICFP Papers and Events
Léon Gondelman Aarhus University, Jonas Kastberg Hinrichsen Aarhus University, Denmark, Mário Pereira NOVA LINCS & DI -- Nova School of Science and Technology, Amin Timany Aarhus University, Lars Birkedal Aarhus University
DOI