Sliced Path Prefixes: An Effective Method to Enable Refinement Selection - Formal Techniques for Distributed Objects, Components, and Systems
Conference Papers Year : 2015

Sliced Path Prefixes: An Effective Method to Enable Refinement Selection

Dirk Beyer
  • Function : Author
Stefan Löwe
  • Function : Author
  • PersonId : 1030894

Abstract

Automatic software verification relies on constructing, for a given program, an abstract model that is (1) abstract enough to avoid state-space explosion and (2) precise enough to reason about the specification. Counterexample-guided abstraction refinement is a standard technique that suggests to extract information from infeasible error paths, in order to refine the abstract model if it is too imprecise. Existing approaches —including our previous work— do not choose the refinement for a given path systematically. We present a method that generates alternative refinements and allows to systematically choose a suited one. The method takes as input one given infeasible error path and applies a slicing technique to obtain a set of new error paths that are more abstract than the original error path but still infeasible, each for a different reason. The (more abstract) constraints of the new paths can be passed to a standard refinement procedure, in order to obtain a set of possible refinements, one for each new path. Our technique is completely independent from the abstract domain that is used in the program analysis, and does not rely on a certain proof technique, such as SMT solving. We implemented the new algorithm in the verification framework CPAchecker and made our extension publicly available. The experimental evaluation of our technique indicates that there is a wide range of possibilities on how to refine the abstract model for a given error path, and we demonstrate that the choice of which refinement to apply to the abstract model has a significant impact on the verification effectiveness and efficiency.
Fichier principal
Vignette du fichier
978-3-319-19195-9_15_Chapter.pdf (849.09 Ko) Télécharger le fichier
Origin Files produced by the author(s)
Loading...

Dates and versions

hal-01767324 , version 1 (16-04-2018)

Licence

Identifiers

Cite

Dirk Beyer, Stefan Löwe, Philipp Wendler. Sliced Path Prefixes: An Effective Method to Enable Refinement Selection. 35th International Conference on Formal Techniques for Distributed Objects, Components, and Systems (FORTE), Jun 2015, Grenoble, France. pp.228-243, ⟨10.1007/978-3-319-19195-9_15⟩. ⟨hal-01767324⟩
119 View
92 Download

Altmetric

Share

More