SPLASH 2022 Doctoral Symposium
as the organisers put it
SPLASH Doctoral Symposium The SPLASH Doctoral Symposium provides students with useful guidance for completing their dissertation research and beginning their research careers. The symposium will provide an interactive forum for 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. Are you at an earlier stage of your studies? Consider applying to the Programming Languages Mentoring Workshop! Related Student Events at SPLASH Participants to the Doctoral Symposium are highly encoura ...
who it's for
PhD students, programming languages researchers, formal methods researchers, software engineering researchers, systems and security researchers, tool builders and maintainers
topics
call-by-push-value cost model; HOL4 mechanized semantics; Coq mwp flow analysis; probabilistic obliviousness proofs; fuzzing plus symbolic execution; SMT and fuzzing integration; local-first reactive language; technical debt quantification model; automated dependency updates; grammar inference for ad hoc parsers; refinement-type inference for strings; program synthesis for concurrency fixes
| title | author | length |
|---|---|---|
| Researching with Undergraduates: a Curricular Approach | Mae Milano | 36m |
Research with undergraduates is framed as a research syllabus that requires a mature artifact, clear measurable success, established prerequisites, and… | ||
| Elevator Pitches | Zhuo Chen | 16m |
Functional languages need cost accounting but each evaluation strategy forces a new model; the work builds a single cost model for Call-by-Push-Value that… | ||
| Towards a Verified Cost Model for Call-by-Push-Value | Zhuo Chen | 30m |
Claims a verified cost model for the call-by-push-value lambda-calculus mechanised in HOL4, by compiling CBPV terms into a substitution machine and proving a… | ||
| Formally Verified Resource Bounds through Implicit Computational Complexity | Neea Rusch | 29m |
Proposes a mechanically checked soundness proof that completing an mwp flow analysis derivation implies polynomial bounds on variable growth, formalizes a… | ||
| Proving Obliviousness of Probabilistic Algorithms with Formal Verification | Pengbo Yan | 28m |
Claims a practical extension to PSL that supports random-loop conditions and dynamic random choice so probabilistic obliviousness can be proved for algorithms… | ||
| Verification of Programs with Concealed Components | Sumit Lahiri | 26m |
Usher synthesizes inductive invariants for programs with concealed components (inline assembly, third‑party APIs, sampling) by running a learner-teacher loop… | ||
| Verification of Hardware and Software with Fuzzing and Proofs | Sujit Kumar Muduli | 24m |
A verification methodology proves end-to-end security of an authenticated firmware loader on a small SoC model and checks typical attacks like TOCTOU by… | ||
| Programming Support for Local-First Software | Julian Haas | 33m |
Describes Law, a dedicated local-first reactive language that models user and outside-world interactions, encodes invariants (e.g. “≤30 vacation days”), and… | ||
| Modelling the Quantification of Technical Debt | Judith Perera | 31m |
Proposes a concrete Technical Debt Quantification Model that defines 21 concepts and delivers a conceptual model, an approach comparison matrix and a… | ||
| Towards Automated Updates of Software Dependencies | Dhanushka Jayasuriya | 28m |
Study compiles ~3,000 Java repositories (using Maven, Java 8/11) from the Libraries.io dataset and extracts ~18,000 artifacts and 163,000 direct dependencies… | ||
| Grammar Inference for Ad Hoc Parsers | Michael Schröder | 29m |
A system translates ad hoc string code (split/map/trim pipelines) into a small lambda IR, runs refinement-type inference to produce verification templates, and… | ||
| Program Synthesis for Artifacts beyond Programs | Pankaj Kumar Kalita | 22m |
Three synthesis projects convert non‑regular artifacts into regular program synthesis problems and actually build working tools: a first‑order theorem prover… | ||
| nothing matches | ||