Title: Systematic Predicate Abstraction using Variable Roles
Language: English
Authors: Demyanova, Yulia 
Rümmer, Philipp 
Zuleger, Florian
Issue Date: 2017
Abstract: 
Heuristics for discovering predicates for abstraction are an essential part of software model checkers. Picking the right predicates affects the runtime of a model checker, or determines if a model checker is able to solve a verification task at all. In this paper we present a method to systematically specify heuristics for generating program-specific abstractions. The heuristics can be used to generate initial abstractions, and to guide abstraction refinement through templates provided for Craig interpolation. We describe the heuristics using variable roles, which allow us to pick domain-specific predicates according to the program under analysis. Variable roles identify typical variable usage patterns and can be computed using lightweight static analysis, for instance with the help of off-the-shelf logical programming engines. We implemented a prototype tool which extracts initial predicates and templates for C programs and passes them to the Eldarica model checker in the form of source code annotations. For evaluation, we defined a set of heuristics, motivated by Eldarica’s previous built-in heuristics and typical verification benchmarks from the literature and SV-COMP. We evaluate our approach on a set of more than 500 programs, and observe an overall increase in the number of solved tasks by 11.2%, and significant speedup on certain benchmark families.
URI: https://resolver.obvsg.at/urn:nbn:at:at-ubtuw:3-3639
http://hdl.handle.net/20.500.12708/909
Library ID: AC15093558
ISBN: 9783319572871
Organisation: E192 - Institut für Logic and Computation 
Publication Type: Inproceedings
Konferenzbeitrag
Appears in Collections:Conference Paper

Files in this item:


Page view(s)

43
checked on Jul 11, 2021

Download(s)

185
checked on Jul 11, 2021

Google ScholarTM

Check


Items in reposiTUm are protected by copyright, with all rights reserved, unless otherwise indicated.