LMPL 2025
who it's for
program verification researchers, developer tool engineers, security researchers, compiler and language engineers, machine learning for code researchers, binary analysis engineers, software architects
topics
LLM call graph construction; cryptographic API misuse detection; LLM-assisted program verification; C++ to Rust translation with LMs; WebAssembly to WebGPU translation; algebraic effect handlers for LLMs; selection monad for LLM sampling; retrieval-augmented proof generation; agentic binary analysis pipelines; hallucination detection via layer scans; specification ranking with LLMs
| title | author | length |
|---|---|---|
| Beyond Static Pattern Matching? Rethinking Automatic Cryptographic API Misuse Detection(…) | Yifan Xia | 18m |
Automatic LLM detection of cryptographic API misuse shows serious instability: over half initial reports are false positives, yet applying a repeated-response… | ||
| CG-Bench: Can Language Models Assist Call Graph Construction in the Real World? | Ting Yuan, Wenrui Zhang, Dong Chen, Jie Wang | 11m |
Benchmark contains 104 call sites drawn from seven large C/C++ projects (GCC, FFMPG, radius, ZFS, cure, open SSH, WRK) and isolates hard cases like dynamic… | ||
| Current Practices for Building LLM-Powered Reasoning Tools Are Ad Hoc—and We Can Do Better | Aaron Bembenek | 15m |
Proposes a Neurosymbolic Transition System that pairs a standard small-step transition system (states, nondeterministic steps) with a domain of intuition and… | ||
| Preguss: It Analyzes, It Specifies, It Verifies | Zhongyi Wang, Tengjie Lin, Mingshuai Chen, Mingqi Yang, Haokun Li, Xiao Yi, Shengchao Qin, Jianwei Yin | 16m |
Preguss decomposes large verification tasks into small VUnits that contain only a guard assertion and minimal context, uses static analysis (RTE alarms) to… | ||
| Programming Large Language Models with Algebraic Effect Handlers and the Selection Monad | Shangyin Tan, Guannan Wei, Koushik Sen, Matei Zaharia | 14m |
Pangolin models LLM calls as algebraic effects and uses a selection monad to search and score nondeterministic outputs; handlers expose a multi‑shot… | ||
| Ranking Formal Specifications using LLMs | Mike He, Zhendong Ang, Ankush Desai, Aarti Gupta | 17m |
An LLM-driven four-metric rating workflow scores mined first-order specifications (generalizability, criticality, distinguishability, visibility) by prompting… | ||
| Challenges in C++ to Rust Translation with Large Language Models: A Preliminary(…) | Yanyan Yan, Yang Feng, Qi He, Jun Zeng, Baowen Xu | 18m |
Empirical evaluation uses GPT-4-turbo and Deepseek-v3 on the roset/Codex-like and Konet datasets, translating small complete units (classes, functions… | ||
| W2GPU: Toward WebAssembly-to-WebGPU Program Translation via Small Language Models | Mehmet Oguz Derin | 16m |
W2GPU fine-tunes small language models to translate WebAssembly Text to WGSL and produces a parallel dataset of 14,547 (WAT, WGSL) pairs derived from GLSL… | ||
| AI Safety through Programming? | Jun Sun | 01h 00m |
Argues that programming ideas can make LLMs safer by: a tiny if-then rule language for domain specs (bank transfers, Singapore traffic and MRT rules) that… | ||
| The Modular Imperative: Rethinking LLMs for Maintainable Software | Anastasiya Kravchuk-Kirilyuk, Fernanda Graciolli, Nada Amin | 16m |
Runs experiments with cursor and cloud sonnet 4 and finds models default to monolithic code, often amplifying complexity and introducing bugs when porting or… | ||
| ClearAgent: Agentic Binary Analysis for Effective Vulnerability Detection | Xiang Chen, Anshunkang Zhou, Chengfeng Ye, Charles Zhang | 15m |
ClearAgent builds an agentic binary-analysis pipeline that wires LLMs to a binary language server and a context manager, using a symbolic lifter (plankton)… | ||
| Toward Repository-Level Program Verification with Large Language Models | Si Cheng Zhong, Xujie Si | 18m |
Introduces a repository-scale verification benchmark RVBench with ~750 proof tasks and >12,000 proof lines drawn from four real Verus projects, and a pipeline… | ||
| A Case Study on the Effectiveness of LLMs in Verification with Proof Assistants | Barış Bayazıt, Yao Li, Xujie Si | 21m |
Evaluation uses two Rocq codebases hs-to-coq (187 proofs) and Verdi (579 proofs), calling LLMs (GPT-4o-mini and DeepSeek/DeepSec family) once per goal and… | ||
| Composable Effect Handling for Programming LLM-integrated Scripts | Di Wang | 20m |
Claim: treating LLM calls, I/O and concurrency as abstract operations discharged by handlers separates workflow from effects and yields real gains. Prototype… | ||
| Hallucination-Resilient LLM-Driven Sound and Tunable Static Analysis | Guannan Wei, Zhuo Zhang, Caterina Urban | 13m |
Claims a sound, LLM-driven static analyzer called LLMAAM that delegates abstract address allocation to an LLM while guaranteeing soundness by construction and… | ||
| nothing matches | ||