Home | Publications

Movec is an automated tool for runtime MOnitoring, VErification and Control of C programs as an extension to the C programming language. Movec provides a source-to-source transformation that statically analyzes input C programs and generates instrumented C programs which can be compiled by any compliant C compiler such as GCC and other platform-specific compilers. By running the compiled programs, memory safety and the specified properties can be automatically monitored and verified at runtime. When a violation is detected, an error message is reported. The user may also specify other control behavior for the violation, e.g., force the program to abort or execute a code snippet for recovery purposes. Movec can be used with fuzzy testing, like other dynamic analysis tools.

In particular, Movec implements the following three features:


To run Movec, please put its executable file in a directory in your PATH. Note that:

References and Documentations

Last updated: July 1, 2021