[cfe-dev] GSoC 2018

[Artem Dergachev via cfe-dev]

Hey, welcome!

Thanks for picking this up, it's indeed a high-impact item - our current 
ultra-simplified solver helped us launch and is often sufficient, but a 
significant portion of our false positives is caused by math being just 
slightly more complicated than it can digest.

As for communications, the only thing lists aren't good enough for is a 
quick chat. It's up to you and George to decide how would you handle 
most of the communication, but i'll recommend keeping the community 
informed about any interesting topics that show up - either technical 
questions or your own developments. In particular, you might potentially 
receive feedback from other active community members on your upcoming 
proposal.

On 23/02/2018 9:29 AM, Mikhail Ramalho via cfe-dev wrote:
> 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.
>
>
> _______________________________________________
> cfe-dev mailing list
> cfe-dev at lists.llvm.org
> http://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-dev