[cfe-dev] GSoC 2018

[Mikhail Ramalho via cfe-dev]

Hi all,

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.

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]).

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.

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.

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.

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?

Also any feedback is welcome.

Thank you,

-- 

Mikhail R. Gadelha.


[0] https://reviews.llvm.org/D36610
[1] https://reviews.llvm.org/D42966
[2] https://github.com/Z3Prover/z3/pull/1501
[3] https://github.com/esbmc/esbmc
[4]
https://archive.fosdem.org/2017/schedule/event/clang_formal_verification_tool_frontend/

-- 

Mikhail Ramalho.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.llvm.org/pipermail/cfe-dev/attachments/20180223/d93adc5d/attachment.html>