Verifying Numerical Programs via Iterative Abstract Testing
In Proceedings of the 26th International Symposium on Static Analysis, Bor-Yuh Evan Chang (Ed), Porto, Portugal, October 8-11, 2019. LNCS 11822, pp. 247—267, © Springer, 2019.
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 verifica- tion approach based on abstract interpretation. A bstract 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 fewer program behaviors and may be easier to verify. Moreover, we lever- age bounded exhaustive testing to verify bounded small sub-spaces, as a means to complement abstract testing based verification. The experimental show that our approach has comparable strength with several state-of-the-art verification tools.
Program verification — Abstract interpretation — Abstract testing — Input space partitioning
@inproceedings{DBLP:conf/sas/YinCL0C19,
author = {Banghu Yin and
Liqian Chen and
Jiangchao Liu and
Ji Wang and
Patrick Cousot},
title = {Verifying Numerical Programs via Iterative Abstract Testing},
booktitle = {{SAS}},
series = {Lecture Notes in Computer Science},
volume = {11822},
pages = {247--267},
publisher = {Springer},
year = {2019}
}