Infer automatically finds problems such as null pointer dereference. What do you do if the problem you are interested in is not one of those Infer finds out-of-the-box? One option is to add a checker to Infer, implementing it in OCaml, using the existing abstract interpretation framework. But, this can take effort. Another option is to use AL, a language understood by Infer that specifies syntactic patterns. But, the problem you are interested in may not be detectable from syntax only: it may require reasoning about semantics. Finally, you can use Topl. When should you use it? As a rule of thumb, if when you explain the problem you are interested in you use words like “after”, “before”, “and then”, you probably want to take a look at Topl. One example kind of problem is information flow: “if a string is returned by method foo() and then is sent as an argument to method bar(), I want to know”. Notice how the words “and then” are used. In general, you can safety temporal properties with data by writing down an automaton with registers. The analysis is compositional, and so it scales to large programs.

This talk will give examples of properties that can be specified in Topl. Then we will see the main ideas of how the analysis is implemented, with an emphasis on how compositionality and scalability are achieved.