Data Race Detection with Frama-C (Competition Contribution)

D 2025

Data Race Detection with Frama-C (Competition Contribution)

DACÍK, Tomáš a Tomáš VOJNAR

Základní údaje

Originální název

Data Race Detection with Frama-C (Competition Contribution)

Autoři

DACÍK, Tomáš a Tomáš VOJNAR

Vydání

Cham, Proc. of 31st International Conference on Tools and Algorithms for the Construction and Analysis of Systems – TACAS'25 as a competition contribution within the 14th International Competition on Software Verification – SV-COMP'25, od s. 248-253, 6 s. 2025

Nakladatel

Springer

Další údaje

Jazyk

angličtina

Typ výsledku

Stať ve sborníku

Obor

10201 Computer sciences, information science, bioinformatics

Stát vydavatele

Švýcarsko

Utajení

není předmětem státního či obchodního tajemství

Forma vydání

tištěná verze "print"

Odkazy

Publisher's webpage, The RacerF tool, Associated technical report

Impakt faktor

Impact factor: 0.402 v roce 2005

Označené pro přenos do RIV

Ano

Organizační jednotka

Fakulta informatiky

ISBN

978-3-031-90659-6

ISSN

DOI

https://doi.org/10.1007/978-3-031-90660-2_20

EID Scopus

2-s2.0-105004792086

Klíčová slova anglicky

program analysis; static analysis; concurrent programs; data races

Příznaky

Mezinárodní význam, Recenzováno

Změněno: 1. 4. 2026 11:05, RNDr. Pavel Šmerk, Ph.D.

Anotace

V originále

RACERF is a static analyser for detection of data races in multithreaded C programs implemented as a plugin of the Frama-C platform. The approach behind RACERF is mostly heuristic and relies on analysis of the sequential behaviour of particular threads whose results are generalised using a combination of under- and over-approximating techniques to allow analysis of the multithreading behaviour. In particular, in SV-COMP’25, RACERF relies on the Frama-C’s abstract interpreter EVA to perform the analysis of the sequential behaviour. Although RACERF does not provide any formal guarantees, it ranked second in the NoDataRace-Main sub-category, providing the largest number of correct results (when excluding metaverifiers) and just 4 false positives.

Návaznosti

GA23-06506S, projekt VaV

Název: Pokročilá analýza a verifikace pro pokročilý software

Investor: Grantová agentura ČR, Pokročilá analýza a verifikace pro pokročilý software

Citovat

DACÍK, Tomáš a Tomáš VOJNAR. Data Race Detection with Frama-C (Competition Contribution). In Proc. of 31st International Conference on Tools and Algorithms for the Construction and Analysis of Systems – TACAS'25 as a competition contribution within the 14th International Competition on Software Verification – SV-COMP'25. Cham: Springer, 2025, s. 248-253. ISBN 978-3-031-90659-6. Dostupné z: https://doi.org/10.1007/978-3-031-90660-2_20.

@inproceedings{2512081,
   author = {Dacík, Tomáš and Vojnar, Tomáš},
   address = {Cham},
   booktitle = {Proc. of 31st International Conference on Tools and Algorithms for the Construction and Analysis of Systems – TACAS'25 as a competition contribution within the 14th International Competition on Software Verification – SV-COMP'25},
   doi = {https://doi.org/10.1007/978-3-031-90660-2_20},
   keywords = {program analysis; static analysis; concurrent programs; data races},
   howpublished = {tištěná verze "print"},
   language = {eng},
   location = {Cham},
   isbn = {978-3-031-90659-6},
   pages = {248-253},
   publisher = {Springer},
   title = {Data Race Detection with Frama-C (Competition Contribution)},
   url = {https://github.com/TDacik/Deadlock_and_Racer},
   year = {2025}
}

TY  - CONF
ID  - 2512081
AU  - Dacík, Tomáš - Vojnar, Tomáš
PY  - 2025
TI  - Data Race Detection with Frama-C (Competition Contribution)
PB  - Springer
CY  - Cham
SN  - 9783031906596
KW  - program analysis
KW  - static analysis
KW  - concurrent programs
KW  - data races
UR  - https://github.com/TDacik/Deadlock_and_Racer
N2  - RACERF is a static analyser for detection of data races in multithreaded C programs implemented as a plugin of the Frama-C platform. The approach behind RACERF is mostly heuristic and relies on analysis of the sequential behaviour of particular threads whose results are generalised using a combination of under- and over-approximating techniques to allow analysis of the multithreading behaviour. In particular, in SV-COMP’25, RACERF relies on the Frama-C’s abstract interpreter EVA to perform the analysis of the sequential behaviour. Although RACERF does not provide any formal guarantees, it ranked second in the NoDataRace-Main sub-category, providing the largest number of correct results (when excluding metaverifiers) and just 4 false positives.
ER  -

DACÍK, Tomáš a Tomáš VOJNAR. Data Race Detection with Frama-C (Competition Contribution). In \textit{Proc. of 31st International Conference on Tools and Algorithms for the Construction and Analysis of Systems – TACAS'25 as a competition contribution within the 14th International Competition on Software Verification – SV-COMP'25}. Cham: Springer, 2025, s.~248-253. ISBN~978-3-031-90659-6. Dostupné z: https://doi.org/10.1007/978-3-031-90660-2\_{}20.

Přehled o publikaci