ZenoTool, A Zeno Run detection tool for UPPAAL. ZenoTool is a small, fast command-line tool that analyzes model specifications of timed automata systems created with UPPAAL for the occurrence of Zeno Runs. Zeno Runs are paths in the timed transition system where infinite actions are executed in finite time. Since such behavior does not comply with real-world behavior, Zeno Runs often are unintentional. Moreover, timelocks, the counterpart to deadlocks in timed systems, may occur due to them.