Equid—A Static Analysis Framework for Industrial Applications

Abstract

The rise of the software engineering industry sparkled the research on static analyzers in both academia and industry. Academic tools historically have an exhaustive feature set but don’t easily apply to industrial applications, and industrial verifiers are still very limited. The Equid project, which loosely stands for “Engine for performing queries on unified intermediate representations of program and domain models” is an attempt to fill the gap between theory and practice by building a language-agnostic analyzer in close contact with development and security community. In this introductory paper we set project goals, reveal motivation and describe code processing stages, such as preprocessing, translation to project’s own intermediate codes, virtual machine execution, constraint solving, all done to make static and interactive contract violation checks easier, more precisive yet informative. The project is compared to other analyzers. We believe that such a framework can draw attention to industrial uses clearly missed by verification communities and help shape a vision of universal static analyzer architectures.