MirandaTesting · Testing Program Analyzers Ad Absurdum

Program analyzers act as guards for ensuring reliability of modern-daysoftware. But who guards the guards themselves? Due to their highcomplexity and sophisticated algorithms, analyzers are likely tocontain critical bugs, which we define as those leading to wrongresults, e.g., returning `correct' for incorrect software. Such bugsmay have detrimental consequences, especially in safety-criticalsettings. It is, therefore, imperative to be able to detect them.Verifying the absence of critical bugs in a program analyzer isprohibitively expensive. Contrary to verification, automated testgeneration can be used to effectively find such bugs. Existing testingapproaches, however, are still in their infancy for this applicationdomain.To address this issue, MirandaTesting will develop the firstprincipled methodology for testing a wide range of programanalyzers. At its core, our methodology exposes more information aboutwhy an analyzer computes a particular result; it then uses thisinformation to interrogate the analyzer aiming to force it into acontradiction, thus revealing a critical bug. The project has thefollowing goals:1. Design a general framework for testing program analyzers using the MirandaTesting methodology;2. Develop interrogation strategies pertaining to eleven prevalent classes of program analyzers;3. Demonstrate the effectiveness of concrete instantiations of the general framework and interrogation strategies for several popular program analyzers from each class;4. Focus on disseminating our methodology and infrastructure.If successful, MirandaTesting will enable systematic testing of entireprogram-analyzer classes. As a result, analyzers will exhibit fewercritical bugs, potentially preventing catastrophic outcomes insafety-critical domains.