<html xmlns:o="urn:schemas-microsoft-com:office:office" xmlns:w="urn:schemas-microsoft-com:office:word" xmlns:m="http://schemas.microsoft.com/office/2004/12/omml" xmlns="http://www.w3.org/TR/REC-html40">
<head>
<meta http-equiv="Content-Type" content="text/html; charset=utf-8">
<meta name="Generator" content="Microsoft Word 15 (filtered medium)">
<style><!--
/* Font Definitions */
@font-face
{font-family:"Cambria Math";
panose-1:2 4 5 3 5 4 6 3 2 4;}
@font-face
{font-family:Calibri;
panose-1:2 15 5 2 2 2 4 3 2 4;}
/* Style Definitions */
p.MsoNormal, li.MsoNormal, div.MsoNormal
{margin:0cm;
margin-bottom:.0001pt;
font-size:11.0pt;
font-family:"Calibri",sans-serif;}
a:link, span.MsoHyperlink
{mso-style-priority:99;
color:blue;
text-decoration:underline;}
a:visited, span.MsoHyperlinkFollowed
{mso-style-priority:99;
color:purple;
text-decoration:underline;}
p.msonormal0, li.msonormal0, div.msonormal0
{mso-style-name:msonormal;
mso-margin-top-alt:auto;
margin-right:0cm;
mso-margin-bottom-alt:auto;
margin-left:0cm;
font-size:11.0pt;
font-family:"Calibri",sans-serif;}
span.EmailStyle18
{mso-style-type:personal-reply;
font-family:"Calibri",sans-serif;
color:windowtext;}
.MsoChpDefault
{mso-style-type:export-only;
font-size:10.0pt;}
@page WordSection1
{size:612.0pt 792.0pt;
margin:70.85pt 70.85pt 2.0cm 70.85pt;}
div.WordSection1
{page:WordSection1;}
--></style>
</head>
<body lang="DE" link="blue" vlink="purple">
<div class="WordSection1">
<p class="MsoNormal"><span lang="EN-GB">Dear Evgeny,<o:p></o:p></span></p>
<p class="MsoNormal"><span lang="EN-GB"><o:p> </o:p></span></p>
<p class="MsoNormal"><span lang="EN-GB">This list of activities is looking very promising and going in the right direction.<o:p></o:p></span></p>
<p class="MsoNormal"><span lang="EN-GB"><o:p> </o:p></span></p>
<p class="MsoNormal"><span lang="EN-GB">(To be very honest: my personal interest in LDV/Klever has been eaten up by the pushbacks and difficulties we encountered last year. Despite all the support you provided and advances you built in Klever last year, it
was just not yet ready for showing the results that I was hoping for. I personally will continue to investigate in syzkaller, but my assessment of Klever’s potential is still positive, and the quantative data I collected shows that LDV is still a promising
tool in the Linux kernel development.<o:p></o:p></span></p>
<p class="MsoNormal"><span lang="EN-GB"><o:p> </o:p></span></p>
<p class="MsoNormal"><span lang="EN-GB">May I share this document with other potential stakeholders, the ELISA collaboration project and other interested parties through my expert network and with Linux Foundation?<o:p></o:p></span></p>
<p class="MsoNormal"><span lang="EN-GB"><o:p> </o:p></span></p>
<p class="MsoNormal"><span lang="EN-GB">Best regards,<o:p></o:p></span></p>
<p class="MsoNormal"><span lang="EN-GB"><o:p> </o:p></span></p>
<p class="MsoNormal"><span lang="EN-GB">Lukas<o:p></o:p></span></p>
<p class="MsoNormal"><span lang="EN-GB"><o:p> </o:p></span></p>
<div style="border:none;border-top:solid #B5C4DF 1.0pt;padding:3.0pt 0cm 0cm 0cm">
<p class="MsoNormal" style="margin-left:36.0pt"><b><span style="font-size:12.0pt;color:black">From:
</span></b><span style="font-size:12.0pt;color:black">Evgeny Novikov <novikov@ispras.ru><br>
<b>Date: </b>Tuesday 2019-01-22 at 08:57<br>
<b>To: </b>LDV list <ldv-project@ispras.ru>, "ldv-project@linuxtesting.org" <ldv-project@linuxtesting.org>, Alexander Petrenko <petrenko@ispras.ru>, "Bulwahn Lukas, JC-22" <Lukas.Bulwahn@bmw.de>, "mSzczepankiewicz@exida.com" <mSzczepankiewicz@exida.com><br>
<b>Subject: </b>Re: [ldv-project] Most important missed features and crucial bugs of Klever<o:p></o:p></span></p>
</div>
<div>
<p class="MsoNormal" style="margin-left:36.0pt"><o:p> </o:p></p>
</div>
<div>
<p class="MsoNormal" style="margin-left:36.0pt">Dear colleagues,<o:p></o:p></p>
</div>
<div>
<p class="MsoNormal" style="margin-left:36.0pt"> <o:p></o:p></p>
</div>
<div>
<p class="MsoNormal" style="margin-left:36.0pt">At last we completed internal discussions of further development of Klever in favor of verification of the Linux kernel. Here is the result:<o:p></o:p></p>
</div>
<div>
<p class="MsoNormal" style="margin-left:36.0pt"> <o:p></o:p></p>
</div>
<div>
<p class="MsoNormal" style="margin-left:36.0pt">https://docs.google.com/document/d/11e7cDzRqx0nO1UBcM75l6MS28zRBJUicXdNiReEpDKI/edit?usp=sharing<o:p></o:p></p>
</div>
<div>
<p class="MsoNormal" style="margin-left:36.0pt"> <o:p></o:p></p>
</div>
<div>
<p class="MsoNormal" style="margin-left:36.0pt">We would be glad to receive any feedback in addition to the one you provided thus far.<o:p></o:p></p>
</div>
<div>
<p class="MsoNormal" style="margin-left:36.0pt"> <o:p></o:p></p>
</div>
<div>
<p class="MsoNormal" style="margin-left:36.0pt">-- <o:p></o:p></p>
</div>
<div>
<p class="MsoNormal" style="margin-left:36.0pt">Evgeny Novikov<br>
Linux Verification Center, ISP RAS<br>
<a href="http://linuxtesting.org">http://linuxtesting.org</a><o:p></o:p></p>
</div>
<div>
<p class="MsoNormal" style="margin-left:36.0pt"> <o:p></o:p></p>
</div>
<div>
<p class="MsoNormal" style="margin-left:36.0pt"> <o:p></o:p></p>
</div>
<div>
<p class="MsoNormal" style="margin-left:36.0pt"> <o:p></o:p></p>
</div>
<div>
<p class="MsoNormal" style="margin-left:36.0pt">25.11.2018, 21:04, "Evgeny Novikov" <novikov@ispras.ru>:<o:p></o:p></p>
</div>
<blockquote style="margin-top:5.0pt;margin-bottom:5.0pt">
<div>
<p class="MsoNormal" style="margin-left:36.0pt">Until the mentioned date we did not receive feature/bug lists from anybody. I guess that this is because the task is not trivial at all. Without really deep understanding one can not reason about Klever pros and
cons well enough. There are no straightforward analogues of Klever in industry, so, nobody can say easily, that X has such features while Klever does not have them.<o:p></o:p></p>
</div>
<div>
<p class="MsoNormal" style="margin-left:36.0pt"> <o:p></o:p></p>
</div>
<div>
<p class="MsoNormal" style="margin-left:36.0pt">From the other side people, who are aware much about Klever internals, can rank missed features and crucial bugs in quite an incorrect way. For instance, I dislike inefficient weaving very much but for many users
better support of new versions and non-standard configurations of the Linux kernel is necessary much more. <o:p></o:p></p>
</div>
<div>
<p class="MsoNormal" style="margin-left:36.0pt"> <o:p></o:p></p>
</div>
<div>
<p class="MsoNormal" style="margin-left:36.0pt">Let's try another approach. The core development team will suggest an initial list of important features and bugs. They will be higher-level than ones in
<a href="https://forge.ispras.ru/projects/klever/issues?set_filter=1">our issue tracker</a>. Then everybody will be able to suggest any improvements to be discussed. I hope that we will complete the former in 2-3 weeks, and we will finish discussion until the
end of this year or the early beginning of the following year.<o:p></o:p></p>
</div>
<div>
<p class="MsoNormal" style="margin-left:36.0pt"> <o:p></o:p></p>
</div>
<div>
<p class="MsoNormal" style="margin-left:36.0pt">-- <o:p></o:p></p>
</div>
<div>
<p class="MsoNormal" style="margin-left:36.0pt">Evgeny Novikov<br>
Linux Verification Center, ISP RAS<br>
<a href="http://linuxtesting.org/">http://linuxtesting.org</a><o:p></o:p></p>
</div>
<div>
<p class="MsoNormal" style="margin-left:36.0pt"> <o:p></o:p></p>
</div>
<div>
<p class="MsoNormal" style="margin-left:36.0pt"> <o:p></o:p></p>
</div>
<div>
<p class="MsoNormal" style="margin-left:36.0pt"> <o:p></o:p></p>
</div>
<div>
<p class="MsoNormal" style="margin-left:36.0pt">14.11.2018, 19:31, "Evgeny Novikov" <<a href="mailto:novikov@ispras.ru">novikov@ispras.ru</a>>:<o:p></o:p></p>
</div>
<blockquote style="margin-top:5.0pt;margin-bottom:5.0pt">
<div>
<p class="MsoNormal" style="margin-left:36.0pt">Dear developers, users and experts!<o:p></o:p></p>
</div>
<div>
<p class="MsoNormal" style="margin-left:36.0pt"> <o:p></o:p></p>
</div>
<div>
<p class="MsoNormal" style="margin-left:36.0pt">We would like to collect your opinions about most important features that are missed in Klever as well as crucial bugs that Klever has at the moment. This survey will help us to evaluate better possible directions
of future development.<o:p></o:p></p>
</div>
<div>
<p class="MsoNormal" style="margin-left:36.0pt"> <o:p></o:p></p>
</div>
<div>
<p class="MsoNormal" style="margin-left:36.0pt">Please, enumerate features and bugs that you treat most vital. We will assume that items that you will put earlier in a list have a larger priority for you. Examples are "Klever does not support verification of
loadable kernel modules of recent versions of the Linux kernel", "Klever lacks documentation on development of requirement specifications", "Klever needs more user-friendly interface".<o:p></o:p></p>
</div>
<div>
<p class="MsoNormal" style="margin-left:36.0pt"> <o:p></o:p></p>
</div>
<div>
<p class="MsoNormal" style="margin-left:36.0pt">We will summarize your feedback on November 23, but we are looking forward for your opinion at any time.<o:p></o:p></p>
</div>
<div>
<p class="MsoNormal" style="margin-left:36.0pt"> <o:p></o:p></p>
</div>
<div>
<p class="MsoNormal" style="margin-left:36.0pt">Best regards,<o:p></o:p></p>
</div>
<div>
<p class="MsoNormal" style="margin-left:36.0pt">Evgeny Novikov<o:p></o:p></p>
</div>
<div>
<p class="MsoNormal" style="margin-left:36.0pt"> <o:p></o:p></p>
</div>
<div>
<p class="MsoNormal" style="margin-left:36.0pt">-- <o:p></o:p></p>
</div>
<div>
<p class="MsoNormal" style="margin-left:36.0pt">Evgeny Novikov<br>
Linux Verification Center, ISP RAS<br>
<a href="http://linuxtesting.org/">http://linuxtesting.org</a><o:p></o:p></p>
</div>
<div>
<p class="MsoNormal" style="margin-left:36.0pt"> <o:p></o:p></p>
</div>
</blockquote>
</blockquote>
</div>
</body>
</html>