ISSTA 2019
Mon 15 - Fri 19 July 2019 Beijing, China
Wed 17 Jul 2019 16:30 - 16:40 at Grand Ballroom - ISSTA Tool Demonstrations

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 Jul
Times are displayed in time zone: Beijing, Chongqing, Hong Kong, Urumqi change

16:00 - 17:30: ISSTA Tool DemonstrationsTool Demonstration at Grand Ballroom
16:00 - 16:10
Talk
Tool Demonstration
Cong WangTsinghua University, Jian GaoSchool of Software, Tsinghua University, Yu Jiang, Zhenchang XingAustralia National University, Huafeng Zhang, Weiliang Ying , Ming GuTsinghua University, Jiaguang Sun
16:10 - 16:20
Talk
Tool Demonstration
16:20 - 16:30
Talk
Tool Demonstration
Li ChiTsinghua University, Min ZhouTsinghua University, Zuxing GuSchool of Software, Tsinghua University, Guang Chen, Yuexing Wang, Jiecheng WuTsinghua University, Ming GuTsinghua University
16:30 - 16:40
Talk
Tool Demonstration
16:40 - 16:50
Talk
Tool Demonstration
16:50 - 17:00
Talk
Tool Demonstration
Linjie PanInstitute of Software, Chinese Academy of Sciences, Baoquan Cui, Jiwei YanInstitute of Software, Chinese Academy of Sciences, Xutong Ma, Jun YanInstitute of Software, Chinese Academy of Sciences, Jian ZhangBeihang University
17:00 - 17:10
Talk
Tool Demonstration
Rohan PadhyeUniversity of California, Berkeley, Caroline LemieuxUniversity of California, Berkeley, Koushik SenUniversity of California, Berkeley
17:10 - 17:20
Talk
Tool Demonstration
Renaud Rwemalika, Marinos Kintis, Mike PapadakisUniversity of Luxembourg, Yves Le TraonUniversity of Luxembourg, Pierre Lorrach
17:20 - 17:30
Talk
Tool Demonstration
Yuying LiState Key Laboratory for Novel Software Technology, Nanjing University, Rui HaoNanjing University, China, Yang FengUniversity of California, Irvine, James JonesUniversity of California, Irvine, Xiaofang Zhang, Zhenyu ChenNanjing University