GSoC Idea: Core KLEE Analysis

KLEE analysis


Areas Code coverage, ...
Good if student knows C, KLEE
Priority Low
Difficulty Medium
Benefits to the student ???
Benefits to the Tcl Community Enhanced validation of the Tcl core's correctness, an extended testsuite
Mentor ???

Project Description

KLEE is a tool for the /quote/ Unassisted And Automatic Generation Of High-Coverage Tests For Complex Systems Programs /end-quote/. I.e., it takes C sources as inputs, symbolically executes all paths, and from that derives constraints and test cases that demonstrate bugs in the original sources.

As such it is in the same general area as Coverity and other static analysis tools.

In this project the student is asked to use KLEE (and possibly other free tools) to analyze the Tcl core to find bugs that have escaped the maintainers so far and enhance the testsuite to demonstrate them. The result should be the enhanced testsuite, plus the scripts written to drive KLEE and other tools, all of which enables future maintainers to reproduce the work and do their own runs.

References

Comments & Discussion

Some comments here