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

共 12 条

[1] [Anonymous], 2013, ESEC FSE
[2] [Anonymous], DATE
[3] [Anonymous], 2011, P 4 ANN IND SOFTW EN, DOI DOI 10.1145/1953355.1953368
[4] [Anonymous], TOOLS ALGORITHMS CON
[5] Beyer Dirk, 2011, Computer Aided Verification. Proceedings 23rd International Conference, CAV 2011, P184, DOI 10.1007/978-3-642-22110-1_16
[6] Coverage-Based Greybox Fuzzing as Markov Chain
Bohme, Marcel
Van-Thuan Pham
Roychoudhury, Abhik
[J]. IEEE TRANSACTIONS ON SOFTWARE ENGINEERING, 2019, 45 (05) : 489 - 506
[7] A tool for checking ANSI-C programs
Clarke, E
Kroening, D
Lerda, F
[J]. TOOLS AND ALGORITHMS FOR THE CONSTRUCTION AND ANALYSIS OF SYSTEMS, PROCEEDINGS, 2004, 2988 : 168 - 176
[8] Precise Analysis of Large Industry Code
Darke, Priyanka
Khanzode, Mayur
Nair, Arun
Shrotri, Ulka
Venkatesh, R.
[J]. 2012 19TH ASIA-PACIFIC SOFTWARE ENGINEERING CONFERENCE (APSEC), VOL 1, 2012, : 306 - 309
[9] Z3: An efficient SMT solver
de Moura, Leonardo
Bjorner, Nikolaj
[J]. TOOLS AND ALGORITHMS FOR THE CONSTRUCTION AND ANALYSIS OF SYSTEMS, 2008, 4963 : 337 - 340
[10] An extensible SAT-solver
Eén, N
Sörensson, N
[J]. THEORY AND APPLICATIONS OF SATISFIABILITY TESTING, 2004, 2919 : 502 - 518

← 1 2 →