Detail výsledku

Predator: A Verification Tool for Programs with Dynamic Linked Data Structures (Competition Contribution)

DUDKA, K.; MÜLLER, P.; PERINGER, P.; VOJNAR, T. Predator: A Verification Tool for Programs with Dynamic Linked Data Structures (Competition Contribution). Lecture Notes in Computer Science, 2012, vol. 2012, no. 7214, p. 544-547. ISSN: 0302-9743.
Typ
článek v časopise
Jazyk
anglicky
Autoři
Dudka Kamil, Ing., UITS (FIT)
Müller Petr, Ing., UITS (FIT)
Peringer Petr, Dr. Ing., UITS (FIT)
Vojnar Tomáš, prof. Ing., Ph.D., UITS (FIT)
Abstrakt

Predator is a tool for automated formal verification of sequential C programs with dynamic linked data structures. It is in principle based on separation logic, but uses a graph-based heap representation. This paper first provides a brief overview of Predator and then discusses experience with its participation in the Software Verification Competition of TACAS'12.

Klíčová slova

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

URL
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 (Competition Contribution)",
  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/"
}
Projekty
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
Pokročilé bezpečné, spolehlivé a adaptivní IT, VUT, Vnitřní projekty VUT, FIT-S-11-1, zahájení: 2011-01-01, ukončení: 2013-12-31, ukončen
Práce se složitými datovými strukturami a paralelismem v prostředí Rich Model Toolkit, MŠMT, COST, OC10009, zahájení: 2010-01-01, ukončení: 2012-12-31, řešení
Statická a dynamická verifikace programů s pokročilými rysy paralelismu a neomezenosti, GAČR, Standardní projekty, GAP103/10/0306, zahájení: 2010-01-01, ukončení: 2013-12-31, řešení
Výzkum informačních technologií z hlediska bezpečnosti, MŠMT, Institucionální prostředky SR ČR (např. VZ, VC), MSM0021630528, zahájení: 2007-01-01, ukončení: 2013-12-31, řešení
Výzkumné skupiny
Výzkumná skupina automatizované analýzy a verifikace - VeriFIT (VZ VERIFIT)
Pracoviště
Ústav inteligentních systémů (UITS)
Nahoru