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