On the Impact of Formal Verification on Software Development (SPLASH 2025 - OOPSLA) - SPLASH 2025

Sun 12 - Sat 18 October 2025 Singapore

co-located with ICFP/SPLASH 2025

Who

Eric Mugnier, Zhou Yuanyuan, Ranjit Jhala, Michael Coblenz

Track

SPLASH 2025 OOPSLA

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

When

Fri 17 Oct 2025 16:30 - 16:45 at Orchid East - Verification 1

Abstract

Auto-active verifiers like Dafny aim to make formal methods accessible to non-expert users through SMT automation. However, despite the automation and other programmer-friendly features, they remain sparsely used in real-world software development, due to the significant effort required to apply them in practice.

We interviewed 14 experienced Dafny users about their experiences using it in large-scale projects. We apply grounded theory to analyze the interviews to systematically identify how the use of auto-active verification impacts software development, and to identify opportunities to simplify the use, and hence, expand the adoption of verification in software development.

Eric Mugnier

University of California San Diego

Zhou Yuanyuan

UCSD

Ranjit Jhala

University of California at San Diego

United States

Michael Coblenz

University of California, San Diego

United States

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

Session Program

Fri 17 Oct
Displayed time zone: Perth change

	16:00 - 17:30	Verification 1OOPSLA at Orchid East

	16:00 15m Talk		A Flow-Sensitive Refinement Type System for Verifying eBPF Programs OOPSLA Ameer Hamza Florida State University, Lucas Zavalia Florida State University Tallahassee, Arie Gurfinkel University of Waterloo, Jorge A. Navas Certora, Grigory Fedyukovich Florida State University
	16:15 15m Talk		Automatically Verifying Replication-aware Linearizability OOPSLA Vimala Soundarapandian IIT Madras, Kartik Nagar IIT Madras, Aseem Rastogi Microsoft Research, KC Sivaramakrishnan IIT Madras and Tarides
	16:30 15m Talk		On the Impact of Formal Verification on Software Development OOPSLA Eric Mugnier University of California San Diego, Zhou Yuanyuan UCSD, Ranjit Jhala University of California at San Diego, Michael Coblenz University of California, San Diego
	16:45 15m Talk		Towards Verifying Crash Consistency OOPSLA Keonho Lee University of California, Irvine, Conan Truong University of California, Irvine, Brian Demsky University of California at Irvine
	17:00 15m Talk		TraceLinking Implementations with their Verified Designs OOPSLA Finn Hackett University of British Columbia, Ivan Beschastnikh The University of British Columbia Pre-print
	17:15 15m Talk		Pyrosome: Verified Compilation for Modular Metatheory OOPSLA Dustin Jamner MIT CSAIL, Gabriel Kammer MIT, Ritam Nag MIT, Adam Chlipala MIT CSAIL