Detail publikace

Template-Based Verification of Array-Manipulating Programs

MALÍK, V.; VOJNAR, T.; SCHRAMMEL, P. Template-Based Verification of Array-Manipulating Programs. In Taming the Infinities of Concurrency. Lecture Notes in Computer Science. Cham: Springer Nature Switzerland AG, 2024. p. 206-224. ISBN: 978-3-031-56221-1.
Název česky
Verifikace programů nad poli založená na šablonách
Typ
článek ve sborníku konference
Jazyk
anglicky
Autoři
Malík Viktor, Ing., Ph.D. (UITS)
Vojnar Tomáš, prof. Ing., Ph.D. (UITS)
Schrammel Peter
URL
Klíčová slova

analýza programů, formální verifikace, odvozování invariantů, invarianty smyček,
abstraktní interpretace, k-indukce, rozbalování smyček, abstraktní doména pro
pole, analýza obsahu polí

Abstrakt

Tato práce se zabývá rámcem pro verifikaci programů 2LS, který kombinuje několik
verifikačních technik - konkrétně abstraktní domény, šablonové invarianty,
k-indukci, omezený model checking a řešení SAT/SMT. Charakteristickým rysem
přístupu používaného v 2LS je, že umožňuje bezproblémové kombinace různých
programových abstrakcí. V této práci zavádíme novou abstraktní šablonovou doménu
umožňující 2LS usuzovat o polích, přičemž k popisu hodnot, které jsou uloženy
uvnitř polí (včetně vnořených polí a dynamicky propojených datových struktur),
používáme libovolnou abstraktní doménu a pole jsou případně vnořena uvnitř jiných
struktur. Navržený přístup používá indexy polí k rozdělení každého pole na více
sousedících, nepřekrývajících se segmentů a pro každý z nich počítá jiný
invariant. Přístup ilustrujeme na programu pracujícím se seznamem polí a následně
představíme, jak nová doména umožnila 2LS zlepšit se v mezinárodní soutěži ve
verifikaci softwaru SV-COMP.

Rok
2024
Strany
206–224
Sborník
Taming the Infinities of Concurrency
Řada
Lecture Notes in Computer Science
Svazek
14660
Konference
European Joint Conferences on Theory and Practice of Software -- ETAPS'24 (TACAS'24), Centre for Security, Reliability and Trust (SnT), University of Luxembourg., LU
ISBN
978-3-031-56221-1
Vydavatel
Springer Nature Switzerland AG
Místo
Cham
DOI
10.1007/978-3-031-56222-8_12
UT WoS
001215137000011
EID Scopus
2-s2.0-85201185142
BibTeX 
@inproceedings{BUT193768,
  author="Viktor {Malík} and Tomáš {Vojnar} and Peter {Schrammel}",
  title="Template-Based Verification of Array-Manipulating Programs",
  booktitle="Taming the Infinities of Concurrency",
  year="2024",
  series="Lecture Notes in Computer Science",
  volume="14660",
  pages="206--224",
  publisher="Springer Nature Switzerland AG",
  address="Cham",
  doi="10.1007/978-3-031-56222-8\{_}12",
  isbn="978-3-031-56221-1",
  url="https://link.springer.com/chapter/10.1007/978-3-031-56222-8_12"
}
Nahoru