Generalised multi-pattern-based verification of programs with linear linked structures |
| |
Authors: | Milan Češka Pavel Erlebach Tomáš Vojnar |
| |
Affiliation: | (1) FIT, Brno University of Technology, Božetěchova 2, 61266 Brno, Czech Republic |
| |
Abstract: | The paper deals with the problem of automatic verification of programs working with extended linear linked dynamic data structures,
in particular, pattern-based verification is considered. In this approach, one can abstract memory configurations by abstracting
away the exact number of adjacent occurrences of certain memory patterns. With respect to the previous work on the subject
the method presented in the paper has been extended to be able to handle multiple patterns, which allows for verification
of programs working with more types of structures and/or with structures with irregular shapes. The experimental results obtained
from a prototype implementation of the method show that the method is very competitive and offers a big potential for future
extensions. |
| |
Keywords: | Formal verification Program analysis Dynamic linked data structures |
本文献已被 SpringerLink 等数据库收录! |
|