Yang, Dao Bo2026-04-292026-04-292026-04-292026-04-20https://hdl.handle.net/10012/23114formal verification, Move Prover, prophecy variables, borrow analysis, ownership, invariant injections, automated reasoning, specificationsenProphecy Variables and Invariants in the Move ProverMaster Thesis