Wed 2 Jul 2025 12:09 - 12:30 at Auditorium M003 - Program Analysis and Verification Chair(s): Einar Broch Johnsen
We present RacerF, a novel static analyser for thread-modular data race detection. The approach behind RacerF exploits static analysis of sequential program behaviour whose results are generalised for multi-threaded programs using a combination of lightweight under- and over-approximating methods. The tool is implemented as a plugin of the Frama-C platform and can leverage several analysis backends, most notably the Frama-C’s abstract interpreter EVA. Although our methods are mostly heuristic without providing formal guarantees, our experimental evaluation shows that even for intricate programs, RacerF can provide very precise results competitive with more heavy-weight approaches while being faster than them.
Wed 2 JulDisplayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change
Wed 2 Jul
Displayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change
10:45 - 12:30 | Program Analysis and VerificationTechnical Papers at Auditorium M003 Chair(s): Einar Broch Johnsen University of Oslo | ||
10:45 21mTalk | Bottom-up Synthesis of Memory Mutations with Separation Logic Technical Papers | ||
11:06 21mTalk | Efficient Neural Network Verification via Order Leading Exploration of Branch-and-Bound Trees Technical Papers Guanqin Zhang University of New South Wales & CSIRO's Data61, Kota Fukuda Kyushu University, Zhenya Zhang Kyushu University, Japan, H M N Dilum Bandara Data61, CSIRO, Shiping Chen Data61 at CSIRO, Australia / UNSW, Australia, Jianjun Zhao Kyushu University, Yulei Sui University of New South Wales Link to publication Pre-print Media Attached | ||
11:27 21mTalk | IsaBIL: A Framework for Verifying (In)correctness of Binaries in Isabelle/HOL Technical Papers Matt Griffin Imperial College London, Brijesh Dongol University of Surrey, Azalea Raad Imperial College London | ||
11:48 21mTalk | Reusing Caches and Invariants for Efficient and Sound Incremental Static Analysis Technical Papers Mamy Razafintsialonina Université Paris-Saclay, CEA, List, Palaiseau / Sorbonne Université, CNRS, LIP6, Paris, David Bühler Université Paris-Saclay, CEA, List, Palaiseau, Antoine Miné Sorbonne Université, Valentin Perrelle Université Paris-Saclay, CEA, List, Palaiseau, Julien Signoles Université Paris-Saclay, CEA, List | ||
12:09 21mTalk | RacerF: Lightweight Static Data Race Detection for C Code Technical Papers Tomáš Dacík Faculty of Information Technology, Brno University of Technology, Tomas Vojnar Masaryk University |