ECOOP 2025
Mon 30 June - Fri 4 July 2025 Bergen, Norway
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 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
21m
Talk
Bottom-up Synthesis of Memory Mutations with Separation Logic
Technical Papers
Kasra Ferdowsi University of California at San Diego, Hila Peleg Technion
11:06
21m
Talk
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
21m
Talk
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
21m
Talk
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
21m
Talk
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
:
:
:
: