VeriAbs: Verification by Abstraction and Test Generation

被引：13

作者：

Darke, Priyanka ^{[1
]}

Prabhu, Sumanth ^{[1
]}

Chimdyalwar, Bharti ^{[1
]}

Chauhan, Avriti ^{[1
]}

Kumar, Shrawan ^{[1
]}

Basakchowdhury, Animesh ^{[1
]}

Venkatesh, R. ^{[1
]}

Datar, Advaita ^{[1
]}

Medicherla, Raveendra Kumar ^{[1
]}

机构：

[1] Tata Res Dev & Design Ctr, Pune, Maharashtra, India

来源：

TOOLS AND ALGORITHMS FOR THE CONSTRUCTION AND ANALYSIS OF SYSTEMS, TACAS 2018, PT II | 2018年 / 10806卷

关键词：

D O I：

10.1007/978-3-319-89963-3_32

中图分类号：

TP301 [理论、方法];

学科分类号：

081202 ;

摘要：

VeriAbs is a portfolio software verifier for ANSI-C programs. To prove properties with better efficiency and scalability, this version implements output abstraction with k-induction in the presence of resets. VeriAbs now generates post conditions over the abstraction to find invariants by applying Z3's tactics of quantifier elimination. These invariants are then used to generate validation witnesses. To find errors in the absence of known program bounds, VeriAbs searches for property violating inputs by applying random test generation with fuzz testing for a better scalability as compared to bounded model checking.

引用

页码：457 / 462

页数：6