RacerF is a static analyser for detection of data races in multi-threaded C programs with mutexes, implemented as a plugin of the Frama-C platform. The approach behind RacerF 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.
Z3-Noodler is an SMT solver for string constraints such as those that occur in symbolic execution and analysis of programs, reasoning about configuration files of cloud services and smart contracts, etc. Z3-Noodler is based on the SMT solver Z3 in which it replaces the solver for the theory of strings. The core of the string solver implements several decision procedures, but mainly it relies on the equation stabilization algorithm.