<div dir="ltr"><div>Hi all,</div><div><br></div><div>My name is Mikhail R. Gadelha, I'm a PhD student from the University of Southampton, UK. I'm interested in working on the project "Integrate with Z3 SMT solver to reduce false positives", during the summer by joining GSoC.</div><div><br></div><div>This would be my first participation in the GSoC; however, I have already contributed to some open source projects (including clang[0][1] and Z3[2]).</div><div><br></div><div>I've been working with clang libTooling for a couple of years now, as a frontend for my verification tool, ESBMC [3]. When developing the frontend, I also presented a WIP version in FOSDEM'17 [4], in the LLVM Toolchain devroom. Regarding SMT solvers, I have experience with Z3, Boolector, MathSAT, CVC4 and Yices, as we support them all in ESBMC. Currently I'm developing a solver-independent SMT library for floating-points, as part of my research.</div><div><br></div><div>I found the project very interesting and it's highly related to my research; witness/counter-example validation is an important topic in the field (and a planned feature for our tool). It would be excellent to implement such feature in clang, and check the results in real-world applications.</div><div><br></div><div>I contacted George Karpenkov (the mentor of the project) with a question about why focusing on Z3 and the reasons are: (1) it's already integrated in the build system, (2) license issues with other solvers (e.g., Yices is GPL3) and (3) time constraints.</div><div><br></div><div>I also have a question about the proposal. I understand that ideas about the project will be discussed in the mailing list. However, once that's settled and I write my first draft proposal, should I send it to the mailing list for discussion again or should I send it only to the mentor?</div><div><br></div><div>Also any feedback is welcome.</div><div><br></div><div>Thank you,</div><div><br></div><div>-- </div><div><br></div><div>Mikhail R. Gadelha.</div><div><br></div><div><br></div><div>[0] <a href="https://reviews.llvm.org/D36610">https://reviews.llvm.org/D36610</a></div><div>[1] <a href="https://reviews.llvm.org/D42966">https://reviews.llvm.org/D42966</a></div><div>[2] <a href="https://github.com/Z3Prover/z3/pull/1501">https://github.com/Z3Prover/z3/pull/1501</a></div><div>[3] <a href="https://github.com/esbmc/esbmc">https://github.com/esbmc/esbmc</a></div><div>[4] <a href="https://archive.fosdem.org/2017/schedule/event/clang_formal_verification_tool_frontend/">https://archive.fosdem.org/2017/schedule/event/clang_formal_verification_tool_frontend/</a></div><div><br></div>-- <br><div class="gmail_signature"><div dir="ltr"><div><br></div><div>Mikhail Ramalho.</div></div></div>
</div>