  In recent years there has been a considerable effort in optimising formal
methods for application to code. This has been driven by tools such as
CPAChecker, DIVINE, and CBMC. At the same time tools such as Uppaal have been
massively expanding the realm of more traditional model checking technologies
to include strategy synthesis algorithms - an aspect becoming more and more
needed as software becomes increasingly parallel. Instead of reimplementing the
advances made by Uppaal in this area, we suggest in this paper to develop a
bridge between the source code and the engine of Uppaal. Our approach uses the
widespread intermediate language LLVM and makes recent advances of the Uppaal
ecosystem readily available to analysis of source code.
