[hkopp]

Thank you for the answer and a big kudos for the project.

Regarding the memory violation, could symbolica deal with symbolic memory? Can it deal with symbolic files as input? How about syscalls with symbolic inputs? These are the main problems I had when I worked on my toy symbolic execution engine. If yes, you should definitely market these features.

[Choc13]

Yeah it can deal with symbolic memory. As long as the memory allocation is fixed size the contents can be fully or partially symbolic. We also support symbolic addresses for allocations to ensure that pointer arithmetic is fully tested.

We're currently simulating a lot of the underlying system at the C std library level. For a number of reasons we'd like to lower this to the raw syscall and assembly level. This would allow any lib C implementation to be tested along with the application code, and we may even be able to simulate threading and the file system. Syscalls could be made symbolic along with files by treating the entire system symbolically, but obviously this is a lot of work so it's something that we're gradually building towards.