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 address the problem of proving a loop invariant property within a perpetual loop. We have two goals. Our first goal is to prove the property holds at over all iterations, ie. to have unbounded verification. Failing this, our subsequent goal is to determine a loop iteration bound where the property holds, ie. to have the best possible bounded verification. Our framework is set in a harness which is essentially a one loop program whose body comprises a bounded computation, for example, one which does not contain any loops. Our interpreter is based on iterative deepening; it performs bounded reasoning at each iteration which increases the bound, and has two key features: incrementality, ie. it learns and exploits the result of the previous iteration, and induction, ie. it has a fixpoint-checking mechanism which can detect that the property is invariant throughout all iterations.

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