An Empirical Study in Software Verification Tools

Mengmeng Jiang, Xiaohong Li, Xiaofei Xie, Yao Zhang

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Abstract

Competitions related to software verification, which systematically compare state-of-art software verification systems, have further contributed to the development of software verification. However, so far there is no systematic study on the relationship between code structures and tools' verification answers, which can be another boost to the development of software verification. In this paper, we do a study to understand the different performance of tools based on different code structures. First, we divide programs into eight categories in accordance with their code structures and analyze the data under each category using evaluation schema. Second, we study how the different properties of the same program affect the answers of tools under each category. Third, we investigate the stability of tools when they treat slightly different programs from each other. Fourth, we probe into the existing software verification methods. We find that programs in the memory category are still challenges for software verification tools, although there are some special methods only designed for it. Through our research, we point out problems base on code structures, which should be taken attention by developments of tools.

Original languageEnglish
Title of host publicationProceedings - 2020 International Symposium on Theoretical Aspects of Software Engineering, TASE 2020
EditorsToshiaki Aoki, Qin Li
PublisherInstitute of Electrical and Electronics Engineers Inc.
Pages201-208
Number of pages8
ISBN (Electronic)9781728140865
DOIs
Publication statusPublished - Dec 2020
Externally publishedYes
Event14th International Symposium on Theoretical Aspects of Software Engineering, TASE 2020 - Hangzhou, China
Duration: Dec 11 2020Dec 13 2020

Publication series

NameProceedings - 2020 International Symposium on Theoretical Aspects of Software Engineering, TASE 2020

Conference

Conference14th International Symposium on Theoretical Aspects of Software Engineering, TASE 2020
Country/TerritoryChina
CityHangzhou
Period12/11/2012/13/20

All Science Journal Classification (ASJC) codes

  • Artificial Intelligence
  • Computational Theory and Mathematics
  • Software
  • Safety, Risk, Reliability and Quality
  • Theoretical Computer Science

Fingerprint

Dive into the research topics of 'An Empirical Study in Software Verification Tools'. Together they form a unique fingerprint.

Cite this