Verifying Numerical Programs via Iterative Abstract Testing

Banghu Yin, Liqian Chen, Jiangchao Liu, Ji Wang, Patrick Cousot

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

Abstract

When applying abstract interpretation to verification, it may suffer from the problem of getting too conservative over-approximations to verify a given target property, and being hardly able to generate counter-examples when the property does not hold. In this paper, we propose iterative abstract testing, to create a property-oriented verification approach based on abstract interpretation. Abstract testing employs forward abstract executions (i.e., forward analysis) together with property checking to mimic (regular) testing, and utilizes backward abstract executions (i.e., backward analysis) to derive necessary preconditions that may falsify the target property, and be useful for reducing the input space that needs further exploration. To verify a property, we conduct abstract testing in an iterative manner by utilizing dynamic partitioning to split the input space into sub-spaces such that each sub-space involves fewer program behaviors and may be easier to verify. Moreover, we leverage bounded exhaustive testing to verify bounded small sub-spaces, as a means to complement abstract testing based verification. The experimental results show that our approach has comparable strength with several state-of-the-art verification tools.

Original languageEnglish (US)
Title of host publicationStatic Analysis - 26th International Symposium, SAS 2019, Proceedings
EditorsBor-Yuh Evan Chang
PublisherSpringer
Pages247-267
Number of pages21
ISBN (Print)9783030323035
DOIs
StatePublished - 2019
Event26th International Static Analysis Symposium, SAS 2019 held as part of the 3rd World Congress on Formal Methods, FM 2019 - Porto, Portugal
Duration: Oct 8 2019Oct 11 2019

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume11822 LNCS
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Conference

Conference26th International Static Analysis Symposium, SAS 2019 held as part of the 3rd World Congress on Formal Methods, FM 2019
CountryPortugal
CityPorto
Period10/8/1910/11/19

Keywords

  • Abstract interpretation
  • Abstract testing
  • Input space partitioning
  • Program verification

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Computer Science(all)

Fingerprint Dive into the research topics of 'Verifying Numerical Programs via Iterative Abstract Testing'. Together they form a unique fingerprint.

Cite this