Result Details

Generalised Multi-Pattern-Based Verification of Programs with Linear Linked Structures

ERLEBACH, P.; ČEŠKA, M.; VOJNAR, T. Generalised Multi-Pattern-Based Verification of Programs with Linear Linked Structures. FORMAL ASPECTS OF COMPUTING, 2007, vol. 19, no. 3, p. 363-374. ISSN: 0934-5043.
Type
journal article
Language
English
Authors
Erlebach Pavel, Ing., Ph.D., DITS (FIT)
Češka Milan, prof. RNDr., CSc., DITS (FIT)
Vojnar Tomáš, prof. Ing., Ph.D., DITS (FIT)
Abstract

The paper deals with the problem of automatic verification of programsworking with extended linear linked dynamic data structures, inparticular, pattern-based verification is considered. In this approach,one can abstract memory configurations by abstracting away the exactnumber of adjacent occurrences of certain memory patterns. With respectto the previous work on the subject the method presented in the paperhas been extended to be able to handle multiple patterns, which allowsfor verification of programs working with more types of structuresand/or with structures with irregular shapes. The experimental resultsobtained from a prototype implementation of the method show that themethod is very competitive and offers a big potential for futureextensions.

Keywords

formal verification, program analysis, shape analysis, dynamic linked data structures

URL
Published
2007
Pages
363–374
Journal
FORMAL ASPECTS OF COMPUTING, vol. 19, no. 3, ISSN 0934-5043
BibTeX 
@article{BUT45155,
  author="Pavel {Erlebach} and Milan {Češka} and Tomáš {Vojnar}",
  title="Generalised Multi-Pattern-Based Verification of Programs with Linear Linked Structures",
  journal="FORMAL ASPECTS OF COMPUTING",
  year="2007",
  volume="19",
  number="3",
  pages="363--374",
  issn="0934-5043",
  url="http://www.springerlink.com/content/47472236k6213t7l/"
}
Projects
Advanced Formal Approaches in the Design and Verification of Computer-Based Systems, GACR, Standardní projekty, GA102/07/0322, start: 2007-01-01, end: 2009-12-31, completed
Advanced Methods of Automatic Verification of Parametric and Infinite-State Systems, GACR, Postdoktorandské granty, GP102/03/D211, start: 2003-09-01, end: 2006-09-01, completed
Integrated approach to education of PhD students in the area of parallel and distributed systems, GACR, Doktorské granty, GD102/05/H050, start: 2005-01-01, end: 2008-12-31, completed
Security-Oriented Research in Information Technology, MŠMT, Institucionální prostředky SR ČR (např. VZ, VC), MSM0021630528, start: 2007-01-01, end: 2013-12-31, running
Research groups
Automated Analysis and Verification Research Group - VeriFIT (RG VERIFIT)
Departments
Department of Intelligent Systems (DITS)
Back to top