<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:"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;
font-family:"Calibri",sans-serif;
color:#1F497D;}
span.EmailStyle20
{mso-style-type:personal-compose;
font-family:"Calibri",sans-serif;
color:windowtext;}
.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:1064598607;
mso-list-template-ids:1338519212;}
@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><span style="font-family:"Calibri",sans-serif;color:black">-- Apologies if you receive multiple copies. ---
<o:p></o:p></span></p>
<p><span style="font-family:"Calibri",sans-serif;color:black"><o:p> </o:p></span></p>
<div id="Item.MessageUniqueBody">
<div>
<div>
<div id="divtagdefaultwrapper">
<div>
<p class="MsoNormal"><span style="font-family:"Calibri",sans-serif;color:black">Hi all,<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 strongly encourage you to come see a talk by Steve Crocker (<a href="https://en.wikipedia.org/wiki/Steve_Crocker" id="LPlnk75779">https://en.wikipedia.org/wiki/Steve_Crocker</a>)
this Friday at 2pm in Stocker 326 (tentative location). Steve did his PhD work in formal methods, then later moved into networking. Abstract is below.
<o:p></o:p></span></p>
<div style="margin-bottom:15.0pt;overflow:auto" id="LPBorder_GT_15233762236620.71876375519053">
<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_15233762236600.17802455075811374">
<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_15233762236600.8521894446928898" 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_15233762236620.674723184602211">
<div id="LPTitle_15233762236620.6334169292441885">
<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_15233762236620.6149187296283717">
<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_15233762236620.5123950955725829">
<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"><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">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: Stocker 326 (tentative)<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">If you don't mind, please
<b>send me a quick note </b>by email (<a href="mailto:gstewart@ohio.edu">gstewart@ohio.edu</a>) if you plan to attend -- I want to make sure we reserve an appropriately sized room (Stocker 326 currently but possibly ARC 221 if we get many responses from you
and others). Note that this talk is in addition to Steve's keynote at ITS day on Thursday, April 12.<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">Thanks,<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">- Gordon<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>
<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>
</div>
</div>
</div>
</div>
<p class="MsoNormal"><span style="font-family:"Calibri",sans-serif;color:black"><o:p> </o:p></span></p>
<p><span style="font-family:"Calibri",sans-serif;color:black"><o:p> </o:p></span></p>
</div>
</body>
</html>