uu.seUppsala University Publications
Change search
ReferencesLink to record
Permanent link

Direct link
Counter-Example Guided Program Verification
Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Computer Systems.
Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Computer Systems.
Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Computer Systems.
2016 (English)In: FM 2016: Formal Methods - 21st International Symposium, Limassol, Cyprus, November 9-11, 2016, Proceedings / [ed] John Fitzgerald, Constance Heitmeyer, Stefania Gnesi, Anna Philippou, Springer Berlin/Heidelberg, 2016, Vol. 9995, 25-42 p.Conference paper (Refereed)
Abstract [en]

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.

Place, publisher, year, edition, pages
Springer Berlin/Heidelberg, 2016. Vol. 9995, 25-42 p.
Series
Lecture Notes in Computer Science, ISSN 0302-9743 ; 9995
National Category
Computer Systems
Identifiers
URN: urn:nbn:se:uu:diva-307789DOI: 10.1007/978-3-319-48989-6_2ISBN: 978-3-319-48988-9 (Print)ISBN: 978-3-319-48989-6 (PDF)OAI: oai:DiVA.org:uu-307789DiVA: diva2:1048404
Conference
FM 2016: Formal Methods - 21st International Symposium, November 9-11, 2016, Limassol, Cyprus
Available from: 2016-11-21 Created: 2016-11-21 Last updated: 2017-01-18Bibliographically approved

Open Access in DiVA

No full text

Other links

Publisher's full textProceedings

Search in DiVA

By author/editor
Abdulla, Parosh AzizAtig, Mohamed FaouziBui, Phi Diep
By organisation
Computer Systems
Computer Systems

Search outside of DiVA

GoogleGoogle Scholar

Altmetric score

Total: 56 hits
ReferencesLink to record
Permanent link

Direct link