Towards Scalable Translation Validation of Static Analyzers

Static analyzers, which have been successfully deployed in real world to statically find software errors, are complex pieces of software whose reliability is very hard to establish by testing. Testing is not so effective because analysis results are hard to validate manually for the following reasons: (i) even valid outputs can contain false alarms (or even false state of an input program are too big to manually inspect. In this paper, we claim that the translation validation approach is a scalable and effective method to establish reliability of such software. To demonstrate scalability, we developed a verified validator for a real-world static analyzer, which uses various complex algorithms. To demonstrate effectiveness, using our validator we validated the analysis results of the analyzer for 16 open-source programs, during which we effectively identified and fixed 13 bugs using the validation results.