The tutorial will briefly cover the following:

• Setting up the Gigahorse framework development environment and related toolchains

• Specifying simple program analyses

• Implement analyses for known vulnerabilities such as reentrancy

• Run these analyses at scale, and compare their results

• Introduce basic analysis design considerations and their effect on precision, completeness and scalability

Necessary background: the tutorial will make as few assumptions as possible regarding the background of participants, especially relative to the blockchain and smart contracts. Necessary concepts of smart contract execution will be introduced in the tutorial, although the emphasis will be on static analysis. Participants should have some background in intermediate languages and simple program analysis, at the level of a Compilers course.

Medium: There will be an initial presentation of tutorial material (slides + screen sharing for command line and setup). Afterwards, the tutorial is expected to be interactive, with extensive screen sharing among participants to jointly examine code.

Platform: Participants should have machines with a Unix-like OS (Linux preferred, MacOS should be ok). The Souffle language will be ideally installed and tested before the tutorial.