6 citations · 7 across the 4 of their papers we have counts for
Showing 2026Show all
2 papers · 1 filter
cs.PL2026
Foundational Refinement Proofs for EVM Bytecode, at the Price of Tokens
Lefteris Lazaropoulos, Zoe Paraskevopoulou
Relating executable code to a high-level model of its behavior has been a central concern of programming-language research for decades. Formally verified compilers, translation val…
cs.PL2026★ 1 cited
Machine-Generated, Machine-Checked Proofs for a Verified Compiler (Experience Report)
Zoe Paraskevopoulou
We report on using an agentic coding assistant (Claude Code, powered by Claude Opus 4.6) to mechanize a substantial Rocq correctness proof from scratch, with human guidance but wit…