4 papers
Defense-in-Depth Runtime Safety in Move
Victor Gao, Wolfgang Grieskamp, Vineeth Kashyap +5
Move is a smart-contract language used to execute transactions on the Aptos blockchain. Move programs execute in a sandboxed VM as typed bytecode. The VM statically verifies founda…
Combining Mechanical and Agentic Specification Inference for Move
Wolfgang Grieskamp, Teng Zhang, Vineeth Kashyap
In this paper, we describe early work on a specification inference tool for the Move Prover that combines a weakest-precondition (WP) analysis over Move bytecode with an agentic co…
Formal Verification of Imperative First-Class Functions in Move
Wolfgang Grieskamp, Teng Zhang, Vineeth Kashyap +1
The Move Prover (MVP) is a formal verifier for smart contracts written in the Move programming language. Recently, Move on Aptos was extended with higher-order functions: imperativ…
Monitoring Assumptions in Assume-Guarantee Contracts
Oleg Sokolsky, Teng Zhang, Insup Lee +1
Pre-deployment verification of software components with respect to behavioral specifications in the assume-guarantee form does not, in general, guarantee absence of errors at run t…