Paper Info
Title
Heuristic-guided abstraction refinement for concurrent systems
Abstract
Predicate abstraction is an established technique in software verification. It inherently includes an abstraction refinement loop successively adding predicates until the right level of abstraction is found. For concurrent systems, predicate abstraction can be combined with spotlight abstraction, further reducing the state space by abstracting away certain processes. Refinement then has to decide whether to add a new predicate or a new process. Selecting the right predicates and processes is a crucial task: The positive effect of abstraction may be compromised by unfavourable refinement decisions. Here we present a heuristic approach to abstraction refinement. The basis for a decision is a set of refinement candidates, derived by multiple counterexample-generation. Candidates are evaluated with respect to their influence on other components in the system. Experimental results show that our technique can significantly speed up verification as compared to a naive abstraction refinement.
Year
DOI
Venue
2012
10.1007/978-3-642-34281-3_25
ICFEM
Keywords
Field
DocType
new predicate,unfavourable refinement decision,spotlight abstraction,concurrent system,naive abstraction refinement,abstraction refinement loop,predicate abstraction,new process,heuristic-guided abstraction refinement,established technique,refinement candidate,right predicate
Kripke structure,Abstraction model checking,Heuristic,Abstraction,Programming language,Refinement calculus,Predicate abstraction,Computer science,Theoretical computer science,Abstraction inversion,Software verification
Conference
Citations 
PageRank 
References 
3
0.43
22
Authors
3
Name
Order
Citations
PageRank
Nils Timm1101.29
Heike Wehrheim21013104.85
Mike Czech340.78