Finding errors in tools that check the correctness of programs.

What is it about?

We developed a tool that allows us to automatically generate programs which we know to be free of or contain errors. Using this, we can test tools which are supposed to find errors in programs or prove their absence, known as program analyzers. The method is simple: If we know one of our test programs contains an error and the tool fails to find it; or if we know there is no error, but the tool claims that there is one. Using the tool we found 30 bugs in state-of-the-art program analyzers, which we reported and were quickly fixed.

Featured Image

Why is it important?

Program analyzers are often used to check programs that run in safety-critical settings. If an analyzer misses an error, e.g. in software that steers an airplane, the consequences can be grave. Therefore it is important to make sure that analyzers work as reliably as possible.