Ethereum smart contracts are public, immutable and distributed and, as such, they are prone to vulnerabilities sourcing from programming mistakes of developers. This paper presents SAFEVM, a verification tool for Ethereum smart contracts that makes use of state-of-the-art verification engines for C programs. SAFEVM takes as input an Ethereum smart contract (provided either in Solidity source code, or in compiled EVM bytecode), optionally with assert and require verification annotations, and produces in the output a report with the verification results. Besides general safety annotations, SAFEVM handles the verification of array accesses: it automatically generates SV-COMP verification assertions such that C verification engines can prove safety of array accesses. Our experimental evaluation has been undertaken on all contracts pulled from etherscan.io (more than 24,000) by using as back-end verifiers CPAchecker, SeaHorn and VeryMax.
Wed 17 JulDisplayed time zone: Beijing, Chongqing, Hong Kong, Urumqi change
16:00 - 17:30 | |||
16:00 10mTalk | Go-Clone: Graph-Embedding Based Clone Detector for Golang Tool Demonstration Cong Wang Tsinghua University, Jian Gao School of Software, Tsinghua University, Yu Jiang , Zhenchang Xing Australia National University, Huafeng Zhang , Weiliang Ying , Ming Gu Tsinghua University, Jiaguang Sun | ||
16:10 10mTalk | VFQL: Combinational Static Analysis as Query Language Tool Demonstration | ||
16:20 10mTalk | VBSAC: A Value-Based Static Analyzer for C Tool Demonstration Li Chi Tsinghua University, Min Zhou Tsinghua University, Zuxing Gu School of Software, Tsinghua University, Guang Chen , Yuexing Wang , Jiecheng Wu Tsinghua University, Ming Gu Tsinghua University | ||
16:30 10mTalk | SAFEVM: A Safety Verifier for Ethereum Smart Contracts Tool Demonstration | ||
16:40 10mTalk | CoCoTest: Collaborative Crowdsourced Testing for Android Applications Tool Demonstration | ||
16:50 10mTalk | Androlic: An Extensible Flow, Context, Object, Field, and Path-Sensitive Static Analysis Framework for Android Tool Demonstration Linjie Pan Institute of Software, Chinese Academy of Sciences, Baoquan Cui , Jiwei Yan Institute of Software, Chinese Academy of Sciences, Xutong Ma , Jun Yan Institute of Software, Chinese Academy of Sciences, Jian Zhang Beihang University | ||
17:00 10mTalk | JQF: Coverage-guided Property-based Testing in Java Tool Demonstration Rohan Padhye University of California, Berkeley, Caroline Lemieux University of California, Berkeley, Koushik Sen University of California, Berkeley | ||
17:10 10mTalk | Ukwikora: Continuous inspection for Keyword-Driven Testing Tool Demonstration Renaud Rwemalika , Marinos Kintis , Mike Papadakis University of Luxembourg, Yves Le Traon University of Luxembourg, Pierre Lorrach | ||
17:20 10mTalk | CTRAS: A Tool for Aggregating and Summarizing Crowdsourced Test Reports Tool Demonstration Yuying Li State Key Laboratory for Novel Software Technology, Nanjing University, Rui Hao Nanjing University, China, Yang Feng University of California, Irvine, James Jones University of California, Irvine, Xiaofang Zhang , Zhenyu Chen Nanjing University | ||