[lsb-discuss] [GSoC] Student - Want to work on "Formalization and Checking of Correct Usage of Kernel Core API"

[Alexey Khoroshilov]

Hi, Alexander!

Thank you for your interest.

I would recommend you some additional information about various details
of LDV project in Russian:
[1] E.M. Novikov. Building Programming Interface Specifications in the
Open System of Componentwise Verification of the Linux Kernel. pp.
293-316. -
http://ispras.ru/ru/proceedings/archives/isp_24_2013/isp_24_2013_293_eng.php
[2] A.V. Khoroshilov, V.S. Mutilin, E.M. Novikov, P.E. Shved, A.V.
Strakh. Linux Driver Verification Architecture. pp. 163-187. -
http://ispras.ru/ru/proceedings/archives/isp_20_2011/isp_20_2011_163_eng.php
[3] Mutilin V.S., Novikov E.M., Khoroshilov A.V. Analysis of typical
faults in Linux operating system drivers. pp. 349-374. -
http://ispras.ru/ru/proceedings/archives/isp_22_2012/isp_22_2012_349_eng.php
[4] Khoroshilov A.V., Mandrykin M.U., Mutilin V.S. Introduction to CEGAR
— Counter-Example Guided Abstraction Refinement. pp. 219-292. -
http://ispras.ru/ru/proceedings/archives/isp_24_2013/isp_24_2013_219_eng.php

Examples of rules formalizing correct usage of kernel core API you can
find here:
https://forge.ispras.ru/git/kernel-rules.git
and some descriptions here:
http://forge.ispras.ru/projects/ldv-rules/issues?query_id=48

Feel free to contact us if any questions.

Best regards,
Alexey Khoroshilov,
Linux Verification Center, ISPRAS


On 09.03.2014 13:48, Alexander Mezin wrote:
> Hi.
>
> I am student and I want to participate in Google Summer of Code this year.
>
> I like the idea "Formalization and Checking of Correct Usage of Kernel
> Core API".
>
> Recently I started contributing patches to Linux. Sadly, I didn't hear
> about LDV before, but I'll surely check it out soon. I think it could
> be used not only for finding problems in existing code. Patches can't
> be reviewed immediately, and every tool that could check code before
> sending it to review could significantly speed up development.
>
> Something about me:
> Currently I am student in Omsk State University, Computer Science
> depart, pursuing Master's degree.
> Got Bachelor's degree in Computer Science and Engineering in
> Novosibirsk State University.
> I don't have much experience in kernel development (currently, only
> one my small patch is accepted), but I can learn new things relatively
> fast. At least, I think so :) Kernel development
> I've successfully completed GSoC previous year. My project "Touchpad
> KCM" [1] for KDE is now included in Arch Linux, and will be installed
> by default in Kubuntu 14.04.
> I have some theoretical knowledge in AOP, however, I didn't do any
> real project using it.
> Also, I have github account: https://github.com/sanya-m/
>
> [1]: https://projects.kde.org/projects/playground/utils/kcm-touchpad/
> _______________________________________________
> lsb-discuss mailing list
> lsb-discuss at lists.linux-foundation.org
> https://lists.linuxfoundation.org/mailman/listinfo/lsb-discuss
>