SPLASH 2025
Sun 12 - Sat 18 October 2025 Singapore
co-located with ICFP/SPLASH 2025
Thu 16 Oct 2025 18:00 - 20:00 at Orchid Dining Hall - SPLASH Posters Session

We present DiLemma, a novel approach to assisting automated inductive equational proofs through lemma discovery with recursive function synthesis. Inductive equational proofs play a crucial role in diverse domains, including the automated assessment of programming assignments and the verification of compiler correctness. However, a major challenge lies in discovering provable and applicable lemmas in stuck states, which often necessitate auxiliary functions to reconcile values of differing structures. To address this issue, we propose DiLemma, a lemma discovery framework that establishes provable lemmas while simultaneously synthesizing and employing auxiliary functions for data handling. DiLemma first identifies recurring patterns from sequences of stuck states, then synthesizes recursive functions based on these patterns, and finally formulates lemmas that integrate the synthesized functions with the corresponding states. Experimental results demonstrate that DiLemma achieves up to a 50% improvement in equivalence proving for introductory-level programs. We further plan to evaluate its effectiveness on benchmarks across a wider range of domains.

Thu 16 Oct

Displayed time zone: Perth change

18:00 - 20:00
SPLASH Posters SessionPosters at Orchid Dining Hall
18:00
2h
Poster
Toward Automated Verification of Static Analysis Results of Android Applications
Posters
Hannuri Kim Chungnam National University, Sungho Lee Chungnam National University, Korea
18:00
2h
Poster
Existentialize your Generics
Posters
Dimi Racordon EPFL, Matt Bovel EPFL, Hamza Remmal EPFL, LAMP
18:00
2h
Poster
View Types in Rust
Posters
Sasha Pak Australian National University, Richard Willie National University of Singapore, Umang Mathur National University of Singapore, Singapore, Fabian Muehlboeck Australian National University, Alex Potanin Australian National University
18:00
2h
Poster
Simplifying Lifter-generated Emulation Style LLVM IR for Analysis Suitability
Posters
Yujin An Chungnam National University, Sungho Lee Chungnam National University, Korea
18:00
2h
Poster
Verifying Extract Method Refactoring in Rust
Posters
Matthew Britton The Australian National University, Alex Potanin Australian National University, Sasha Pak Australian National University
18:00
2h
Poster
Reproducibility Debt in Scientific Software
Posters
Zara Hassan Australian National University, Christoph Treude Singapore Management University, Graham Williams Australian National University, Michael Norrish Australian National University, Alex Potanin Australian National University
18:00
2h
Poster
Lemma Discovery for Inductive Equational Proofs via Recursive Function Synthesis
Posters
Mingyu Jo Korea University, Hakjoo Oh Korea University
18:00
2h
Poster
Logically Qualified Types for Scala
Posters
18:00
2h
Poster
Incremental and Unbounded Loop Analysis
Posters
Arpita Dutta National University of Singapore, Joxan Jaffar National University of Singapore
18:00
2h
Poster
Type Checking for Python Using Intersection Types
Posters
Mingyeong Jeong Chungnam National University, Sungho Lee Chungnam National University, Korea
18:00
2h
Poster
Current Practices for Building LLM-Powered Reasoning Tools Are Ad Hoc—and We Can do Better
Posters
Aaron Bembenek The University of Melbourne