6 papers
Automated Testing and Repair for Verified Compilers Generated by a Coding Agent
Martin Rinard
We present an agent based automated testing and repair system for verified compilers that contain four kinds of code: verified code, checked code, unverified code, and specificatio…
Incremental Computation for Efficient Programmable Inference in Probabilistic Programs
Fabian Zaiser, Jack Czenszak, Martin C. Rinard +2
Inference in probabilistic programs generally requires evaluating many possible program executions to find those of high posterior density. To scale inference to large datasets, it…
Testing, Credible Compilation, and Verification in the Axon Verified Compiler in Lean and Claude Code
Martin Rinard
This paper presents the use of testing, credible compilation/translation validation, verification, and audits in the Axon compiler. Axon comes with fully machine checked proofs tha…
Automated Lemma Discovery in Agentic Program Verification
Huan Zhao, Haoxin Tu, Zhengyao Liu +3
Deductive verification provides strong correctness guarantees for code by extracting verification conditions (VCs) and writing formal proofs for them. The expertise-intensive task…
Lexo: Eliminating Stealthy Supply-Chain Attacks via LLM-Assisted Program Regeneration
Evangelos Lamprou, Julian Dai, Grigoris Ntousakis +2
Software supply-chain attacks are an important and ongoing concern in the open source software ecosystem. These attacks maintain the standard functionality that a component impleme…
Probing the Design Space: Parallel Versions for Exploratory Programming
Tom Beckmann, Joana Bergsiek, Eva Krebs +4
Exploratory programming involves open-ended tasks. To evaluate their progress on these, programmers require frequent feedback and means to tell if the feedback they observe is brin…