Zur Seitenansicht


Systematic Predicate Abstraction using Variable Roles
Verfasser / Verfasserin Demyanova, Yulia ; Rümmer, Philipp ; Zuleger, Florian
Erschienen in
NASA Formal Methods - 9th International Symposium, NFM 2017, Moffett Field, CA, USA, May 16-18, 2017, Proceedings : Barrett, Clark; Davies, Misty; Kahsai, Temesghen, Cham, 2017, S. 265-281
SerieLecture Notes in Computer Science ; 10227
DokumenttypAufsatz in einem Sammelwerk
Projekt-/ReportnummerAustrian Science Fund (FWF): Austrian National Research Network S11403-N23 (RiSE)
URNurn:nbn:at:at-ubtuw:3-3639 Persistent Identifier (URN)
 Das Werk ist frei verfügbar
Systematic Predicate Abstraction using Variable Roles [0.36 mb]
Zusammenfassung (Englisch)

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 Eldaricas 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.

Das PDF-Dokument wurde 11 mal heruntergeladen.