Verifying Numerical Programs via Iterative Abstract Testing

EasyChair Preprint 1749

Abstract

This paper aims to create an iterative and property oriented verification approach based on abstract testing. 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, which are useful for reducing the input space that needs further investigation. 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. Compared with abstract interpretation based verification, the strength of our approach will give a proof when the property holds, or generate a counter-example otherwise. The experimental results show that our approach has broad overall strength compared with several state-of-the-art verification tools.

Keyphrases: Abstract Testing, Input space partitioning, abstract interpretation, program verification

@booklet{EasyChair:1749,
  author    = {Banghu Yin and Liqian Chen and Jiangchao Liu and Ji Wang and Patrick Cousot},
  title     = {Verifying Numerical Programs via Iterative Abstract Testing},
  howpublished = {EasyChair Preprint 1749},
  year      = {EasyChair, 2019}}