Check-exec is a Python extension to GDB aiming at checking runtime properties inside the debugger.
It lets a developer debug their program by writing properties and have their debugger find the moment when something goes wrong. Then, the developer can look into it using the debugger in the way they are familiar with.
You can take a look at the documentation.
You can look at the master thesis report that presents the approach in detail.
You can read the COMPAS'16 paper (French) that is shorter and older.
You can look at the slides for both the COMPAS'16 paper and the master thesis report.
You can watch a short video in which check-exec is used to detect an overflow in a producer-consumers toy program:
check-exec, use Git:
git clone https://forge.imag.fr/anonscm/git/check-exec/check-exec.git
Check-exec is currently under the Mozilla Public Licence, though we might switch to GPL at some point.
You can check experiments and evaluations done on check-exec here.
Any patch or suggestion is welcome. Please contact us, we will be glad to hear about you.
Raphaël Jakse: raphael dot jakse at imag dot fr
Yliès Falcone: ylies dot falcone at ujf dash grenoble dot fr
Kevin Poujet: kevin dot poujet at imag dot fr
Jean-François Méhaut: jean dash francois dot mehaut at imag dot fr