Result Details

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

DACÍK, T.; VOJNAR, T. 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. Hamilton: Springer Nature Switzerland AG, 2025. p. 248-253. ISBN: 978-3-031-90659-6.
Type
conference paper
Language
English
Authors
Dacík Tomáš, Ing., DITS (FIT)
Vojnar Tomáš, prof. Ing., Ph.D., DITS (FIT)
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.

Keywords

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

URL
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
ISBN
978-3-031-90659-6
Publisher
Springer Nature Switzerland AG
Place
Hamilton
DOI
10.1007/978-3-031-90660-2_20
EID Scopus
2-s2.0-105004792086
BibTeX 
@inproceedings{BUT198081,
  author="Tomáš {Dacík} and Tomáš {Vojnar}",
  title="RacerF: Data Race Detection with Frama-C (Competition Contribution)",
  booktitle="Proceedings of the 31st International Conference on Tools and Algorithms for the Construction and Analysis of Systems, part 3",
  year="2025",
  series="Lecture Notes in Computer Science",
  volume="15698",
  pages="248--253",
  publisher="Springer Nature Switzerland AG",
  address="Hamilton",
  doi="10.1007/978-3-031-90660-2\{_}20",
  isbn="978-3-031-90659-6",
  url="https://link.springer.com/content/pdf/10.1007/978-3-031-90660-2_20.pdf"
}
Projects
Advanced Analysis and Verification for Advanced Software, GACR, Standardní projekty, GA23-06506S, start: 2023-01-01, end: 2025-12-31, running
Reliable, Secure, and Intelligent Computer Systems, BUT, Vnitřní projekty VUT, FIT-S-23-8151, start: 2023-03-01, end: 2026-02-28, running
Verification and Analysis for Safety and Security of Applications in Life, EU, HORIZON EUROPE, SEP-210979090, start: 2024-06-01, end: 2027-05-31, running
Departments
Department of Intelligent Systems (DITS)
Back to top