Detail publikace

Template-Based Verification of Array-Manipulating Programs

MALÍK Viktor, SCHRAMMEL Peter a VOJNAR Tomáš. Template-Based Verification of Array-Manipulating Programs. In: Taming the Infinities of Concurrency . Lecture Notes in Computer Science, roč. 14660. Cham: Springer Nature Switzerland AG, 2024, s. 206-224. ISBN 978-3-031-56221-1. Dostupné z: https://link.springer.com/chapter/10.1007/978-3-031-56222-8_12
Název česky
Verifikace programů nad poli založená na šablonách
Typ
článek ve sborníku konference
Jazyk
angličtina
Autoři
Malík Viktor, Ing. (UITS FIT VUT)
Schrammel Peter, Dr. (US)
Vojnar Tomáš, prof. Ing., Ph.D. (UITS FIT VUT)
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, CH
DOI
10.1007/978-3-031-56222-8_12
UT WoS
001215137000011
EID Scopus
2-s2.0-85201185142
BibTeX 
@INPROCEEDINGS{FITPUB13332,
   author = "Viktor Mal\'{i}k and Peter Schrammel and Tom\'{a}\v{s} Vojnar",
   title = "Template-Based Verification of Array-Manipulating Programs",
   pages = "206--224",
   booktitle = "Taming the Infinities of Concurrency ",
   series = "Lecture Notes in Computer Science",
   volume = 14660,
   year = 2024,
   location = "Cham, CH",
   publisher = "Springer Nature Switzerland AG",
   ISBN = "978-3-031-56221-1",
   doi = "10.1007/978-3-031-56222-8\_12",
   language = "english",
   url = "https://www.fit.vut.cz/research/publication/13332"
}
Nahoru