Publication Details

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

DACÍK Tomáš and 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, vol. 15698. Hamilton: Springer Nature Switzerland AG, 2025, pp. 248-253. ISBN 978-3-031-90659-6. Available from: https://link.springer.com/content/pdf/10.1007/978-3-031-90660-2_20.pdf
Czech title
RacerF: Detekce souběhů nad daty s pomocí Frama-C (příspěvek do soutěže)
Type
conference paper
Language
english
Authors
Dacík Tomáš, Ing. (DITS FIT BUT)
Vojnar Tomáš, prof. Ing., Ph.D. (DITS FIT BUT)
URL
Keywords

data race, data race detection, static analysis, program verification, SV-COMP

Abstract

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.

Published
2025
Pages
248-253
Proceedings
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
Conference
31st International Conference on Tools and Algorithms for the Construction and Analysis of Systems --- TACAS'25, Hamilton, CA
ISBN
978-3-031-90659-6
Publisher
Springer Nature Switzerland AG
Place
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"
}
Back to top