Paper Info
Title
Counter-Example Guided Program Verification.
Abstract
This paper presents a novel counter-example guided abstraction refinement algorithm for the automatic verification of concurrent programs. Our algorithm proceeds in different steps. It first constructs an abstraction of the original program by slicing away a given subset of variables. Then, it uses an external model checker as a backend tool to analyze the correctness of the abstract program. If the model checker returns that the abstract program is safe then we conclude that the original one is also safe. If the abstract program is unsafe, we extract an "abstract" counter-example. In order to check if the abstract counter-example can lead to a real counter-example of the original program, we add back to the abstract counter-example all the omitted variables (that have been sliced away) to obtain a new program. Then, we call recursively our algorithm on the new obtained program. If the recursive call of our algorithm returns that the new program is unsafe, then we can conclude that the original program is also unsafe and our algorithm terminates. Otherwise, we refine the abstract program by removing the abstract counter-example from its set of possible runs. Finally, we repeat the procedure with the refined abstract program. We have implemented our algorithm, and run it successfully on the concurrency benchmarks in SV-COMP15. Our experimental results show that our algorithm significantly improves the performance of the backend tool.
Year
DOI
Venue
2016
10.1007/978-3-319-48989-6_2
Lecture Notes in Computer Science
Field
DocType
Volume
Model checking,Abstraction,Computer science,Concurrency,Correctness,Slicing,Theoretical computer science,Counterexample,Dependency graph,Recursion
Conference
9995
ISSN
Citations 
PageRank 
0302-9743
0
0.34
References 
Authors
9
3
Name
Order
Citations
PageRank
Parosh Aziz Abdulla12010122.22
Mohamed Faouzi Atig250540.94
Bui Phi Diep3101.85