Detail výsledku

CPAlien: Shape Analyzer for CPAChecker (Competition Contribution)

MÜLLER, P.; VOJNAR, T. CPAlien: Shape Analyzer for CPAChecker (Competition Contribution). 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.
Typ
článek ve sborníku konference
Jazyk
anglicky
Autoři
Müller Petr, Ing., UITS (FIT)
Vojnar Tomáš, prof. Ing., Ph.D., UITS (FIT)
Abstrakt


CPALien is a configurable program analysis framework instance. It
uses an extension of the symbolic memory graphs (SMGs) abstract domain for
shape analysis of programs manipulating the heap. In particular, CPAlien ex-
tends SMGs with a simple integer value analysis in order to handle programs
with both pointers and integer data. The current version of CPAlien is an early
prototype intended as a basis for a future research in the given area. The version
submitted for SV-COMP'14 does not contain any shape abstraction, but it is still powerful enough to participate in several categories.

Klíčová slova

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

URL
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
Konference
European Joint Conferences on Theory and Practice of Software -- ETAPS'14 (TACAS'14)
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 (Competition Contribution)",
  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"
}
Projekty
Automatizovaná formální analýza a verifikace programů se složitými datovými a řídicími strukturami s předem neomezenou velikostí, GAČR, Standardní projekty, GA14-11384S, zahájení: 2014-01-01, ukončení: 2016-12-31, ukončen
Centrum excelence IT4Innovations, MŠMT, Operační program Výzkum a vývoj pro inovace, ED1.1.00/02.0070, zahájení: 2011-01-01, ukončení: 2015-12-31, ukončen
Verifikace a optimalizace počítačových systémů, VUT, Vnitřní projekty VUT, FIT-S-12-1, zahájení: 2012-01-01, ukončení: 2014-12-31, ukončen
Výzkumné skupiny
Výzkumná skupina automatizované analýzy a verifikace - VeriFIT (VZ VERIFIT)
Pracoviště
Ústav inteligentních systémů (UITS)
Nahoru