A Verified Thread-Safe Array in Rust (IWACO 2025)

Sun 12 - Sat 18 October 2025 Singapore

Who

Sasha Pak, Fabian Muehlboeck, Alex Potanin

Track

IWACO 2025

This program is tentative and subject to change.

Time Zone

The program is currently displayed in (GMT+08:00) Perth.

Use conference time zone: (GMT+08:00) PerthSelect other time zone

The GMT offsets shown reflect the offsets at the moment of the conference.

Time Band

By setting a time band, the program will dim events that are outside this time window. This is useful for (virtual) conferences with a continuous program (with repeated sessions).
The time band will also limit the events that are included in the personal iCalendar subscription service.

Display full programSpecify a time band

Save

When

Tue 14 Oct 2025 13:40 - 14:10 at Peony NE - Formal verification Chair(s): Hemant Gouni

Abstract

Rust’s ownership type system limits the flexibility of safe parallel array manipulation. In particular, safe code is con- fined to partitioning arrays into disjoint, contiguous slices. We present a statically verified, thread-safe array API that enables arbitrary parallel access patterns. This unlocks more expressive parallelism in safe Rust without relying on run- time checks or unsafe code.

Sasha Pak

The Australian National University

Australia

Fabian Muehlboeck

Australian National University

Australia

Alex Potanin

Australian National University

Australia

This program is tentative and subject to change.

Time Zone

The program is currently displayed in (GMT+08:00) Perth.

Use conference time zone: (GMT+08:00) PerthSelect other time zone

The GMT offsets shown reflect the offsets at the moment of the conference.

Time Band

Display full programSpecify a time band

Save

Session Program

Tue 14 Oct
Displayed time zone: Perth change

13:40 - 15:20	Formal verificationIWACO at Peony NE Chair(s): Hemant Gouni Carnegie Mellon University

13:40 30m Talk		A Verified Thread-Safe Array in Rust IWACO Sasha Pak The Australian National University, Fabian Muehlboeck Australian National University, Alex Potanin Australian National University
14:10 30m Talk		Unfolding Expressions for Gradual Verification IWACO Hazel Torek Clemson University, Long Tien Nguyen Carnegie Mellon University, Jonathan Aldrich Carnegie Mellon University
14:40 30m Talk		Gradual Verification: Assuring Software Incrementally IWACO Jonathan Aldrich Carnegie Mellon University