Smart contract analysis and verification

Abstract

As smart contracts being used by more and more industries, security and correctness of them are becoming more important than ever. There have been many security analysis tools for Solidity language, a language for building smart contracts. However, none of them enables the user to provide information about properties the contract is expected to satisfy. This project is our attempt to build a security analysis tool for Solidity, $solv$, that incorporates property declaration given by the user as special comments in the source file. The first part of this project involves building a framework for general property checking in which specific properties can be easily added. After that, specific properties are defined and implemented.