2 papers
cs.SE2026
Finding a Crab in the C: Assured Translation via Comparative Symbolic Execution
Caleb Helbling, Graham Leach-Krouse, Michael Crystal
Modern high-assurance software systems development favors memory safe languages such as SPARK (ADA) or Rust. However, developers often encounter non-memory safe code (e.g., C) in l…
cs.GT2025
Rationally Analyzing Shelby: Proving Incentive Compatibility in a Decentralized Storage Network
Michael Crystal, Guy Goren, Scott Duke Kominers
Decentralized storage is one of the most natural applications built on blockchains and a central component of the Web3 ecosystem. Yet despite a decade of active development -- from…