Detail publikace

RacerF: Data Race Detection with Frama-C (Competition Contribution)

DACÍK Tomáš a VOJNAR Tomáš. RacerF: Data Race Detection with Frama-C (Competition Contribution). In: Proceedings of the 31st International Conference on Tools and Algorithms for the Construction and Analysis of Systems, part 3. Lecture Notes in Computer Science, roč. 15698. Hamilton: Springer Nature Switzerland AG, 2025, s. 248-253. ISBN 978-3-031-90659-6. Dostupné z: https://link.springer.com/content/pdf/10.1007/978-3-031-90660-2_20.pdf
Název česky
RacerF: Detekce souběhů nad daty s pomocí Frama-C (příspěvek do soutěže)
Typ
článek ve sborníku konference
Jazyk
angličtina
Autoři
Dacík Tomáš, Ing. (UITS FIT VUT)
Vojnar Tomáš, prof. Ing., Ph.D. (UITS FIT VUT)
URL
Klíčová slova

souběh nad daty, detekce souběhů nad daty, statická analýza, verifikace programů, SV-COMP

Abstrakt

RacerF je statický analyzátor pro detekci souběhů nad daty ve vícevláknových C programech, implementovaný jako plugin platformy Frama-C. Náš přístup je založen na heuristických metodách využívajících analýzu sekvenčního chování jednotlivých vláken, jehož výsledek je následně zobecněn za použití pod- a nad-aproximace vícevláknového chování. V soutěži SV-COMP'25 RacerF využívá abstraktní interpret EVA pro analýzu sekvenčního chování vláken. Přestože náš přístup neposkytuje formální záruky, RacerF se umístil na druhém místě v kategorii NoDataRace-Main, kde navíc dosáhl největšího počtu správných výsledků (mimo metaverifikátory) a pouze čtyř nesprávně nahlášených chyb.

Rok
2025
Strany
248-253
Sborník
Proceedings of the 31st International Conference on Tools and Algorithms for the Construction and Analysis of Systems, part 3
Řada
Lecture Notes in Computer Science
Svazek
15698
Konference
31st International Conference on Tools and Algorithms for the Construction and Analysis of Systems --- TACAS'25, Hamilton, CA
ISBN
978-3-031-90659-6
Vydavatel
Springer Nature Switzerland AG
Místo
Hamilton, CA
DOI
10.1007/978-3-031-90660-2_20
EID Scopus
2-s2.0-105004792086
BibTeX 
@INPROCEEDINGS{FITPUB13525,
   author = "Tom\'{a}\v{s} Dac\'{i}k and Tom\'{a}\v{s} Vojnar",
   title = "RacerF: Data Race Detection with Frama-C (Competition Contribution)",
   pages = "248--253",
   booktitle = "Proceedings of the 31st International Conference on Tools and Algorithms for the Construction and Analysis of Systems, part 3",
   series = "Lecture Notes in Computer Science",
   volume = 15698,
   year = 2025,
   location = "Hamilton, CA",
   publisher = "Springer Nature Switzerland AG",
   ISBN = "978-3-031-90659-6",
   doi = "10.1007/978-3-031-90660-2\_20",
   language = "english",
   url = "https://www.fit.vut.cz/research/publication/13525"
}
Nahoru