<html xmlns:v="urn:schemas-microsoft-com:vml" 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=us-ascii">
<meta name="Generator" content="Microsoft Word 15 (filtered medium)">
<!--[if !mso]><style>v\:* {behavior:url(#default#VML);}
o\:* {behavior:url(#default#VML);}
w\:* {behavior:url(#default#VML);}
.shape {behavior:url(#default#VML);}
</style><![endif]--><style><!--
/* Font Definitions */
@font-face
{font-family:Wingdings;
panose-1:5 0 0 0 0 0 0 0 0 0;}
@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;}
@font-face
{font-family:"Frutiger 45 Light";
panose-1:2 11 5 0 0 0 0 0 0 0;}
@font-face
{font-family:"Segoe UI";
panose-1:2 11 5 2 4 2 4 2 2 3;}
@font-face
{font-family:"Segoe UI Light";
panose-1:2 11 5 2 4 2 4 2 2 3;}
/* Style Definitions */
p.MsoNormal, li.MsoNormal, div.MsoNormal
{margin:0in;
margin-bottom:.0001pt;
font-size:12.0pt;
font-family:"Times New Roman",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
{mso-style-priority:99;
margin:0in;
margin-bottom:.0001pt;
font-size:12.0pt;
font-family:"Times New Roman",serif;}
p.msonormal0, li.msonormal0, div.msonormal0
{mso-style-name:msonormal;
margin:0in;
margin-bottom:.0001pt;
font-size:12.0pt;
font-family:"Times New Roman",serif;}
span.EmailStyle19
{mso-style-type:personal-reply;
font-family:"Frutiger 45 Light";
color:#1F497D;}
.MsoChpDefault
{mso-style-type:export-only;
font-size:10.0pt;}
@page WordSection1
{size:8.5in 11.0in;
margin:1.0in 1.0in 1.0in 1.0in;}
div.WordSection1
{page:WordSection1;}
/* List Definitions */
@list l0
{mso-list-id:583995425;
mso-list-template-ids:-733208088;}
@list l0:level1
{mso-level-number-format:bullet;
mso-level-text:\F0B7;
mso-level-tab-stop:.5in;
mso-level-number-position:left;
text-indent:-.25in;
mso-ansi-font-size:10.0pt;
font-family:Symbol;}
@list l0:level2
{mso-level-number-format:bullet;
mso-level-text:o;
mso-level-tab-stop:1.0in;
mso-level-number-position:left;
text-indent:-.25in;
mso-ansi-font-size:10.0pt;
font-family:"Courier New";
mso-bidi-font-family:"Times New Roman";}
@list l0:level3
{mso-level-number-format:bullet;
mso-level-text:\F0A7;
mso-level-tab-stop:1.5in;
mso-level-number-position:left;
text-indent:-.25in;
mso-ansi-font-size:10.0pt;
font-family:Wingdings;}
@list l0:level4
{mso-level-number-format:bullet;
mso-level-text:\F0A7;
mso-level-tab-stop:2.0in;
mso-level-number-position:left;
text-indent:-.25in;
mso-ansi-font-size:10.0pt;
font-family:Wingdings;}
@list l0:level5
{mso-level-number-format:bullet;
mso-level-text:\F0A7;
mso-level-tab-stop:2.5in;
mso-level-number-position:left;
text-indent:-.25in;
mso-ansi-font-size:10.0pt;
font-family:Wingdings;}
@list l0:level6
{mso-level-number-format:bullet;
mso-level-text:\F0A7;
mso-level-tab-stop:3.0in;
mso-level-number-position:left;
text-indent:-.25in;
mso-ansi-font-size:10.0pt;
font-family:Wingdings;}
@list l0:level7
{mso-level-number-format:bullet;
mso-level-text:\F0A7;
mso-level-tab-stop:3.5in;
mso-level-number-position:left;
text-indent:-.25in;
mso-ansi-font-size:10.0pt;
font-family:Wingdings;}
@list l0:level8
{mso-level-number-format:bullet;
mso-level-text:\F0A7;
mso-level-tab-stop:4.0in;
mso-level-number-position:left;
text-indent:-.25in;
mso-ansi-font-size:10.0pt;
font-family:Wingdings;}
@list l0:level9
{mso-level-number-format:bullet;
mso-level-text:\F0A7;
mso-level-tab-stop:4.5in;
mso-level-number-position:left;
text-indent:-.25in;
mso-ansi-font-size:10.0pt;
font-family:Wingdings;}
ol
{margin-bottom:0in;}
ul
{margin-bottom:0in;}
--></style><!--[if gte mso 9]><xml>
<o:shapedefaults v:ext="edit" spidmax="1026" />
</xml><![endif]--><!--[if gte mso 9]><xml>
<o:shapelayout v:ext="edit">
<o:idmap v:ext="edit" data="1" />
</o:shapelayout></xml><![endif]-->
</head>
<body lang="EN-US" link="blue" vlink="purple">
<div class="WordSection1">
<p class="MsoNormal"><span style="font-family:"Calibri",sans-serif;color:black">Dear all,<br>
<br>
Friendly reminder: Steve Crocker (<a href="https://en.wikipedia.org/wiki/Steve_Crocker" id="LPlnk406363">https://en.wikipedia.org/wiki/Steve_Crocker</a> is giving a talk
<b>today at</b> <b>2pm in ARC 221 (NEW LOCATION)</b> on the question, Why Isn't Verification Standard Practice? I encourage all of you to attend.
<o:p></o:p></span></p>
<div style="margin-bottom:15.0pt;overflow:auto" id="LPBorder_GT_15236288504800.6918023978429098">
<table class="MsoNormalTable" border="1" cellspacing="0" cellpadding="0" width="90%" style="width:90.0%;background:white;border-top:dotted #C8C8C8 1.0pt;border-left:none;border-bottom:dotted #C8C8C8 1.0pt;border-right:none">
<tbody>
<tr>
<td width="271" valign="top" style="width:187.5pt;border:none;padding:15.0pt 15.0pt 15.0pt .75pt">
<div style="margin-top:5.0pt;margin-bottom:5.0pt;display:table" id="LPImageContainer_15236288504780.13586488748843106">
<p class="MsoNormal" style="margin-top:15.0pt;background:white"><a href="https://en.wikipedia.org/wiki/Steve_Crocker" target="_blank"><span style="text-decoration:none"><img border="0" width="250" height="250" style="width:2.6041in;height:2.6041in" id="LPThumbnailImageID_15236288504780.980642281498494" src="https://upload.wikimedia.org/wikipedia/commons/b/b5/Steve_Crocker_%28square_crop%29.jpg"></span></a><o:p></o:p></p>
</div>
</td>
<td valign="top" style="border:none;padding:0in 0in 0in 0in;display:table-cell" id="TextCell_15236288504780.69497192206151">
<div id="LPTitle_15236288504780.21089502091117884">
<p class="MsoNormal" style="margin-top:15.0pt;mso-line-height-alt:15.75pt"><span style="font-size:16.0pt;font-family:"Segoe UI Light",sans-serif;color:#3B5777"><a href="https://en.wikipedia.org/wiki/Steve_Crocker" target="_blank"><span style="text-decoration:none">Steve
Crocker - Wikipedia</span></a><o:p></o:p></span></p>
</div>
<div style="margin-top:7.5pt;margin-bottom:12.0pt" id="LPMetadata_15236288504780.9903521366406721">
<p class="MsoNormal" style="margin-top:15.0pt;line-height:10.5pt"><span style="font-size:10.5pt;font-family:"Segoe UI",sans-serif;color:#666666">en.wikipedia.org<o:p></o:p></span></p>
</div>
<div id="LPDescription_15236288504800.510708807278161">
<p class="MsoNormal" style="margin-top:15.0pt;line-height:15.0pt"><span style="font-size:10.5pt;font-family:"Segoe UI",sans-serif;color:#666666">Stephen D. Crocker (born October 15, 1944, in Pasadena, California) is the inventor of the Request for Comments
series, authoring the very first RFC and many more. He received his bachelor's degree (1968) and PhD (1977) from the University of California, Los Angeles.<o:p></o:p></span></p>
</div>
</td>
</tr>
</tbody>
</table>
</div>
<p class="MsoNormal" style="margin-bottom:12.0pt"><span style="font-family:"Calibri",sans-serif;color:black"><o:p> </o:p></span></p>
<div>
<p class="MsoNormal"><span style="font-family:"Calibri",sans-serif;color:black">What: talk by Steve Crocker entitled "Why Isn't Verification Standard Practice?"
<o:p></o:p></span></p>
</div>
<div>
<p class="MsoNormal"><span style="font-family:"Calibri",sans-serif;color:black">When: Friday, April 13 at 2pm<o:p></o:p></span></p>
</div>
<div>
<p class="MsoNormal"><span style="font-family:"Calibri",sans-serif;color:black">Where:
<b>ARC 221 (NEW LOCATION)</b><o:p></o:p></span></p>
</div>
<p class="MsoNormal" style="margin-bottom:12.0pt"><span style="font-family:"Calibri",sans-serif;color:black"><br>
Steve's abstract is included once again below (apologies if you've received multiple copies of this mail). I hope to see many of you there!<o:p></o:p></span></p>
<div>
<p class="MsoNormal"><span style="font-family:"Calibri",sans-serif;color:black">- Gordon<br>
<br>
<o:p></o:p></span></p>
</div>
<div>
<div style="margin-top:14.0pt">
<p class="MsoNormal" style="text-align:justify"><b><span style="font-size:18.0pt;font-family:"Calibri",sans-serif;color:#4F81BD">Why Isn’t Verification Standard Practice?</span></b><span style="font-family:"Calibri",sans-serif;color:black"><o:p></o:p></span></p>
</div>
<p class="MsoNormal" align="center" style="text-align:center"><span style="font-family:"Calibri",sans-serif;color:black">Steve Crocker<o:p></o:p></span></p>
<div style="margin-top:14.0pt">
<p class="MsoNormal" style="text-align:justify"><b><span style="font-size:18.0pt;font-family:"Calibri",sans-serif;color:#4F81BD">Motivation</span></b><span style="font-family:"Calibri",sans-serif;color:black"><o:p></o:p></span></p>
</div>
<div>
<p class="MsoNormal"><span style="font-family:"Calibri",sans-serif;color:black"><o:p> </o:p></span></p>
</div>
<div>
<p class="MsoNormal"><span style="font-family:"Calibri",sans-serif;color:black">Despite big advances in proof systems, SMT solvers, higher order logic, etc. and some noteworthy successes in the use of formal methods in specific areas, e.g. for device drivers,
formal methods are still not in common use and low-level, “simple” bugs in critical software still bedevil us. Why don’t we have adequate tool support to catch those sorts of bugs before the software leaves the programmer’s desk?<o:p></o:p></span></p>
</div>
<div>
<p class="MsoNormal"><span style="font-family:"Calibri",sans-serif;color:black"><o:p> </o:p></span></p>
</div>
<div>
<p class="MsoNormal"><span style="font-family:"Calibri",sans-serif;color:black">The purpose of this talk is to provoke discussion of the question Why Isn’t Verification Standard Practice? To stimulate that discussion, I’ll sketch some thoughts about how to
fashion the tools. Strong arguments are welcome.<o:p></o:p></span></p>
</div>
<div style="margin-top:14.0pt">
<p class="MsoNormal" style="text-align:justify"><b><span style="font-size:18.0pt;font-family:"Calibri",sans-serif;color:#4F81BD">The Sketch</span></b><span style="font-family:"Calibri",sans-serif;color:black"><o:p></o:p></span></p>
</div>
<div>
<p class="MsoNormal"><span style="font-family:"Calibri",sans-serif;color:black"><o:p> </o:p></span></p>
</div>
<div>
<p class="MsoNormal"><span style="font-family:"Calibri",sans-serif;color:black">I think it is possible to put the pieces of this technology together in a way that achieves all of the following:<o:p></o:p></span></p>
</div>
<div>
<p class="MsoNormal"><span style="font-family:"Calibri",sans-serif;color:black"><o:p> </o:p></span></p>
</div>
<div>
<ul type="disc">
<li class="MsoNormal" style="color:black;mso-margin-top-alt:auto;margin-bottom:12.0pt;mso-list:l0 level1 lfo1">
<span style="font-family:"Calibri",sans-serif">Widespread, general use of formal proofs in all of the regularly used programming languages. This implies the methodology is usable and learnable.<o:p></o:p></span></li></ul>
</div>
<div>
<ul type="disc">
<li class="MsoNormal" style="color:black;mso-margin-top-alt:auto;margin-bottom:12.0pt;mso-list:l0 level1 lfo1">
<span style="font-family:"Calibri",sans-serif">Proofs of low-level properties, particularly integrity of data structures and termination.<o:p></o:p></span></li></ul>
</div>
<div>
<ul type="disc">
<li class="MsoNormal" style="color:black;mso-margin-top-alt:auto;margin-bottom:12.0pt;mso-list:l0 level1 lfo1">
<span style="font-family:"Calibri",sans-serif">Certainty about the proof process. The proof system should not be asked to solve unbounded or impossible problems, nor should it even have to work very hard. We need only for the proof system to see what the programmer
would expect another programmer to also see, i.e. what’s “obvious.” The programmer should know well what the proof system is able to prove.<o:p></o:p></span></li></ul>
</div>
<div>
<ul type="disc">
<li class="MsoNormal" style="color:black;mso-margin-top-alt:auto;margin-bottom:12.0pt;mso-list:l0 level1 lfo1">
<span style="font-family:"Calibri",sans-serif">Requires limited only annotation. As a guess, no more than 100% addition of text, and preferably less.<o:p></o:p></span></li></ul>
</div>
<div>
<ul type="disc">
<li class="MsoNormal" style="color:black;mso-margin-top-alt:auto;mso-margin-bottom-alt:auto;mso-list:l0 level1 lfo1">
<span style="font-family:"Calibri",sans-serif">Connected to the development environment. Most formal methods tools are separated from the development environments and run either as separate batch processes or separate interactive processes.<o:p></o:p></span></li></ul>
</div>
</div>
<p class="MsoNormal"><span style="font-family:"Calibri",sans-serif;color:black"><o:p> </o:p></span></p>
</div>
</body>
</html>
<head>
<meta http-equiv="Content-Type" content="text/html; charset=us-ascii">
<meta name="Generator" content="Microsoft Word 15 (filtered medium)">
<!--[if !mso]><style>v\:* {behavior:url(#default#VML);}
o\:* {behavior:url(#default#VML);}
w\:* {behavior:url(#default#VML);}
.shape {behavior:url(#default#VML);}
</style><![endif]--><style><!--
/* Font Definitions */
@font-face
{font-family:Wingdings;
panose-1:5 0 0 0 0 0 0 0 0 0;}
@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;}
@font-face
{font-family:"Frutiger 45 Light";
panose-1:2 11 5 0 0 0 0 0 0 0;}
@font-face
{font-family:"Segoe UI";
panose-1:2 11 5 2 4 2 4 2 2 3;}
@font-face
{font-family:"Segoe UI Light";
panose-1:2 11 5 2 4 2 4 2 2 3;}
/* Style Definitions */
p.MsoNormal, li.MsoNormal, div.MsoNormal
{margin:0in;
margin-bottom:.0001pt;
font-size:12.0pt;
font-family:"Times New Roman",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
{mso-style-priority:99;
margin:0in;
margin-bottom:.0001pt;
font-size:12.0pt;
font-family:"Times New Roman",serif;}
p.msonormal0, li.msonormal0, div.msonormal0
{mso-style-name:msonormal;
margin:0in;
margin-bottom:.0001pt;
font-size:12.0pt;
font-family:"Times New Roman",serif;}
span.EmailStyle19
{mso-style-type:personal-reply;
font-family:"Frutiger 45 Light";
color:#1F497D;}
.MsoChpDefault
{mso-style-type:export-only;
font-size:10.0pt;}
@page WordSection1
{size:8.5in 11.0in;
margin:1.0in 1.0in 1.0in 1.0in;}
div.WordSection1
{page:WordSection1;}
/* List Definitions */
@list l0
{mso-list-id:583995425;
mso-list-template-ids:-733208088;}
@list l0:level1
{mso-level-number-format:bullet;
mso-level-text:\F0B7;
mso-level-tab-stop:.5in;
mso-level-number-position:left;
text-indent:-.25in;
mso-ansi-font-size:10.0pt;
font-family:Symbol;}
@list l0:level2
{mso-level-number-format:bullet;
mso-level-text:o;
mso-level-tab-stop:1.0in;
mso-level-number-position:left;
text-indent:-.25in;
mso-ansi-font-size:10.0pt;
font-family:"Courier New";
mso-bidi-font-family:"Times New Roman";}
@list l0:level3
{mso-level-number-format:bullet;
mso-level-text:\F0A7;
mso-level-tab-stop:1.5in;
mso-level-number-position:left;
text-indent:-.25in;
mso-ansi-font-size:10.0pt;
font-family:Wingdings;}
@list l0:level4
{mso-level-number-format:bullet;
mso-level-text:\F0A7;
mso-level-tab-stop:2.0in;
mso-level-number-position:left;
text-indent:-.25in;
mso-ansi-font-size:10.0pt;
font-family:Wingdings;}
@list l0:level5
{mso-level-number-format:bullet;
mso-level-text:\F0A7;
mso-level-tab-stop:2.5in;
mso-level-number-position:left;
text-indent:-.25in;
mso-ansi-font-size:10.0pt;
font-family:Wingdings;}
@list l0:level6
{mso-level-number-format:bullet;
mso-level-text:\F0A7;
mso-level-tab-stop:3.0in;
mso-level-number-position:left;
text-indent:-.25in;
mso-ansi-font-size:10.0pt;
font-family:Wingdings;}
@list l0:level7
{mso-level-number-format:bullet;
mso-level-text:\F0A7;
mso-level-tab-stop:3.5in;
mso-level-number-position:left;
text-indent:-.25in;
mso-ansi-font-size:10.0pt;
font-family:Wingdings;}
@list l0:level8
{mso-level-number-format:bullet;
mso-level-text:\F0A7;
mso-level-tab-stop:4.0in;
mso-level-number-position:left;
text-indent:-.25in;
mso-ansi-font-size:10.0pt;
font-family:Wingdings;}
@list l0:level9
{mso-level-number-format:bullet;
mso-level-text:\F0A7;
mso-level-tab-stop:4.5in;
mso-level-number-position:left;
text-indent:-.25in;
mso-ansi-font-size:10.0pt;
font-family:Wingdings;}
ol
{margin-bottom:0in;}
ul
{margin-bottom:0in;}
--></style><!--[if gte mso 9]><xml>
<o:shapedefaults v:ext="edit" spidmax="1026" />
</xml><![endif]--><!--[if gte mso 9]><xml>
<o:shapelayout v:ext="edit">
<o:idmap v:ext="edit" data="1" />
</o:shapelayout></xml><![endif]-->
</head>
<body lang="EN-US" link="blue" vlink="purple">
<div class="WordSection1">
<p class="MsoNormal"><span style="font-family:"Calibri",sans-serif;color:black">Dear all,<br>
<br>
Friendly reminder: Steve Crocker (<a href="https://en.wikipedia.org/wiki/Steve_Crocker" id="LPlnk406363">https://en.wikipedia.org/wiki/Steve_Crocker</a> is giving a talk
<b>today at</b> <b>2pm in ARC 221 (NEW LOCATION)</b> on the question, Why Isn't Verification Standard Practice? I encourage all of you to attend.
<o:p></o:p></span></p>
<div style="margin-bottom:15.0pt;overflow:auto" id="LPBorder_GT_15236288504800.6918023978429098">
<table class="MsoNormalTable" border="1" cellspacing="0" cellpadding="0" width="90%" style="width:90.0%;background:white;border-top:dotted #C8C8C8 1.0pt;border-left:none;border-bottom:dotted #C8C8C8 1.0pt;border-right:none">
<tbody>
<tr>
<td width="271" valign="top" style="width:187.5pt;border:none;padding:15.0pt 15.0pt 15.0pt .75pt">
<div style="margin-top:5.0pt;margin-bottom:5.0pt;display:table" id="LPImageContainer_15236288504780.13586488748843106">
<p class="MsoNormal" style="margin-top:15.0pt;background:white"><a href="https://en.wikipedia.org/wiki/Steve_Crocker" target="_blank"><span style="text-decoration:none"><img border="0" width="250" height="250" style="width:2.6041in;height:2.6041in" id="LPThumbnailImageID_15236288504780.980642281498494" src="https://upload.wikimedia.org/wikipedia/commons/b/b5/Steve_Crocker_%28square_crop%29.jpg"></span></a><o:p></o:p></p>
</div>
</td>
<td valign="top" style="border:none;padding:0in 0in 0in 0in;display:table-cell" id="TextCell_15236288504780.69497192206151">
<div id="LPTitle_15236288504780.21089502091117884">
<p class="MsoNormal" style="margin-top:15.0pt;mso-line-height-alt:15.75pt"><span style="font-size:16.0pt;font-family:"Segoe UI Light",sans-serif;color:#3B5777"><a href="https://en.wikipedia.org/wiki/Steve_Crocker" target="_blank"><span style="text-decoration:none">Steve
Crocker - Wikipedia</span></a><o:p></o:p></span></p>
</div>
<div style="margin-top:7.5pt;margin-bottom:12.0pt" id="LPMetadata_15236288504780.9903521366406721">
<p class="MsoNormal" style="margin-top:15.0pt;line-height:10.5pt"><span style="font-size:10.5pt;font-family:"Segoe UI",sans-serif;color:#666666">en.wikipedia.org<o:p></o:p></span></p>
</div>
<div id="LPDescription_15236288504800.510708807278161">
<p class="MsoNormal" style="margin-top:15.0pt;line-height:15.0pt"><span style="font-size:10.5pt;font-family:"Segoe UI",sans-serif;color:#666666">Stephen D. Crocker (born October 15, 1944, in Pasadena, California) is the inventor of the Request for Comments
series, authoring the very first RFC and many more. He received his bachelor's degree (1968) and PhD (1977) from the University of California, Los Angeles.<o:p></o:p></span></p>
</div>
</td>
</tr>
</tbody>
</table>
</div>
<p class="MsoNormal" style="margin-bottom:12.0pt"><span style="font-family:"Calibri",sans-serif;color:black"><o:p> </o:p></span></p>
<div>
<p class="MsoNormal"><span style="font-family:"Calibri",sans-serif;color:black">What: talk by Steve Crocker entitled "Why Isn't Verification Standard Practice?"
<o:p></o:p></span></p>
</div>
<div>
<p class="MsoNormal"><span style="font-family:"Calibri",sans-serif;color:black">When: Friday, April 13 at 2pm<o:p></o:p></span></p>
</div>
<div>
<p class="MsoNormal"><span style="font-family:"Calibri",sans-serif;color:black">Where:
<b>ARC 221 (NEW LOCATION)</b><o:p></o:p></span></p>
</div>
<p class="MsoNormal" style="margin-bottom:12.0pt"><span style="font-family:"Calibri",sans-serif;color:black"><br>
Steve's abstract is included once again below (apologies if you've received multiple copies of this mail). I hope to see many of you there!<o:p></o:p></span></p>
<div>
<p class="MsoNormal"><span style="font-family:"Calibri",sans-serif;color:black">- Gordon<br>
<br>
<o:p></o:p></span></p>
</div>
<div>
<div style="margin-top:14.0pt">
<p class="MsoNormal" style="text-align:justify"><b><span style="font-size:18.0pt;font-family:"Calibri",sans-serif;color:#4F81BD">Why Isn’t Verification Standard Practice?</span></b><span style="font-family:"Calibri",sans-serif;color:black"><o:p></o:p></span></p>
</div>
<p class="MsoNormal" align="center" style="text-align:center"><span style="font-family:"Calibri",sans-serif;color:black">Steve Crocker<o:p></o:p></span></p>
<div style="margin-top:14.0pt">
<p class="MsoNormal" style="text-align:justify"><b><span style="font-size:18.0pt;font-family:"Calibri",sans-serif;color:#4F81BD">Motivation</span></b><span style="font-family:"Calibri",sans-serif;color:black"><o:p></o:p></span></p>
</div>
<div>
<p class="MsoNormal"><span style="font-family:"Calibri",sans-serif;color:black"><o:p> </o:p></span></p>
</div>
<div>
<p class="MsoNormal"><span style="font-family:"Calibri",sans-serif;color:black">Despite big advances in proof systems, SMT solvers, higher order logic, etc. and some noteworthy successes in the use of formal methods in specific areas, e.g. for device drivers,
formal methods are still not in common use and low-level, “simple” bugs in critical software still bedevil us. Why don’t we have adequate tool support to catch those sorts of bugs before the software leaves the programmer’s desk?<o:p></o:p></span></p>
</div>
<div>
<p class="MsoNormal"><span style="font-family:"Calibri",sans-serif;color:black"><o:p> </o:p></span></p>
</div>
<div>
<p class="MsoNormal"><span style="font-family:"Calibri",sans-serif;color:black">The purpose of this talk is to provoke discussion of the question Why Isn’t Verification Standard Practice? To stimulate that discussion, I’ll sketch some thoughts about how to
fashion the tools. Strong arguments are welcome.<o:p></o:p></span></p>
</div>
<div style="margin-top:14.0pt">
<p class="MsoNormal" style="text-align:justify"><b><span style="font-size:18.0pt;font-family:"Calibri",sans-serif;color:#4F81BD">The Sketch</span></b><span style="font-family:"Calibri",sans-serif;color:black"><o:p></o:p></span></p>
</div>
<div>
<p class="MsoNormal"><span style="font-family:"Calibri",sans-serif;color:black"><o:p> </o:p></span></p>
</div>
<div>
<p class="MsoNormal"><span style="font-family:"Calibri",sans-serif;color:black">I think it is possible to put the pieces of this technology together in a way that achieves all of the following:<o:p></o:p></span></p>
</div>
<div>
<p class="MsoNormal"><span style="font-family:"Calibri",sans-serif;color:black"><o:p> </o:p></span></p>
</div>
<div>
<ul type="disc">
<li class="MsoNormal" style="color:black;mso-margin-top-alt:auto;margin-bottom:12.0pt;mso-list:l0 level1 lfo1">
<span style="font-family:"Calibri",sans-serif">Widespread, general use of formal proofs in all of the regularly used programming languages. This implies the methodology is usable and learnable.<o:p></o:p></span></li></ul>
</div>
<div>
<ul type="disc">
<li class="MsoNormal" style="color:black;mso-margin-top-alt:auto;margin-bottom:12.0pt;mso-list:l0 level1 lfo1">
<span style="font-family:"Calibri",sans-serif">Proofs of low-level properties, particularly integrity of data structures and termination.<o:p></o:p></span></li></ul>
</div>
<div>
<ul type="disc">
<li class="MsoNormal" style="color:black;mso-margin-top-alt:auto;margin-bottom:12.0pt;mso-list:l0 level1 lfo1">
<span style="font-family:"Calibri",sans-serif">Certainty about the proof process. The proof system should not be asked to solve unbounded or impossible problems, nor should it even have to work very hard. We need only for the proof system to see what the programmer
would expect another programmer to also see, i.e. what’s “obvious.” The programmer should know well what the proof system is able to prove.<o:p></o:p></span></li></ul>
</div>
<div>
<ul type="disc">
<li class="MsoNormal" style="color:black;mso-margin-top-alt:auto;margin-bottom:12.0pt;mso-list:l0 level1 lfo1">
<span style="font-family:"Calibri",sans-serif">Requires limited only annotation. As a guess, no more than 100% addition of text, and preferably less.<o:p></o:p></span></li></ul>
</div>
<div>
<ul type="disc">
<li class="MsoNormal" style="color:black;mso-margin-top-alt:auto;mso-margin-bottom-alt:auto;mso-list:l0 level1 lfo1">
<span style="font-family:"Calibri",sans-serif">Connected to the development environment. Most formal methods tools are separated from the development environments and run either as separate batch processes or separate interactive processes.<o:p></o:p></span></li></ul>
</div>
</div>
<p class="MsoNormal"><span style="font-family:"Calibri",sans-serif;color:black"><o:p> </o:p></span></p>
</div>
</body>
</html>