Dynamically allocated memory is difficult to verify automatically. There are some tools based on separation logic (e.g. Smallfoot, HIP/SLEEK, jStar) that are able to verify C programs (or C-like programs). Current developments in this area are focusing on automatically inferring specifications (also known as abductive reasoning). Moreover, automatically verifying concurrent programs is also difficult and a hot research topic at the moment.
If I am not mistaken, Smallfoot is the basis for a professional product being developed by Monoidics (http://www.monoidics.com). Interestingly, the company was recently acquired by Facebook :)
Excellent work, guys! As an amateur sax player, I can see myself using your app to produce some funky beats on-the-fly. I wish you all the best and I hope I can buy your app in the near future. :)
If I am not mistaken, Smallfoot is the basis for a professional product being developed by Monoidics (http://www.monoidics.com). Interestingly, the company was recently acquired by Facebook :)
Update: Here's a link with a list of related tools: http://www0.cs.ucl.ac.uk/staff/p.ohearn/Invader/Invader/Frie...