Skip to Main content Skip to Navigation
Conference papers

Sliced Path Prefixes: An Effective Method to Enable Refinement Selection

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.
Complete list of metadata

Cited literature [22 references]  Display  Hide  Download

https://hal.inria.fr/hal-01767324
Contributor : Hal Ifip <>
Submitted on : Monday, April 16, 2018 - 10:18:35 AM
Last modification on : Monday, April 16, 2018 - 10:20:27 AM

File

978-3-319-19195-9_15_Chapter.p...
Files produced by the author(s)

Licence


Distributed under a Creative Commons Attribution 4.0 International License

Identifiers

Citation

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⟩

Share

Metrics

Record views

391

Files downloads

201