GSoC 2018 | Integrate Z3 SMT solver with clang static analyzer

Hello all,

All the discussions that I had with George Kaepenkov and Dominic Chen on the cfe-dev mailing list and some of my personal research, I have written the first draft of my proposal:

https://docs.google.com/document/d/1A_r_1b2deVz9bB52SyevbeFtfoI0bIBGQtMoyU_6A9s/edit?usp=sharing

I request all the members of the community to please add your valuable comments.

Thank you very much,

Ashish Kumar Gahlot

Hi Ashish,

The first paragraph of your proposal is taken almost verbatim from the abstract of "Dynamic Taint Analysis for Automatic Detection, Analysis, and Signature Generation of Exploits on Commodity Software”, and the second from “Z3: An Efficient SMT Solver”.
The rest of the proposal is problematic as well, with many unrelated items mixed together.

George

Respected sir,

Please have a look at the proposal now. I have made changes to the mentioned problematic paragraphs.

Thank you very much,

Ashish Kumar Gahlot