Detail publikace

CPAlien: Shape Analyzer for CPAChecker

MÜLLER, P.; VOJNAR, T. CPAlien: Shape Analyzer for CPAChecker. In Tools and Algorithms for the Construction and Analysis of Systems. Lecture Notes in Computer Science. Heidelberg: Springer Verlag, 2014. p. 395-397. ISBN: 978-3-642-54861-1.
Název česky
CPAlien: Analyzátor tvaru pro framework CPAChecker
Typ
článek ve sborníku konference
Jazyk
anglicky
Autoři
Müller Petr, Ing.
Vojnar Tomáš, prof. Ing., Ph.D. (UITS)
URL
Klíčová slova

shape analysis configurable program analysis static analysis symbolic memory graphs memory safety software verification

Abstrakt

CPAlien je instance frameworku konfigurovatelné analýzy programů. Používá rozšířenou abstraktní doménu symbolických grafů paměti k analýze tvarů pro programy pracující s dynamicky alokovanou pamětí. Rozšíření abstraktní domény symbolických grafů paměti spočívá v použití jednoduché analýzy celočíselných hodnot, což umožňuje zvládnutí programů pracujících zároveň s ukazateli a s celočíselnými daty. V současnosti je CPAlien ve stavu prototypu, jako základ pro další výzkum v dané oblasti. Verze pro SV-COMP'14 neobsahuje žádné abstrakce tvaru, ale přesto je uspokojivě výkonná pro účast v několika soutěžních kategoriích.

Rok
2014
Strany
395–397
Sborník
Tools and Algorithms for the Construction and Analysis of Systems
Řada
Lecture Notes in Computer Science
Svazek
8413
ISBN
978-3-642-54861-1
Vydavatel
Springer Verlag
Místo
Heidelberg
DOI
10.1007/978-3-642-54862-8_28
EID Scopus
2-s2.0-84900537327
BibTeX 
@inproceedings{BUT111527,
  author="Petr {Müller} and Tomáš {Vojnar}",
  title="CPAlien: Shape Analyzer for CPAChecker",
  booktitle="Tools and Algorithms for the Construction and Analysis of Systems",
  year="2014",
  series="Lecture Notes in Computer Science",
  volume="8413",
  pages="395--397",
  publisher="Springer Verlag",
  address="Heidelberg",
  doi="10.1007/978-3-642-54862-8\{_}28",
  isbn="978-3-642-54861-1",
  url="http://link.springer.com/chapter/10.1007/978-3-642-54862-8_28"
}
Nahoru