[BiteCode_dev]

Thank you.

> The key difference is that we don’t actually invoke the code with concrete values, but rather treat it like a set of constraints that should always be satisfied

How does that work with a dynamic language such as Python?

[Choc13]

The static type information isn't actually too important to us, what our tool cares about is being able to interpret branching conditions in the code in order to turn them into constraints. We currently do this at the LLVM IR level, so as long as we can compile the code down into this form then we can analyse it. With Python a lot of the work we had to do in order to get a prototype working was in being able to handle all of the system calls that the Python interpreter needs to make when booting up. These aren't always straight forward to treat symbolically because they interact with the file system etc, but it's possible to provide mock implementations that don't affect the analysis of the users code.