Detail publikace

Predator: A Verification Tool for Programs with Dynamic Linked Data Structures

DUDKA, K.; MÜLLER, P.; PERINGER, P.; VOJNAR, T. Predator: A Verification Tool for Programs with Dynamic Linked Data Structures. Lecture Notes in Computer Science, 2012, vol. 2012, no. 7214, p. 544-547. ISSN: 0302-9743.
Název česky
Predator: Nástroj pro verifikaci programů s dynamickými datovými strukturami
Typ
článek v časopise
Jazyk
anglicky
Autoři
Dudka Kamil, Ing.
Müller Petr, Ing.
Peringer Petr, Dr. Ing. (UITS)
Vojnar Tomáš, prof. Ing., Ph.D. (UITS)
URL
Klíčová slova

separation logic, shape analysis, dynamic linked data structures, pointers, linked lists, tool support, formal verification, Linux lists, Competition on Software Verification

Abstrakt

Predator je nástroj pro automatickou formální verifikaci sekvenčních programů v jazyce C s dynamickými datovými strukturami. Tento nástroj je založený na principech separační logiky, ale používá grafovou reprezentaci hromady. V tomto článku je stručně představen nástroj Predator a dále jsou popsány zkušenosti z jeho účastí na soutěži Competition on Software Verification, která je pořádána ve spojení s konferencí TACAS'12.

Rok
2012
Strany
544–547
Časopis
Lecture Notes in Computer Science, roč. 2012, č. 7214, ISSN 0302-9743
BibTeX 
@article{BUT91458,
  author="Kamil {Dudka} and Petr {Müller} and Petr {Peringer} and Tomáš {Vojnar}",
  title="Predator: A Verification Tool for Programs with Dynamic Linked Data Structures",
  journal="Lecture Notes in Computer Science",
  year="2012",
  volume="2012",
  number="7214",
  pages="544--547",
  issn="0302-9743",
  url="http://www.springerlink.com/content/5x4748456031r18x/"
}
Nahoru