Quick Guide to TESLA

This is a quick write-up on what is TESLA and how to use it in order to verify temporal properties of running code.

TESLA relies on some 3rd party software (which you can install from the ports or package system), notable requirements are:

• environment able to build llvm/clang (CMake, Python)
• OCaml
• svn (recommended way to get sources)

TEAL language:

• automata
• either {} or
• multiple