Soufflé is a system for developing static program analyses in a declarative fashion. An analysis is expressed in a Datalog-like logic language. From the logic specification of the analysis, Soufflé synthesizes a highly efficient, parallel C++ program via partial evaluation. Soufflé is currently being employed for industrial-strength static analysis problems, including large-scale program analysis and security analysis of cloud networks. This tutorial will introduce (1) the logic language of Soufflé, (2) how to write Datalog-based static analyses, (3) give a guide on how one can build efficient static analyzers using industrial use-cases, and (4) give an overview of the underlying technology of Soufflé.

Please bring your notebook for hands-on exercises.