RTL-Check

RTL-check is an extensible and powerful abstract interpretation framework for static analysis of programs from a safety and security perspective. It performs analysis on RTL, which is the low-level intermediate representation generated by GCC. See the documentation section for more information.

News

Patrice Lacroix master's thesis is available here. (2006-09-27)
Small improvement in performance, minor bug fixed. (0.1.7, 2006-09-12) [Download]
Experimental analyses to detect integer overflows and the size of local variables, and a preview of RDB. (0.1.6, 2006-04-02)
New release that adds flow insensitive analysis and preliminary call size inference. (0.1.5, 2005-12-22)
Major bug fix release. The analysis is now believed to be safe, except for integer overflows. (0.1.4, 2005-08-07)
Improved framework for widening and narrowing, fixed a few bugs. (0.1.3, 2005-07-20)
Improved framework, implementation of liveness analysis follows more closely the theorical monotone framework. (0.1.2, 2005-06-27)
Support of memory aliases, much cleaner output, improved documentation, many bugs fixed (0.1.1, 2005-05-31)
New abstract interpretation framework, analysis now understands linear relations between variables (0.1.0, 2005-03-05)
Faster analysis and returns more useful set of constraints instead of "Impossible" (0.0.8, 2005-01-25)
Implemented abstract interpretation to perform analysis on programs using the constraint system. (0.0.7, 2004-11-11)
RTL-Check has a constraint system to represent program states. (0.0.6, 2004-09-30)
RTL-Check implements some kind of shape analysis. (0.0.4, 2004-06-12)
RTL-Check can now generate control-flow graphs on demand. (0.0.3, 2004-05-26)
First release of RTL-Check is available. (2004-05-07)

Useful links

Documentation

A presentation of the RTL-Check project and its goals.
RTL-Check: A Practical Static Analysis Framework to Verify Memory Safety and More is Patrice Lacroix master's thesis and certainly the best source of technical information about the RTL-Check framework and the different analyses implemented with it.
A small user's guide is also available.

About the authors

The main author of RTL-Check is Patrice Lacroix. RTL-Check was started as a part of his master's program in computer science at Université Laval under the direction of Jules Desharnais. He was supported by a Postgraduate Scholarship from NSERC.

Moritz Muehlenhoff from University of Bremen also contributed to this project.

RTL-Check is hosted by: