Mufin–Runtime Monitoring with Union-Find Structures

Tagged runtime-verification, uni

Mufin is a tool that implements a runtime monitoring algorithm that can efficiently track properties that take hierarchical relationships of objects into account.

Using the union-find data structure, it can perform updates for multiple tracked objects simultaneously. It won the Java Track of the International Runtime Verification Competition 2016.

I contributed to the design of the final algorithm used and wrote an efficient implementation targeting the JVM. More information can be found on the official project page and in the corresponding paper.