Checking $\delta$-Satisfiability of Reals with Integrals (SPLASH 2025 - OOPSLA) - SPLASH 2025

Sun 12 - Sat 18 October 2025 Singapore

co-located with ICFP/SPLASH 2025

Who

Cody Rivera, Bishnu Bhusal, Rohit Chadha, A. Prasad Sistla, Mahesh Viswanathan

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

Sat 18 Oct 2025 14:15 - 14:30 at Orchid Small - Proofs

Abstract

Many synthesis and verification problems can be reduced to determining the truth of formulas over the real numbers. These formulas often involve constraints with integrals in them. To this end, we extend the framework of δ-decision procedures with techniques for handling integrals of user-specified real functions. We implement this decision procedure in the tool ∫dReal, which is built on top of dReal.

Cody Rivera

University of Illinois, Urbana-Champaign

Bishnu Bhusal

University of Missouri

Nepal

Rohit Chadha

University of Missouri

A. Prasad Sistla

University of Illinois at Chicago

Mahesh Viswanathan

University of Illinois at Urbana-Champaign

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

Sat 18 Oct
Displayed time zone: Perth change

	13:45 - 15:30	ProofsOOPSLA at Orchid Small

	13:45 15m Talk		Adaptive Shielding via Parametric Safety Proofs OOPSLA Yao Feng Tsinghua University, Jun Zhu Nankai University, André Platzer Karlsruhe Institute of Technology (KIT), Jonathan Laurent Carnegie Mellon University / Karlsruhe Institute of Technology
	14:00 15m Talk		Certified Decision Procedures for Width-Independent Bitvector Predicates OOPSLA Siddharth Bhat University of Cambridge, Leo Stefanesco University of Cambridge, Chris Hughes Independent Researcher, Tobias Grosser University of Cambridge
	14:15 15m Talk		Checking $\delta$-Satisfiability of Reals with Integrals OOPSLA Cody Rivera University of Illinois, Urbana-Champaign, Bishnu Bhusal University of Missouri, Rohit Chadha University of Missouri, A. Prasad Sistla University of Illinois at Chicago, Mahesh Viswanathan University of Illinois at Urbana-Champaign
	14:30 15m Talk		Coinductive Proofs of Regular Expression Equivalence in Zero Knowledge OOPSLA John C. Kolesar Yale University, Shan Ali Yale University, Timos Antonopoulos Yale University, Ruzica Piskac Yale University
	14:45 15m Talk		Incremental Certified Programming OOPSLA Tomás Diaz University of Chile, Kenji Maillard Inria – LS2N, Université de Nantes, Nicolas Tabareau Inria, Éric Tanter University of Chile
	15:00 15m Talk		Pathological Cases for a Class of Reachability-Based Garbage Collectors OOPSLA Matthew Sotoudeh Stanford University Link to publication
	15:15 15m Talk		SafeTree: Expressive Tree Policies for Microservices OOPSLA Karuna Grewal , Brighten Godfrey UIUC and Broadcom, Justin Hsu Cornell University