Doctoral Symposium @ SPLASH 2025
as the organisers put it
SPLASH Doctoral Symposium The SPLASH Doctoral Symposium provides an interactive forum primarily aimed at mid-stage doctoral students who have progressed far enough in their research to have a structured proposal but will not be defending their dissertation in the next 12 months. Student proposals and presentations will be discussed and evaluated with the aim of providing important guidance for completing their dissertation research and beginning their research careers. The symposium is a one-day event, structured around presentations of a student’s current research agenda and plans, with p ...
who it's for
programming language researchers, compiler engineers, formal verification researchers, security researchers, blockchain developers, quantum software engineers, developer tools engineers
topics
LLVM-based SMT simplification; instrumenting LLVM passes; lexical effect handlers; stack switching via stacktrack; software MMU and virtual resumption; compositional diagram compiler; series-parallel graph layout; runtime guards for upgradeable contracts; Trace2Inv invariant mining; quantum-circuit rewrite synthesis
| title | author | length |
|---|---|---|
| Towards Compiler-Guided Static Analysis | Benjamin Mikek | 21m |
Proposes extracting compiler internals to help static analyses: translates SMT constraints into LLVM IR, runs selected LLVM optimization passes to simplify SMT… | ||
| Lexical Effect Handler: Fast by Design, Correct by Proof | Cong Ma | 22m |
Claims a compiler and language named Lexa that outperforms existing effect handler implementations while preserving lexical scoping and formal correctness… | ||
| Practical compositional diagramming | Shardul Chiplunkar | 21m |
Diagrams are rare in programming and theorem-proving environments because current tools are non‑compositional; this work proposes compositional diagramming and… | ||
| A Multi-Layer Dynamic Security Framework for DeFi Smart Contracts | Zhiyang Chen | 22m |
A multi-layer framework instruments upgradeable contracts with runtime guards and ecosystem monitors: Trace2Inv mines invariants from historical transaction… | ||
| How to Synthesize Quantum-Circuit Optimizers | Amanda Xu | 22m |
Synthesizes provably correct rewrite rules for device-specific gate sets by hashing polynomial circuit semantics so enumeration becomes linear not quadratic… | ||
| Separation Logics for Probability, Concurrency, and Security | Kwing Hei Li | 21m |
Presents concrete logics that extend Iris + Rocq to reason about randomized, higher‑order, concurrent code: unary Errors with an error credit resource that… | ||
| nothing matches | ||