Program
Verification
Book

PV2 ⊧ MOVEC: MOnitoring, VErification and Controlperforms aspect weaving

Application domain/field

Runtime verification
Aspect-oriented Programming (AOP)

Type of tool

source to source transformer/compiler based on aspect weaving

Expected input

C program + monitor files

Format:

C-program

Expected output

instrumented header + source files

Internals

aspect oriented programming, aspect weaving

Links

Project page: https://drzchen.github.io/projects/movec/
Repository: https://github.com/drzchen/movec
- Last commit date: 10 Dec 2021 (default branch)
- Last commit date: 10 Dec 2021 (last activity)

Related papers

Runtime detection of memory errors with smart status (ISSTA '21)
Detecting memory errors at runtime with source-level instrumentation (ISSTA '19)
Parametric Runtime Verification of C Programs (TACAS '16)

Last publication date

11 July 2021

Related tools

ProVerB specific

Markdown description: view/edit
Contained in the ProVerB22 dataset (paper + artefact)

ProVerB is a part of SLEBoK. Last updated: February 2023.