%!PS-Adobe-2.0
%%Title: atp-and-sys-ver.mss
%%DocumentFonts: (atend)
%%Creator: Dianne King and Scribe 7(1750)
%%CreationDate: 13 January 1992 12:55
%%Pages: (atend)
%%EndComments
% PostScript Prelude for Scribe.
/BS {/SV save def
/PH exch 100 div def
/PW exch 100 div def
0.0 PH translate
.01 -.01 scale} bind def
/ES {SV restore showpage} bind def
/SC {setrgbcolor} bind def
/FMTX matrix def
/RDF {WFT SLT 0.0 eq
{SSZ 0.0 0.0 SSZ neg 0.0 0.0 FMTX astore}
{SSZ 0.0 SLT neg sin SLT cos div SSZ mul SSZ neg 0.0 0.0 FMTX astore}
ifelse makefont setfont} bind def
/SLT 0.0 def
/SI { /SLT exch cvr def RDF} bind def
/WFT /Courier findfont def
/SF { /WFT exch findfont def RDF} bind def
/SSZ 1000.0 def
/SS { /SSZ exch 100.0 mul def RDF} bind def
/AF { /WFT exch findfont def /SSZ exch 100.0 mul def RDF} bind def
/MT /moveto load def
/PF{transform .25 sub round .25 add exch
.25 sub round .25 add exch itransform} bind def
/RPF{currentpoint exch 4 1 roll
add 3 1 roll add exch PF} bind def
/XM {currentpoint exch pop moveto} bind def
/UL {gsave newpath moveto dup 2.0 div 0.0 exch RPF moveto
setlinewidth 0.0 rlineto stroke grestore} bind def
/LH {gsave newpath PF moveto setlinewidth
0.0 rlineto
gsave stroke grestore} bind def
/LV {gsave newpath PF moveto setlinewidth
0.0 exch rlineto
gsave stroke grestore} bind def
/BX {gsave newpath PF moveto setlinewidth
exch
dup 0.0 RPF lineto
exch 0.0 exch neg RPF lineto
neg 0.0 RPF lineto
closepath
gsave stroke grestore} bind def
/BX1 {grestore} bind def
/BX2 {setlinewidth 1 setgray stroke grestore} bind def
/PB {/PV save def newpath translate
100.0 -100.0 scale pop /showpage {} def} bind def
/PE {PV restore} bind def
/GB {/PV save def newpath translate rotate
div dup scale 100.0 -100.0 scale /showpage {} def} bind def
/GE {PV restore} bind def
/FB {dict dup /FontMapDict exch def begin} bind def
/FM {cvn exch cvn exch def} bind def
/FE {end /original-findfont /findfont load def /findfont
{dup FontMapDict exch known{FontMapDict exch get} if
original-findfont} def} bind def
/BC {gsave moveto dup 0 exch rlineto exch 0 rlineto neg 0 exch rlineto closepath clip} bind def
/EC /grestore load def
/SH /show load def
/MX {exch show 0.0 rmoveto} bind def
/W {0 32 4 -1 roll widthshow} bind def
/WX {0 32 5 -1 roll widthshow 0.0 rmoveto} bind def
/RC {100.0 -100.0 scale
PW 0.0 translate
-90.0 rotate
.01 -.01 scale} bind def
/URC {100.0 -100.0 scale
90.0 rotate
PW neg 0.0 translate
.01 -.01 scale} bind def
/RCC {100.0 -100.0 scale
0.0 PH neg translate 90.0 rotate
.01 -.01 scale} bind def
/URCC {100.0 -100.0 scale
-90.0 rotate 0.0 PH translate
.01 -.01 scale} bind def
/CL {gsave newpath moveto setrgbcolor
exch
dup 0.0 rlineto
exch 0.0 exch neg rlineto
neg 0.0 rlineto
fill grestore} bind def
%%EndProlog
%%Page: 0 1
61200 79200 BS
0 SI
11 /Times-Roman AF
18144 29555 MT
(Technical Report 73)SH
37894 XM
(January, 1992)SH
10 SS
26167 52926 MT
(Computational Logic Inc.)SH
26014 54484 MT
(1717 W. 6th St. Suite 290)SH
27167 56042 MT
(Austin, Texas 78703)SH
28195 57600 MT
(\050512\051 322-9951)SH
19440 61385 MT
(This work was supported in part)
106 W( at Computational Logic,)105 W
19440 62490 MT
(Inc., by the Defense Advanced Research Projects Agency,)62 W
19440 63595 MT
(ARPA Order 7406. The views and conclusions contained)117 W
19440 64700 MT
(in this document are)
70 W( those of the author\050s\051 and should not)71 W
19440 65805 MT
(be interpreted as representing the official policies,)
173 W( either)172 W
19440 66910 MT
(expressed or implied, of Computational Logic, Inc., the)224 W
19440 68015 MT
(Defense Advanced Research Projects)
122 W( Agency or the U.S.)121 W
19440 69120 MT
(Government.)SH
14 /Times-Bold AF
21054 17138 MT
(The Role of Automated Reasoning)SH
27412 18940 MT
(in Integrated)SH
21015 20742 MT
(System Verification Environments)SH
12 /Times-Roman AF
27570 24445 MT
(Donald I. Good)SH
27503 25948 MT
(Matt Kaufmann)SH
27252 27451 MT
(J Strother Moore)SH
ES
%%Page: 0 2
61200 79200 BS
0 SI
13 /Times-Bold AF
28433 8071 MT
(Abstract)SH
10 /Times-Roman AF
9504 12357 MT
(This paper focuses on ``system verification,'' the)
28 W( activity of mechanically proving properties of computer)29 W
9504 13643 MT
(systems. Distinguishing)
782 W( characteristics of systems)
266 W( include their large size, their multiple layers of)265 W
9504 14929 MT
(abstraction, and their frequent concern with multiple programming languages)
296 W( and, more generally,)297 W
9504 16215 MT
(multiple models of computation. System verification)297 W
/Times-Italic SF
33194 XM
(systems)SH
/Times-Roman SF
36796 XM
(require supreme)
297 W( integration of their)296 W
9504 17501 MT
(component parts. To)
201 W( reason formally about systems one must be able to reason about the relations)202 W
9504 18787 MT
(between its disparate modules, layers of abstraction, and various models of computation. Facilitating)165 W
9504 20073 MT
(system verification is,)
196 W( we believe, the underlying theme of this ``Workshop on the Effective Use of)197 W
9504 21359 MT
(Automated Reasoning Technology in System Development.'')
127 W( We)
503 W( address that theme explicitly in this)126 W
9504 22645 MT
(paper. We)
284 W( make)
17 W( an important, often overlooked, but essentially trivial point: to reason formally about the)18 W
9504 23931 MT
(relations between)
208 W( various ideas, those ideas must be formalized. However, the popular approach to)207 W
9504 25217 MT
(imposing formal)
53 W( semantics on computational models, namely the creation of ``formula generators,'' fails)54 W
9504 26503 MT
(to formalize the very ideas allegedly being studied. In our view, this explains)
138 W( why so much work on)137 W
9504 27789 MT
(system verification is thwarted by ``integration problems.'' These ``integration problems'')
296 W( simply)297 W
9504 29075 MT
(disappear when)
202 W( the ideas being studied are formalized and available for logical manipulation by the)201 W
9504 30361 MT
(automated reasoning system. Our observations are supported by our experience in)
6 W( verifying several of the)7 W
9504 31647 MT
(largest systems studied to date.)SH
ES
%%Page: 1 3
61200 79200 BS
0 SI
13 /Times-Bold AF
28759 8071 MT
(Preface)SH
10 /Times-Roman AF
9504 12357 MT
(The introductory discussion in the call for)
134 W( papers for this workshop mentions)133 W
/Times-Italic SF
42214 XM
(system)SH
/Times-Roman SF
45263 XM
(specification and)133 W
9504 13643 MT
(verification repeatedly. For example, it says ``The purpose of)
98 W( this workshop is to explore issues in the)99 W
9504 14929 MT
(application of)
80 W( automated reasoning technology to)79 W
/Times-Italic SF
30032 XM
(systems)SH
/Times-Roman SF
33416 XM
(with critical requirements'' [emphasis added].)79 W
9504 16215 MT
(System verification, as opposed to the more limited area of program verification, is a topic)
82 W( of particular)83 W
9504 17501 MT
(concern to those)
26 W( of us at Computational Logic, Inc. \050CLI\051. We find ourselves compelled to respond to all)25 W
9504 18787 MT
(six of the announced ``Areas of Interest.'' These may be summarized as follows:)SH
/Symbol SF
11794 20240 MT
(\267)SH
/Times-Roman SF
12504 XM
(Applying Different Tools to the Same Problem)SH
/Symbol SF
11794 21998 MT
(\267)SH
/Times-Roman SF
12504 XM
(Exchanging Data)SH
/Symbol SF
11794 23756 MT
(\267)SH
/Times-Roman SF
12504 XM
(Exchanging Code)SH
/Symbol SF
11794 25514 MT
(\267)SH
/Times-Roman SF
12504 XM
(Interface Logics)SH
/Symbol SF
11794 27272 MT
(\267)SH
/Times-Roman SF
12504 XM
(User Interfaces and Interaction Styles)SH
/Symbol SF
11794 29030 MT
(\267)SH
/Times-Roman SF
12504 XM
(Significant System Verification Applications)SH
9504 30369 MT
(We will speak to each of these issues in turn, all within the context of)208 W
/Times-Italic SF
40676 XM
(system)SH
/Times-Roman SF
43800 XM
(verification. In)
666 W( our)208 W
9504 31655 MT
(companion submission to this workshop,)
100 W( [1],)
SH( we discuss the possible)
100 W( use of interface logics in program)99 W
9504 32941 MT
(verification.)SH
9504 35513 MT
(However, a general theme running throughout this paper is what we will call the)SH
/Times-Bold SF
10254 37123 MT
(Fundamental Admonition)SH
/Times-Roman SF
(:)SH
/Times-Italic SF
10254 38228 MT
(To reason formally about an idea you must formalize the idea)SH
/Times-Roman SF
(.)SH
9504 39838 MT
(Put another way, if you wish)
248 W( to study an idea formally, you must cast the idea into some formal)249 W
9504 41124 MT
(mathematical logic.)SH
9504 43696 MT
(Unfortunately, a popular approach to verification is the ``formula generator'' approach.)
185 W( A)
618 W( ``formula)184 W
9504 44982 MT
(generator'' is a computer program that models some aspect of computation)
291 W( such as programming)292 W
9504 46268 MT
(language semantics, security, performance, concurrency,)
122 W( etc. We call these ``computational models.'')121 W
8 SS
51800 45923 MT
(1)SH
10 SS
9504 47554 MT
(For expository reasons, let us fix upon the most common kind of formula generator, a)
193 W( ``verification)194 W
9504 48840 MT
(condition generator'' or ``vcg'' program. Such a program is)
3 W( a procedure which implicitly represents some)2 W
9504 50126 MT
(of the semantics of some particular programming language. Let us suppose)
211 W( we have a vcg for the)212 W
9504 51412 MT
(language L. Applied to)
34 W( a particular program in L and its specification, the vcg will formalize the problem)33 W
9504 52698 MT
(``does this program satisfy its specification?'')
244 W( by converting it to the problem ``are these formulas)245 W
9504 53984 MT
(theorems?'' If)
326 W( one)
38 W( wishes to study particular programs of L, then vcgs are adequate formalizing devices.)37 W
9504 55270 MT
(This explains their historical relevance to verification.)SH
9504 57842 MT
(Now suppose one is interested)
176 W( in verifying a system in which L is one of the computational models)177 W
9504 59128 MT
(provided or involved. If)
47 W( all we can do with the vcg for L is apply it to particular programs, then it is not)46 W
9504 60414 MT
(possible to answer questions about)
29 W( L, such as ``is L implemented by this system?'', ``does L permit these)30 W
9504 61700 MT
(bad transitions?'',)
124 W( ``how fast does L execute under this model?'' But these are the kinds of questions)123 W
9504 62986 MT
(asked in a systems context.)SH
9504 65558 MT
(In general, formula generators)
47 W( procedurally encode the semantics of some computational model, but they)48 W
10800 50 9504 68504 UL
6 SS
10304 69843 MT
(1)SH
8 SS
10604 70152 MT
(By ``computational model'' we mean to)
173 W( include universal models of computation such as the Turing machine model and)172 W
9504 71076 MT
(lambda-calculus, but also)
86 W( to include less sweeping models of computation such as security models, performance models, or even)87 W
9504 72000 MT
(models of local relevance only such as the integrity model of some particular data base or spread sheet system.)SH
ES
%%Page: 2 4
61200 79200 BS
0 SI
10 /Times-Roman AF
51700 4286 MT
(2)SH
9504 7886 MT
(do not formalize that model \050unless the formula generator is,)
50 W( itself, written in a language which has been)49 W
9504 9172 MT
(formalized\051. Thus,)
666 W( in a systems context, they do not offer a workable response to the fundamental)209 W
9504 10458 MT
(admonition: formalize the ideas you want to reason about.)SH
9504 13030 MT
(Perhaps because systems are so)
5 W( complicated, this simple fact is often overlooked. Rather than formalizing)4 W
9504 14316 MT
(the various layers of abstraction and the computational models of local interest to)
43 W( the system, researchers)44 W
9504 15602 MT
(often attack system)
145 W( verification problems by building additional formula generators \050e.g., that produce)144 W
9504 16888 MT
(formulas that)
102 W( establish that a particular program doesn't violate any of the integrity rules\051 and other)103 W
/Times-Italic SF
51200 XM
(ad)SH
9504 18174 MT
(hoc)SH
/Times-Roman SF
11235 XM
(``specification processors.'' These tools are built in an attempt to deal with an unavoidable problem,)37 W
9504 19460 MT
(namely the complexity of the system, by introducing)
12 W( abstractions. This need for abstraction is an inherent)13 W
9504 20746 MT
(property of systems and will arise even if)
21 W( the system being studied is not an operating system or universal)20 W
9504 22032 MT
(computational paradigm but is just a data base or spread)
257 W( sheet or word processor. Abstraction is)258 W
9504 23318 MT
(necessary. But)
776 W( formula generators are an unworkable response because they do)
263 W( not formalize the)262 W
9504 24604 MT
(abstractions and thus do not permit)
132 W( one to reason about relationships between them. The result is the)133 W
9504 25890 MT
(feeling that one has)
217 W( many formula generators that deal with aspects of the system but they are not)216 W
9504 27176 MT
(``integrated.'' But)
250 W( the problem is not one of integration so much as it is one of formalization.)SH
9504 29748 MT
(In our opinion, the fundamental admonition, when taken in a systems context, requires the following)175 W
9504 31034 MT
(responses, in roughly the order listed:)SH
11504 32373 MT
(1.)SH
12504 XM
(choose a mathematical logic,)SH
11504 34131 MT
(2.)SH
12504 XM
(formalize the relevant computational models in that logic,)SH
11504 35889 MT
(3.)SH
12504 XM
(choose or develop some automated reasoning tools to support the chosen logic,)SH
11504 37647 MT
(4.)SH
12504 XM
(explicate each computational model, i.e., develop within the logic a ``reusable theory'')223 W
12504 38752 MT
(about each model so that)
103 W( high-level proofs can be constructed by the reasoning tools, and)104 W
12504 39857 MT
(then)SH
11504 41615 MT
(5.)SH
12504 XM
(apply the tools and the theories to reason about the system.)SH
9504 42954 MT
(Today, the first three steps are often interwoven. System developers who)
223 W( do not wish to work on)222 W
9504 44240 MT
(automated reasoning)
86 W( tools should choose a logic already supported by such tools. As time goes on and)87 W
9504 45526 MT
(more computational models are formalized and explicated within mechanically supported logics, system)84 W
9504 46812 MT
(verification gets easier; it may ultimately become merely)
149 W( a matter of acquiring the appropriate formal)150 W
9504 48098 MT
(models and their reusable theories and then reasoning about)
134 W( the relationships relevant to the particular)133 W
9504 49384 MT
(system being studied. However, because system development so often involves the creation of new)197 W
9504 50670 MT
(computational paradigms, we suspect there will)
168 W( always be some need to formalize and explicate new)167 W
9504 51956 MT
(models.)SH
9504 54528 MT
(The five-step program outlined above has been followed)
50 W( repeatedly by numerous researchers and has led)51 W
9504 55814 MT
(to excellent)
37 W( results. The largest systems verified to date have been verified by this approach. Where this)36 W
9504 57100 MT
(methodology is)
69 W( practiced, systems verification is alive and well and fully integrated tool sets proliferate.)70 W
9504 58386 MT
(But the)
297 W( tools are logical entities such as formal models of computations, reusable theories, proof)296 W
9504 59672 MT
(strategies, etc., not formula generator programs.)SH
9504 62244 MT
(The structure of this paper is parallel to the Call for Papers for the workshop. We display in italics each)56 W
9504 63530 MT
(``area of interest,'' taken verbatim from the Call for Papers.)
69 W( We)
386 W( add a final unsolicited item of interest,)68 W
9504 64816 MT
(namely the view of verification as an engineering activity.)SH
ES
%%Page: 3 5
61200 79200 BS
0 SI
10 /Times-Roman AF
51700 4286 MT
(3)SH
12 /Times-Bold AF
9504 8004 MT
(1. Applying)
300 W( Different Tools to the Same Problem)SH
10 /Times-Italic AF
9504 10472 MT
(1. Applications of different automated reasoning tools to the same problem or specification.)SH
11 /Times-Bold AF
9504 13369 MT
(1.1 An)
275 W( Integrated System Verification Environment)SH
10 /Times-Roman AF
9504 15707 MT
(At CLI we have a)
97 W( wide variety of automated reasoning tools. One tool allows us to analyze hardware,)98 W
9504 16993 MT
(both for functional correctness and for such ``intensional'' properties as gate delay)
90 W( and the adequacy of)89 W
9504 18279 MT
(the loads and drives through a netlist. Another tool)
33 W( supports formal reasoning about a machine language.)34 W
9504 19565 MT
(A third supports formal reasoning about an assembly language. A fourth supports formal)
21 W( reasoning about)20 W
9504 20851 MT
(a high-level Pascal-like language. These four tools are completely integrated.)
134 W( We)
520 W( can freely mix the)135 W
9504 22137 MT
(analysis of functional correctness, timing, and other intensional properties at all levels.)
32 W( We)
313 W( can build and)31 W
9504 23423 MT
(verify systems at any one of these)
160 W( levels of abstraction. More interestingly, we can build and verify)161 W
9504 24709 MT
(systems that span)
137 W( many levels of abstraction and involve hundreds of modules at each level. We can)136 W
9504 25995 MT
(smoothly move from the highest levels of a)
104 W( system \050e.g., the properties of application programs\051 to the)105 W
9504 27281 MT
(lowest \050e.g., the gate-delay through a given hardware module\051.)SH
11 /Times-Bold AF
9504 30178 MT
(1.2 The)
275 W( FM8502 Short Stack)SH
10 /Times-Roman AF
9504 32516 MT
(This integration was achieved as follows. During the period 1985-1988, we and our)
91 W( colleagues at CLI,)90 W
9504 33802 MT
(working concurrently and only loosely coordinated,)
273 W( used the Nqthm \050``Boyer-Moore''\051 logic)
274 W( [2])
SH( to)274 W
9504 35088 MT
(formalize the semantics of a series of computational engines consisting of a)
122 W( gate-level register transfer)121 W
9504 36374 MT
(machine, a machine code \050``FM8502''\051,)
204 W( an assembly language \050``Piton''\051, and a high-level language)205 W
9504 37660 MT
(\050``Micro-Gypsy''\051. Each)
626 W( model was formalized operationally in the Nqthm logic \050though the use of)187 W
9504 38946 MT
(operational semantics)
177 W( is irrelevant to our argument\051; however, the models differ significantly in style)178 W
9504 40232 MT
(because they were formalized by different people. In)
59 W( addition, ``transducers'' were defined that mapped)58 W
9504 41518 MT
(between the different models: a ``compiler'' mapped from the high-level language)
60 W( to the assembly code,)61 W
9504 42804 MT
(an assembler and linker mapped down to the binary machine code, and a loader mapped down to the)146 W
9504 44090 MT
(initialization of the gate-level machine. These transducers were)
52 W( defined as functions in the Nqthm logic.)53 W
9504 45376 MT
(Each transducer was proved to preserve, in a certain sense, the semantics of the appropriate)
12 W( computational)11 W
9504 46662 MT
(models. These)
626 W( proofs were constructed with Nqthm and)
188 W( its interactive proof-checker, Pc-Nqthm)
189 W( [3].)SH
9504 47948 MT
(These theorems were then combined to obtain a proof of a formula that states, roughly, that)
138 W( if a non-)137 W
9504 49234 MT
(erroneous high-level program is compiled,)
183 W( assembled, linked, loaded, and run on the register-transfer)184 W
9504 50520 MT
(machine, then the answer produced by that machine agrees with that specified by the high-level)
23 W( language.)22 W
9504 51806 MT
(This assemblage is called the ``FM8502 short stack.'' See)
69 W( [4])
SH( for an introduction to our)
69 W( approach and a)70 W
9504 53092 MT
(discussion of each of the components.)SH
11 /Times-Bold AF
9504 55989 MT
(1.3 Nqthm: A)
275 W( Verification Shell?)SH
10 /Times-Roman AF
9504 58327 MT
(As a side-effect of this work, we developed reusable libraries of lemmas in the)
58 W( Nqthm logic that convert)57 W
9504 59613 MT
(the general-purpose Nqthm theorem prover into a special-purpose machine for reasoning about)
267 W( the)268 W
9504 60899 MT
(particular language concerned. For example, when)
42 W( operating under the ``Piton library,'' Nqthm becomes)41 W
9504 62185 MT
(an engine for reasoning about Piton. But when the Micro-Gypsy library is loaded,)
14 W( Nqthm is an engine for)15 W
9504 63471 MT
(reasoning about Micro-Gypsy. Thus, in some real and practical sense, we have built and mixed)295 W
9504 64757 MT
(verification environments for a hardware design language, a machine code, an assembly language, and)127 W
9504 66043 MT
(Micro-Gypsy. Indeed,)
364 W( we have used)
57 W( these ``verification environments'' independently of the short stack)56 W
9504 67329 MT
(to verify properties of programs written in the individual languages. See for example [5].)SH
9504 69901 MT
(We have also derived performance)
75 W( bounds on high-level programs in the sense that the proofs give us a)76 W
9504 71187 MT
(constructive characterization of the number of microcode cycles)
168 W( that must be executed to carry out a)167 W
ES
%%Page: 4 6
61200 79200 BS
0 SI
10 /Times-Roman AF
51700 4286 MT
(4)SH
9504 7886 MT
(high-level computation. These ``clock)
122 W( functions'' are, of course, hierarchically developed in the sense)123 W
9504 9172 MT
(that we)
85 W( measure the performance of Micro-Gypsy programs in terms of assembly language instructions,)84 W
9504 10458 MT
(assembly code in terms of machine instructions,)
35 W( and machine instructions in terms of microcycles. Thus,)36 W
9504 11744 MT
(we have verification environments that let us do performance analysis on programs in)
114 W( several different)113 W
9504 13030 MT
(languages, these languages are connected by verified transducers, and the)
105 W( verification environments are)106 W
9504 14316 MT
(totally integrated.)SH
11 /Times-Bold AF
9504 17213 MT
(1.4 The)
275 W( FM9001 Short Stack)SH
10 /Times-Roman AF
9504 19551 MT
(Since the FM8502 short stack was)
206 W( reported in 1989, Warren Hunt and Bishop Brock, of CLI, have)205 W
9504 20837 MT
(fabricated \050a successor)
123 W( to\051 the register-transfer layer in silicon. This required formalizing a significant)124 W
9504 22123 MT
(fragment of a commercial hardware description language \050the NDL)
170 W( language of LSI Logic, Inc.\051 and)169 W
9504 23409 MT
(capturing the semantic properties of)
197 W( the conventional ``off-the-shelf'' hardware modules used in LSI)198 W
9504 24695 MT
(Logic designs. In the new language)
39 W( we also address certain other inadequacies of our earlier approach to)38 W
9504 25981 MT
(hardware; in particular, it is now possible to analyze formally such design aspects)
134 W( as the fanout, gate-)135 W
9504 27267 MT
(delay, and the)
80 W( adequacy of the electrical loads and drives through the netlist. We then re-expressed our)79 W
9504 28553 MT
(chip design in the new language.)
21 W( This)
294 W( slightly changed the machine code implemented by our device and)22 W
9504 29839 MT
(so the)
52 W( semantic definition of the machine code was altered. Because fabrication was intended, we added)51 W
9504 31125 MT
(scan chains and other)
SH( considerations to allow for post-fabrication testing. The hardware was mechanically)1 W
9504 32411 MT
(verified with Nqthm)
52 W( to implement the new machine code. The new device, called the FM9001, has now)51 W
9504 33697 MT
(been fabricated by LSI Logic, Inc., and is being tested at CLI.)SH
9504 36269 MT
(Thus, we added to)
215 W( our tool kit an integrated verification environment for a subset of a commercial)216 W
9504 37555 MT
(hardware description language, including features for analyzing fanout, gate)
35 W( delay, loads and drives. The)34 W
9504 38841 MT
(reusable library for this language has since been used)
179 W( to verify the design of a Byzantine agreement)180 W
9504 40127 MT
(chip [6].)SH
9504 42699 MT
(Because we formalized LSI Logic's NDL we can also use commercial tools to)
164 W( analyze our hardware)163 W
9504 43985 MT
(designs. We)
318 W( have used Nqthm to verify the logical and some performance properties of chip designs and)35 W
9504 45271 MT
(then used LSI Logic tools to do electrical analysis, layout,)
72 W( schematic liberation, and fabrication. This is)71 W
9504 46557 MT
(another example of the application of different tools to the same problem. See [6] for an example.)SH
9504 49129 MT
(Upon the fabrication of the)
52 W( FM9001, we ``ported'' the old stack proof to the new machine using Nqthm.)53 W
9504 50415 MT
(This required modifying the linker so as to generate the binary appropriate for the new machine.)
84 W( Other)417 W
9504 51701 MT
(changes were made in anticipation of actually running)
54 W( the device \050e.g., we arranged to lay out the binary)55 W
9504 52987 MT
(in a designated portion of memory so that memory-mapped io could)
46 W( be used\051. The new assembler/linker)45 W
9504 54273 MT
(was re-verified with Nqthm from a)
142 W( modified version of the old proof script. Because the upper level)143 W
9504 55559 MT
(specification of)
12 W( the assembler did not change, it was logically unnecessary to re-verify the higher levels of)11 W
9504 56845 MT
(the stack. The entire port took less than one man-week.)SH
11 /Times-Bold AF
9504 59742 MT
(1.5 Integrating)
275 W( Verification Tools)SH
10 /Times-Roman AF
9504 62080 MT
(In summary, at CLI we have a wide variety of integrated verification)
167 W( environments in which we can)168 W
9504 63366 MT
(analyze hardware designs and several different programming languages. We can)
286 W( mix correctness,)285 W
9504 64652 MT
(performance and other analyses. We can address)
117 W( ourselves to properties of particular programs and to)118 W
9504 65938 MT
(properties of particular programming languages. We can smoothly move from the highest levels)
147 W( of a)146 W
9504 67224 MT
(system to the lowest.)SH
9504 69796 MT
(This was not achieved by the adoption of an interface logic, disparate formula generators and the)
11 W( cobbling)12 W
9504 71082 MT
(together of a bunch of random tools. We do not)
112 W( believe that the integrated verification systems of the)111 W
ES
%%Page: 5 7
61200 79200 BS
0 SI
10 /Times-Roman AF
51700 4286 MT
(5)SH
9504 7886 MT
(future will be built that way either.)SH
9504 10458 MT
(We propose a different and far more flexible and powerful role)
219 W( for logic and automated reasoning:)220 W
9504 11744 MT
(describe your problem)
100 161 WX(\320)SH
/Times-Italic SF
20024 XM
(your whole problem)161 W
/Times-Roman SF
28501 XM
(\320)
100 MX(in a)
161 W( suitable logic and then reason about it with your)160 W
9504 13030 MT
(theorem prover. In this approach, the)
307 W( first step is to choose a logic suitable for expressing the)308 W
9504 14316 MT
(computational models of interest. This logic will be the)
215 W( ``implementation language'' of the system)214 W
9504 15602 MT
(verification system in the sense that the computatational models of interest must be)
14 W( expressed in the logic.)15 W
9504 16888 MT
(The chosen logic must be supported by a powerful general-purpose theorem prover. If one is)
32 W( unavailable)31 W
9504 18174 MT
(for the chosen logic,)
87 W( one must be built; this task is hard. System developers wishing to avoid it should)88 W
9504 19460 MT
(choose a logic that is)
103 W( mechanically supported. The automated reasoning system is essentially a system)102 W
9504 20746 MT
(verification system shell; both the development and the application of the)
26 W( verification system proceeds by)27 W
9504 22032 MT
(interacting with the automated reasoning system. In particular, the verification system is built by:)SH
/Symbol SF
11794 23485 MT
(\267)SH
/Times-Roman SF
12504 XM
(acquiring or developing formal models of the computational paradigms involved; and then)SH
/Symbol SF
11794 25243 MT
(\267)SH
/Times-Roman SF
12504 XM
(acquiring or developing reusable theories, tactics, etc., that explicate)
119 W( those models so that)118 W
12504 26348 MT
(high-level proofs are convenient.)SH
9504 28920 MT
(A mathematical analogy may be in order: logic can be used to reason about)
45 W( numbers and to reason about)46 W
9504 30206 MT
(sets. The)
256 W( activity of reasoning is the same in both cases; it is only the)
3 W( data \050i.e., the axioms\051 that lead us to)2 W
9504 31492 MT
(call one activity ``number theory'' and the other ``set theory.'' This is the power of logic. To gain)
13 W( access)14 W
9504 32778 MT
(to this power you must cast your problem into logic.)SH
9504 35350 MT
(The activity of reasoning is implemented by mechanized)
128 W( reasoning systems. When operating with the)127 W
9504 36636 MT
(axioms of number theory, the theorem)
3 W( prover is doing number theory. When operating with the axioms of)4 W
9504 37922 MT
(set theory, the theorem prover is doing set theory.)SH
9504 40494 MT
(Specialized verification environments for two different computational paradigms can be)
207 W( built from a)206 W
9504 41780 MT
(single theorem prover and logic.)83 W
/Times-Italic SF
23472 XM
(Nqthm operating with two distinct data)
83 W( bases is as surely two distinct)84 W
9504 43066 MT
(verifiers as would be obtained by implementing them independently in a common programming language.)SH
/Times-Roman SF
9504 45638 MT
(From a systems perspective, however, there is a crucial difference)
289 W( between our approach and the)288 W
9504 46924 MT
(alternative of independently implementing two theorem provers: if)
312 W( our approach is followed it is)313 W
9504 48210 MT
(immediately possible to)
216 W( reason about the union of the two models, i.e., about their interactions and)215 W
9504 49496 MT
(relationships.)SH
9504 52068 MT
(Nqthm has been used \050or is being used\051 to formalize and explicate)SH
/Symbol SF
11794 53521 MT
(\267)SH
/Times-Roman SF
12504 XM
(a commercial netlist language [6],)SH
/Symbol SF
11794 55279 MT
(\267)SH
/Times-Roman SF
12504 XM
(a gate-level description of a microprocessor [7],)SH
/Symbol SF
11794 57037 MT
(\267)SH
/Times-Roman SF
12504 XM
(a model of asynchrony suitable to proving the reliability of)
146 W( communication protocols for)147 W
12504 58142 MT
(independently-clocked processors [8],)SH
/Symbol SF
11794 59900 MT
(\267)SH
/Times-Roman SF
12504 XM
(Turing machines [9],)SH
/Symbol SF
11794 61658 MT
(\267)SH
/Times-Roman SF
12504 XM
(Lambda calculus [10],)SH
/Symbol SF
11794 63416 MT
(\267)SH
/Times-Roman SF
12504 XM
(a simple but usable machine code [11],)SH
/Symbol SF
11794 65174 MT
(\267)SH
/Times-Roman SF
12504 XM
(a large part of the machine code for the MC68020 [12],)SH
/Symbol SF
11794 66932 MT
(\267)SH
/Times-Roman SF
12504 XM
(a stack-based assembly language [5],)SH
/Symbol SF
11794 68690 MT
(\267)SH
/Times-Roman SF
12504 XM
(several high level languages including Micro-Gypsy)
164 W( [13],)
SH( Middle-Gypsy)
164 W( [14],)
SH( the Nqthm)164 W
12504 69795 MT
(logic itself [2], and a small subset of Ada [15],)SH
/Symbol SF
11794 71553 MT
(\267)SH
/Times-Roman SF
12504 XM
(a home-grown separation kernel \050implementing multi-processing on a uniprocessor\051 [16],)SH
ES
%%Page: 6 8
61200 79200 BS
0 SI
10 /Times-Roman AF
51700 4286 MT
(6)SH
/Symbol SF
11794 8000 MT
(\267)SH
/Times-Roman SF
12504 XM
(a requirements model for the Mach micro-kernel, and)SH
/Symbol SF
11794 9758 MT
(\267)SH
/Times-Roman SF
12504 XM
(the Unity system \050a model of the Misra-Chandy language for describing)
104 W( nondeterministic,)105 W
12504 10863 MT
(distributed, concurrent programs\051 [17].)SH
9504 12202 MT
(All of these)
149 W( computational models are integrated in the sense that we can formally reason about their)148 W
9504 13488 MT
(interactions. \050See)
250 W( however the footnote about ``Nthm'' on page 9.\051)SH
9504 16060 MT
(This is not to say that Nqthm's logic or)
75 W( its proof engine are ideal; far from it. But their clumsiness and)76 W
9504 17346 MT
(inadequacy are greatly)
83 W( offset by the leverage obtained by casting problems formally and using logic the)82 W
9504 18632 MT
(way it was intended: to reason about formal)
3 W( objects. Nqthm's success can perhaps be attributed to the fact)4 W
9504 19918 MT
(that its users have ``bitten the bullet'' and truly formalized their problems.)SH
11 /Times-Bold AF
9504 22815 MT
(1.6 Does)
275 W( the Approach Scale?)SH
10 /Times-Roman AF
9504 25153 MT
(A standard misconception is that this approach is merely an elegant ``toy'' that will not ``scale.'')
50 W( In)
348 W( this)49 W
9504 26439 MT
(section, by ``scale'' we mean ``remain)
88 W( manageable as applications approach the complexity of practical)89 W
9504 27725 MT
(systems.'' Later,)
376 W( in Section 7, we discuss a)
63 W( second sense of the word ``scale'' where we mean ``remain)62 W
9504 29011 MT
(viable in an industrial setting.'')SH
9504 31583 MT
(The suggestion that the fundamental admonition is an ideal that only works on)
33 W( ``toy'' examples is simply)34 W
9504 32869 MT
(inconsistent with the fact that)58 W
/Times-Italic SF
21821 XM
(systems verified by this method already approach realistic)
58 W( complexity)57 W
/Times-Roman SF
(. To)364 W
9504 34155 MT
(support this claim we will briefly indicate the)
72 W( complexity of some Nqthm system applications. Because)73 W
9504 35441 MT
(we don't know how to quantify complexity, we)
110 W( will simply describe the verified systems, emphasizing)109 W
9504 36727 MT
(quantitative aspects and peeling back the first layer of abstraction.)SH
11 /Times-Bold AF
9504 39624 MT
(1.6-A The)
275 W( Complexity of the FM9001 Short Stack)SH
10 /Times-Roman AF
9504 41962 MT
(The short stack involves four main models of computation: a hardware)
28 W( description language, the FM9001)29 W
9504 43248 MT
(machine code, the Piton assembly language, and the Micro-Gypsy programming)
325 W( language. Each)324 W
9504 44534 MT
(successive layer was proved to have been correctly implemented on top of the previous one.)SH
9504 47106 MT
(The hardware description language permits the description of modules composed of connected)
40 W( primitives)41 W
9504 48392 MT
(and other modules. Approximately 60)
150 W( primitives are supported. The particular primitives chosen are)149 W
9504 49678 MT
(among those supported by LSI Logic Inc's language NDL. The)
14 W( model permits reasoning about the values)15 W
9504 50964 MT
(delivered by modules as well as gate-delay, fanout, and the loads and)
112 W( drives requirements. The model)111 W
9504 52250 MT
(provides both two-valued)
139 W( \050true and false\051 and a four-valued \050true, false, undefined, and indeterminate\051)140 W
9504 53536 MT
(semantics. An)
408 W( extensive reusable library)
79 W( makes it convenient to reason about modules. About one-half)78 W
9504 54822 MT
(page of Lisp code is sufficient to translate our)
106 W( formal hardware description language into the syntax of)107 W
9504 56108 MT
(LSI Logic's NDL and hence use commercial layout and fabrication tools on the same designs. This)
12 W( direct)11 W
9504 57394 MT
(translation to)
222 W( NDL \050it is almost a lexeme-by-lexeme transliteration from parse-tree form to external)223 W
9504 58680 MT
(syntax\051 is an informal demonstration of the relevance of our formal model.)SH
9504 61252 MT
(Using the formal hardware description language, Brock and Hunt designed the FM9001, a simple)
74 W( 32-bit)73 W
9504 62538 MT
(microprocessor. The)
276 W( user-visible state of)
13 W( the FM9001 includes a general-purpose 16-element register file,)14 W
9504 63824 MT
(four arithmetic flags, and the external memory. Register 15)
34 W( is overloaded to contain the program counter)33 W
9504 65110 MT
(address, but in all other respects operates like the other registers. The implementation allows any)
69 W( of the)70 W
9504 66396 MT
(16 registers to be used as the program counter.)SH
9504 68968 MT
(Each FM9001 instruction fetches operand A, then)
55 W( fetches operand B if necessary, computes a result, and)54 W
9504 70254 MT
(stores the result in the location referenced by operand B. There are)
69 W( two instruction formats \050two-address)70 W
9504 71540 MT
(format and immediate datum)
107 W( format\051. Except for the immediate datum mode there are four addressing)106 W
ES
%%Page: 7 9
61200 79200 BS
0 SI
10 /Times-Roman AF
51700 4286 MT
(7)SH
9504 7886 MT
(modes: register direct, register indirect, register indirect)
167 W( with pre-increment, and register indirect with)168 W
9504 9172 MT
(post-increment. Thus,)
370 W( the FM9001 has five addressing modes for operand A and)
60 W( four addressing modes)59 W
9504 10458 MT
(for operand B. Every addressing mode works with all instructions. There are 15 different arithmetic)171 W
9504 11744 MT
(instructions. Each)
322 W( instruction contains four bits that allow the arithmetic flags,)
36 W( carry, overflow, zero, and)35 W
9504 13030 MT
(negative, to)
157 W( be selectively updated. Also, each instruction contains four bits that specify whether the)158 W
9504 14316 MT
(result computed by an instruction)
32 W( is stored, based on the values of the arithmetic flags at the beginning of)31 W
9504 15602 MT
(an instruction. Conditional branch and jump)
91 W( instructions are just arithmetic instructions that operate on)92 W
9504 16888 MT
(the program counter.)SH
9504 19460 MT
(The FM9001 is implemented in a netlist that is composed of 85)
51 W( modules that collectively reference 1800)50 W
9504 20746 MT
(primitives of 48 different types. Roughly 28,000 transistors are required in the design.)
41 W( The)
333 W( FM9001 has)42 W
9504 22032 MT
(95 I/O pins, of which 32 are bi-directional. The)
148 W( NDL translation of the verified netlist contains over)147 W
9504 23318 MT
(91,000 characters in)
77 W( 2,215 lines. This NDL specification is used by LSI Logic as a wiring guide for an)78 W
9504 24604 MT
(actual implementation.)SH
9504 27176 MT
(To facilitate post-fabrication testing, the 248)
166 W( internal single-bit latches are connected in a scan chain.)165 W
9504 28462 MT
(Using the test enable and input pins, it is possible to load or read every bit in the chain.)SH
9504 31034 MT
(The stack-based assembly language, Piton, is implemented)
218 W( on top of FM9001. The Piton language)219 W
9504 32320 MT
(provides provides execute-only programs, recursive subroutine call and return, stack based parameter)193 W
9504 33606 MT
(passing, local variables, global variables and arrays, a)
26 W( user-visible stack for intermediate results, the usual)27 W
9504 34892 MT
(instructions for control and resource monitoring, and instructions for)
80 W( handling seven abstract data types:)79 W
9504 36178 MT
(integers, natural numbers,)
SH( bit vectors, Booleans, data addresses, program addresses \050labels\051 and subroutine)1 W
9504 37464 MT
(names. There)
492 W( are 65 different Piton instruction opcodes. Piton is implemented by an Nqthm function)120 W
9504 38750 MT
(which transforms Piton programs and data into binary FM9001 machine code.)SH
9504 41322 MT
(The Micro-Gypsy language is)
117 W( a high-level language based on Gypsy \050which was largely influenced by)118 W
9504 42608 MT
(Pascal\051. Micro-Gypsy)
538 W( provides four data types:)
144 W( Boolean, integer, character, and arrays of these. The)143 W
9504 43894 MT
(Micro-Gypsy statement types are)23 W
/Courier-Bold SF
23149 XM
(IF)SH
/Times-Roman SF
24622 XM
(and)SH
/Courier-Bold SF
26339 XM
(LOOP)SH
/Times-Roman SF
(, together with)24 W
/Courier-Bold SF
34866 XM
(BEGIN-WHEN)SH
/Times-Roman SF
(, and)24 W
/Courier-Bold SF
43108 XM
(SIGNAL)SH
/Times-Roman SF
46982 XM
(for condition)24 W
9504 45180 MT
(handling, and also procedure definition, call and return. Fourteen predefined utilities are provided.)240 W
9504 46466 MT
(Others can be added at the incremental cost)
124 W( of verifying their Piton implementations. Micro-Gypsy is)125 W
9504 47752 MT
(implemented by an Nqthm function that transforms Micro-Gypsy programs and data into Piton.)SH
9504 50324 MT
(The entire short stack effort, i.e., specification and)
47 W( proof of the correctness of Micro-Gypsy on top of the)46 W
9504 51610 MT
(hardware description language, requires about 2,500 Nqthm definitions)
123 W( and the proof of approximately)124 W
9504 52896 MT
(5,500 lemmas. We estimate the size of the formal proof which)
64 W( Nqthm verified to be roughly 15 million)63 W
9504 54182 MT
(inference steps.)SH
8 SS
15724 53837 MT
(2)SH
11 /Times-Bold AF
9504 57079 MT
(1.6-B The)
275 W( Complexity of the Motorola MC68020)SH
10 /Times-Roman AF
9504 59417 MT
(While the stack is relatively deep, the)
145 W( computing engine at the bottom, the FM9001, is simple by the)146 W
9504 60703 MT
(standards of commercial microprocessors.)SH
9504 63275 MT
(Yuan Yu, a graduate student)
86 W( at the University of Texas at Austin, has used the Nqthm system to model)85 W
9504 64561 MT
(about 80% of the user available instruction set of the Motorola MC68020 microprocessor.)
180 W( The)
611 W( user)181 W
10800 50 9504 66656 UL
6 SS
10304 67995 MT
(2)SH
8 SS
10604 68304 MT
(By ``inference step'' we mean)
11 W( the application of such rules of inference as instantiation, modus ponens, substitution of equals for)12 W
9504 69228 MT
(equals, and tautology checking. Because Nqthm does not actually construct a formal proof but)
57 W( \050allegedly\051 verifies that one exists,)56 W
9504 70152 MT
(the size)
21 W( of the verified formal proof is merely estimated here. The estimate is based on figures obtained from an augmented version)22 W
9504 71076 MT
(of Nqthm that counted the number of such steps \050in successful branches of the proof search\051 during a complete run of)
45 W( the FM9001)44 W
9504 72000 MT
(portion of the stack. The number for FM9001 alone is slightly over 6 million.)SH
ES
%%Page: 8 10
61200 79200 BS
0 SI
10 /Times-Roman AF
51700 4286 MT
(8)SH
9504 7886 MT
(visible state consists of 8 data registers,)
74 W( 8 address registers, a 32-bit program counter, an 8-bit condition)73 W
9504 9172 MT
(code register \050which includes condition codes for carry, overflow, zero, negative,)
255 W( and extend\051, and)256 W
9504 10458 MT
(memory. Semantics)
388 W( are formalized for approximately 80 instruction opcodes. Breaking the)
69 W( instructions)68 W
9504 11744 MT
(down into the ten categories of the MC68020 user's manual)
259 W( [18],)
SH( Yu formalizes all 9)
259 W( of the data)260 W
9504 13030 MT
(movement instructions, 27 of the 28)
9 W( integer arithmetic instructions \050)8 W
/Courier-Bold SF
(CMP2)SH
/Times-Roman SF
39515 XM
(is excluded\051, all 9 of the logical)8 W
9504 14316 MT
(operations, all 9 of the shift and rotate instructions, all 4 of the bit manipulation instructions, all 8 of)
63 W( the)64 W
9504 15602 MT
(bit field instructions, none of the binary coded decimal instructions, 11 of the 13 program)
256 W( control)255 W
9504 16888 MT
(instructions \050)157 W
/Courier-Bold SF
(CALLM)SH
/Times-Roman SF
18318 XM
(and)SH
/Courier-Bold SF
20169 XM
(RTM)SH
/Times-Roman SF
22376 XM
(are excluded\051, 5 of the 21 system control instructions, and none of the)157 W
9504 18174 MT
(multiprocessor instructions. The formal specification is an operational model involving about)
24 W( 700 Nqthm)23 W
9504 19460 MT
(function definitions. It occupies about 80 pages.)SH
9504 22032 MT
(Yu has also developed a reusable library of rules about these definitions so)
82 W( that Nqthm can behave as a)83 W
9504 23318 MT
(proof engine for MC68020 machine code programs.)
93 W( The)
434 W( MC68020 library contains approximately 900)92 W
9504 24604 MT
(rules. The)
1032 W( library deals with nonnegative integer arithmetic and modulo arithmetic, alternative)392 W
9504 25890 MT
(interpretations of bit vectors \050e.g., the)
202 W( arithmetic meaning of some logical operations\051, and symbolic)201 W
9504 27176 MT
(memory management \050i.e., what is obtained by reading from a symbolic memory address)
91 W( in a symbolic)92 W
9504 28462 MT
(machine state\051.)SH
9504 31034 MT
(To demonstrate the viability of the)
174 W( approach Yu has produced mechanically checked proofs of many)173 W
9504 32320 MT
(interesting machine)
162 W( code programs. These programs are obtained from high-level language programs)163 W
9504 33606 MT
(written in C or Ada and then compiled with commercially)
96 W( available compilers targetting the MC68020.)95 W
9504 34892 MT
(The Gnu C compiler and the)
178 W( Verdix Ada compiler were used. Among the programs so verified are)179 W
9504 36178 MT
(Hoare's)SH
/Times-Italic SF
12998 XM
(in situ)79 W
/Times-Roman SF
15879 XM
(Quick Sort, binary search, and several C programs from)
79 W( the widely used Berkeley string)78 W
9504 37464 MT
(processing library. See [12] for details.)SH
9504 40036 MT
(To the best of our knowledge, this is the first example of the)175 W
/Times-Italic SF
36165 XM
(post hoc)176 W
/Times-Roman SF
40128 XM
(verification of commericially)176 W
9504 41322 MT
(produced software for a)
273 W( commercially produced microprocessor. We do not recommend)272 W
/Times-Italic SF
48567 XM
(post hoc)272 W
/Times-Roman SF
9504 42608 MT
(verification, but it is sometimes possible.)SH
11 /Times-Bold AF
9504 45505 MT
(1.7 Conclusion: Logic)
275 W( Comes First)SH
10 /Times-Roman AF
9504 47843 MT
(It is no wonder that trouble ensues when we try to impose logic)31 W
/Times-Italic SF
35543 XM
(post facto)31 W
/Times-Roman SF
39772 XM
(via a ``formula generator.'' In)31 W
9504 49129 MT
(such an approach, the computational engine)
15 W( of interest is literally described)14 W
/Times-Italic SF
40102 XM
(informally)SH
/Times-Roman SF
44533 XM
(in the sense that its)14 W
9504 50415 MT
(semantics is not expressed within)
18 W( the logic and is thus not subject to formal reasoning. Attempts to repair)19 W
9504 51701 MT
(this by building other formula generators,)
343 W( formalizing other models of the engine, introduce the)342 W
9504 52987 MT
(``integration'' problem by inviting)
344 W( the suggestion that we ought to be able to reason about the)345 W
9504 54273 MT
(relationships between the two models. This of course is impossible as long as)
25 W( the two models themselves)24 W
9504 55559 MT
(remain informal.)SH
9504 58131 MT
(Logic comes first. Given a logic, one should)
33 W( ``code'' the semantics of the various computational engines)34 W
9504 59417 MT
(in the chosen logic.)
39 W( ``Formula)
327 W( generation'' is merely an artifact of proof and is mechanically realized by)38 W
9504 60703 MT
(whatever theorem prover supports your chosen logic.)SH
9504 63275 MT
(Formula generation programs are just \050sometimes)
90 W( elaborate\051 derived rules of inference about the formal)91 W
9504 64561 MT
(semantics. They)
266 W( allow you to prove certain kinds of theorems about)7 W
/Times-Italic SF
37225 XM
(concretely)SH
/Times-Roman SF
41647 XM
(given programs. They are)7 W
9504 65847 MT
(useful as such derived)
8 W( rules. We consider it a worthy task to formalize a vcg for one of our computational)9 W
9504 67133 MT
(models and verify its correctness, simply)
180 W( to offer the user additional avenues of proof. But formula)179 W
9504 68419 MT
(generators fit into an integrated whole only when their true role is understood. And)
136 W( in the context of)137 W
9504 69705 MT
(system verification, integration is paramount.)SH
ES
%%Page: 9 11
61200 79200 BS
0 SI
10 /Times-Roman AF
51700 4286 MT
(9)SH
12 /Times-Bold AF
9504 8004 MT
(2. Exchanging)
300 W( Data)SH
10 /Times-Italic AF
9504 10472 MT
(2. Methods for exchanging useful data among automated)
135 W( theorem provers, software engineering tools,)134 W
9504 11758 MT
(and other analysis tools.)SH
/Times-Roman SF
9504 14330 MT
(First, we would like to note that to the extent that the)
71 W( various incarnations of Nqthm above are different)72 W
9504 15616 MT
(software engineering tools, we have a perfectly formal method for exchanging data: everything is)285 W
9504 16902 MT
(expressed in the Nqthm logic and is readily available to the different tools.)SH
8 SS
39611 16557 MT
(3)SH
10 SS
9504 19474 MT
(Second, as noted above,)
16 W( we do not believe that useful integration will be achieved via the pasting together)17 W
9504 20760 MT
(of different logics and theorem provers. Roughly speaking, we think)
138 W( every integrated tool set will be)137 W
9504 22046 MT
(based on a single logic and theorem prover.)35 W
8 SS
27190 21701 MT
(4)SH
10 SS
28160 22046 MT
(But this is not to say that the world needs only one)
35 W( logic or)36 W
9504 23332 MT
(theorem prover,)
45 W( much less that we have yet identified even one empirically adequate system. The nature)44 W
9504 24618 MT
(of the logic and its mechanized support depend upon)
57 W( the kinds of computational models needed. This is)58 W
9504 25904 MT
(the subject of today's research.)SH
9504 28476 MT
(Such research requires exchanging data between the advocates of the)
37 W( various logics and theorem provers.)36 W
/Times-Italic SF
9504 29762 MT
(Note that this is different from exchanging data between different parts of an)
SH( implemented system!)1 W
/Times-Roman SF
49340 XM
(We are)1 W
9504 31048 MT
(advocating the need for what)
17 W( might be called)16 W
/Times-Italic SF
27910 XM
(informal data exchange)16 W
/Times-Roman SF
(. In)
282 W( our opinion, such research-level)16 W
9504 32334 MT
(exchange is most easily facilitated by)SH
/Symbol SF
11794 33787 MT
(\267)SH
/Times-Roman SF
12504 XM
(having a clear, self-contained, human-readable)
303 W( description of your logic including)304 W
/Times-Italic SF
48644 XM
(all)SH
/Times-Roman SF
12504 34892 MT
(abbreviation conventions and parsing information,)SH
/Symbol SF
11794 36650 MT
(\267)SH
/Times-Roman SF
12504 XM
(self-contained, human-readable papers in which the formalizations of computational)
35 W( models)34 W
12504 37755 MT
(are presented and explicated in the traditional, journal-level informal style, and)SH
/Symbol SF
11794 39513 MT
(\267)SH
/Times-Roman SF
12504 XM
(self-contained, machine-readable files in which correspond to the published papers.)SH
9504 42085 MT
(Our logic is presented in complete)
337 W( detail in pages 93-141 of)
338 W( [2].)
SH( We)
926 W( currently make available)338 W
9504 43371 MT
(approximately ten megabytes of formal definitions and theorems. Each problem set)
73 W( is documented by a)72 W
9504 44657 MT
(published book, journal article, PhD dissertation, technical report, or extensive comments in the file.)
17 W( This)285 W
9504 45943 MT
(discipline succeeds in fostering valuable collaboration.)SH
9504 48515 MT
(Our problem sets are used world-wide both to benchmark our system and challenge)
164 W( others. Our bit-)163 W
9504 49801 MT
(vector, natural, and integer libraries, for example,)
78 W( are currently being studied by Gerard Huet's group at)79 W
9504 51087 MT
(INRIA \050France\051 with the aim of converting them to)
73 W( useful libraries for their Coq theorem prover for the)72 W
9504 52373 MT
(calculus of constructions. That group has also taken)
213 W( the Nqthm proof script for the Church-Rosser)214 W
10800 50 9504 55568 UL
6 SS
10304 56907 MT
(3)SH
8 SS
10604 57216 MT
(The newest and as yet unreleased version of Nqthm,)
38 W( called Nthm, is in fact a radical departure from Nqthm in that it provides a)39 W
9504 58140 MT
(great deal of support for combining independently generated reusable libraries.)
179 W( Indeed,)
556 W( in Nthm we have replaced the term)178 W
9504 59064 MT
(``library'' by the term ``book'' to suggest more directly the idea that a)
75 W( given development effort may rely on the results in many)76 W
9504 59988 MT
(different books. Two problems typically encountered)
20 W( in trying to combine two books or ``explicated models'' are name clashes and)19 W
9504 60912 MT
(disagreement over strategies encoded in rules. These problems are addressed explicitly in Nthm by scoping features and ``theories.'')SH
6 SS
10304 62451 MT
(4)SH
8 SS
10604 62760 MT
(This sentence is unnecessarily strong)
19 W( but intended provocatively. We actually imagine families of very closely linked logics and)20 W
9504 63684 MT
(various theorem provers that support individual logics within the families. At)
32 W( CLI the Nqthm logic is used both with and without a)31 W
9504 64608 MT
(nonconstructive ``patch'' that adds the power of first-order)
20 W( quantification; we use both the Nqthm theorem prover and its interactive)21 W
9504 65532 MT
(enhancement Pc-Nqthm. But these systems)
12 W( are so closely linked that for all practical purposes \050i.e., except when feeling particularly)11 W
9504 66456 MT
(picky about)
107 W( constructivity\051 we could just always use the extended Nqthm logic and Pc-Nqthm. We also believe that ultimately)108 W
9504 67380 MT
(several different logical)
5 W( systems will be unified by a single formal metalogic. We have already seen this in)
4 W( [19],)
SH( where propositional)4 W
9504 68304 MT
(calculus, Shoenfield's first-order logic, Church's lambda calculus, and Cohen's hereditarily finite)
77 W( set theory Z2 are all formalized)78 W
9504 69228 MT
(with Nqthm's logic)
77 W( as the metalogic. Properties of these formal systems are then derived, including such interesting ones as that)76 W
9504 70152 MT
(every tautology has a proof,)
11 W( the Church-Rosser property of lambda calculus, and Goedel's incompleteness theorem. We believe that)12 W
9504 71076 MT
(eventually such formal, mechanized metalogical embeddings will permit automated reasoning systems to make)
229 W( the kind of)228 W
9504 72000 MT
(intralogical jumps so common in everyday mathematics.)SH
ES
%%Page: 10 12
61200 79200 BS
0 SI
10 /Times-Roman AF
51200 4286 MT
(10)SH
9504 7886 MT
(theorem [10])
SH( and massaged it so that Coq can reproduce the)
1 W( proof. Similarly, Hantoa Zhang and Xin Hua,)SH
9504 9172 MT
(of the University of Iowa, have massaged)
177 W( our Nqthm proof script for the finite version of Ramsey's)178 W
9504 10458 MT
(theorem [20])
SH( into a form suitable for successful processing by the RRL)
231 W( [21].)
SH( These)
711 W( are significant)230 W
9504 11744 MT
(examples of data exchange at the research level.)SH
9504 14316 MT
(In addition,)
1 W( it is easy for us to ``farm out'' the non-inductive parts of our proofs out to a predicate-calculus)2 W
9504 15602 MT
(proof engine. We can easily generate clause)
192 W( sets capturing such logical problems and have shipped)191 W
9504 16888 MT
(hundreds of such clause sets to Argonne over the years so they could experiment with our problems.)SH
9504 19460 MT
(We have also been on the receiving end of such)
SH( scientific exchanges. For example, Bill Young of CLI has)1 W
9504 20746 MT
(taken the EHDM proof of the interactive convergence clock synchronization algorithm by Rushby)
129 W( and)128 W
9504 22032 MT
(von Henke)
17 W( [22])
SH( and converted it to a successfully processed Nqthm proof script)
17 W( [23].)
SH( This)
286 W( script contains)18 W
9504 23318 MT
(200 definitions and theorems \050not counting those in)
330 W( our standard rational arithmetic library\051 and)329 W
9504 24604 MT
(represents another significant example of data exchange.)SH
12 /Times-Bold AF
9504 28288 MT
(3. Exchanging)
300 W( Code)SH
10 /Times-Italic AF
9504 30756 MT
(3. Methods for promoting the interchangeability of component parts of automated reasoning tools.)SH
/Times-Roman SF
9504 33328 MT
(There are)
11 W( three major obstacles in the way of interchanging component parts of theorem provers: different)12 W
9504 34614 MT
(implementation languages, different logics, and the so-called ``open black box'' problem discussed below.)SH
9504 37186 MT
(The world's major automated reasoning systems)
37 W( are written in a wide variety of programming languages.)36 W
9504 38472 MT
(Nqthm and RRL are written in Common Lisp, HOL)
134 W( and Nuprl are written in ML, Larch is written in)135 W
9504 39758 MT
(CLU, OTTER is written in C, and Oyster/Clam is written in Prolog.)
53 W( Even)
354 W( if all these systems supported)52 W
9504 41044 MT
(the same logic, it would not be easy or natural to plug in component modules. Unless we wish)
199 W( to)200 W
9504 42330 MT
(standardize on a single implementation language, we believe)
16 W( that interchangeability of components is best)15 W
9504 43616 MT
(achieved via clearly written descriptions of the algorithms and representations.)SH
9504 46188 MT
(Such methods actually work. Our system is documented so thoroughly in the book)
72 W( [24])
SH( that)
72 W( it has been)73 W
9504 47474 MT
(reprogrammed from scratch in such remote sites)
148 W( as Amherst, Massachusettes and Bejing, China. Our)147 W
9504 48760 MT
(algorithms are at the heart)
119 W( of Alan Bundy's Oyster/Clam project \050Edinburgh, Scotland\051 where they are)120 W
9504 50046 MT
(used to guide the construction of proofs in)
215 W( a Martin Lof-style type theory. Bundy reports that our)214 W
9504 51332 MT
(heuristic algorithms search the space and generate detailed proof plans about ten times faster)
145 W( than the)146 W
9504 52618 MT
(formal proof checker)
182 W( can check them. Our algorithms or methods contributed to the design of such)181 W
9504 53904 MT
(diverse systems as)
106 W( RRL)
107 W( [21],)
SH( NEVER)
107 W( [25],)
SH( and INRIA's Coq.)107 W
/Times-Italic SF
36073 XM
(Clear documentation essentially allows)107 W
9504 55190 MT
(the exchange of components even in the face of vast differences)
138 W( in the underlying logical systems and)137 W
9504 56476 MT
(implementation languages.)SH
/Times-Roman SF
9504 59048 MT
(We also have much experience)
70 W( with adapting components written by others. It has led us to understand)71 W
9504 60334 MT
(what we)
146 W( called the ``open black box'' problem. In)
145 W( [26])
SH( we describe a four-year effort to encorporate)145 W
9504 61620 MT
(linear arithmetic decision procedures into Nqthm. We studied and implemented)
394 W( procedures by)395 W
9504 62906 MT
(Hodes [27],)
SH( Bledsoe)
1 W( [28],)
SH( Shostak)
1 W( [29],)
SH( and Nelson and Oppen)
1 W( [30].)
SH( The)
252 W( primary)
1 W( benefit promised by the)SH
9504 64192 MT
(inclusion of a decision procedure in a general-purpose setting is to relieve the general-purpose)
71 W( device of)72 W
9504 65478 MT
(the need to explore the search space attributable to the)
104 W( decidable fragment. Our study indicates that in)103 W
9504 66764 MT
(order to realize this benefit it is necessary to ``open'' the black-box decision)
79 W( procedure so that it can be)80 W
9504 68050 MT
(used in all)
274 W( the ways the general-purpose device would have used the axioms and theorems to be)273 W
9504 69336 MT
(eliminated. Not)
496 W( only may)
123 W( the general-purpose device invoke the decision procedure in many different)124 W
9504 70622 MT
(ways, but it)
22 W( may be necessary for the decision procedure to communicate with the general-purpose device)21 W
9504 71908 MT
(to cause it to pursue)
43 W( goals required by the procedure. Furthermore, once so integrated, we found that the)44 W
ES
%%Page: 11 13
61200 79200 BS
0 SI
10 /Times-Roman AF
51200 4286 MT
(11)SH
9504 7886 MT
(performance of)
116 W( the whole is not much affected by the speed of the decision procedure! The dominant)115 W
9504 9172 MT
(consideration is the speed with which information flows)
52 W( back and forth between the two components. A)53 W
9504 10458 MT
(component that gains internal efficiency by)
5 W( using intricate representations of the data is often less efficient)4 W
9504 11744 MT
(\050because of the cost of the transformation at the interface\051 in an integrated system than)
56 W( a component that)57 W
9504 13030 MT
(sacrifices speed to work directly on the input)
64 W( representations. Thus, despite our conviction that decision)63 W
9504 14316 MT
(procedures are extremely important to general-purpose theorem proving, much research)
135 W( devoted to the)136 W
9504 15602 MT
(run-time efficiency of stand-alone)
87 W( decision procedures is not just wasted effort but counterproductive to)86 W
9504 16888 MT
(the goals of general-purpose theorem proving.)SH
9504 19460 MT
(More recently, we have)
105 W( studied the integration of a binary decision diagram \050BDD\051 algorithm)
106 W( [31])
SH( into)106 W
9504 20746 MT
(Nqthm. While)
310 W( our work on this topic is still young, the)
30 W( opinions expressed above have been validated by)29 W
9504 22032 MT
(our experiments so far.)SH
9504 24604 MT
(In conclusion, while interchangeability of parts is clearly desirable, it will)
40 W( not be enabled by the adoption)41 W
9504 25890 MT
(of a common programming language and/or a common)
8 W( logical basis. Observe that in our linear arithmetic)7 W
9504 27176 MT
(example above, we never discussed the fact that the formalizations of arithmetic employed by)
32 W( the various)33 W
9504 28462 MT
(decision procedures were different from each other and)
70 W( different from that in Nqthm. These differences)69 W
9504 29748 MT
(are often minor \050when the decision procedure is of interest at all\051.)
108 W( Practical)
468 W( interchangeability of parts)109 W
9504 31034 MT
(must await a better understanding of how)
36 W( theorem provers are structured, how their data is structured and)35 W
9504 32320 MT
(stored, how contextual information is maintained,)
86 W( etc. The field is too young for us to set standards on)87 W
9504 33606 MT
(such issues now.)SH
12 /Times-Bold AF
9504 37290 MT
(4. Interface)
300 W( Logics)SH
10 /Times-Italic AF
9504 39758 MT
(4. Establishing a formal basis for exchanging information)
24 W( among automated reasoning tools and between)23 W
9504 41044 MT
(formal specification processing tools and automated theorem provers.)SH
/Times-Roman SF
9504 43616 MT
(The ``formal basis'' mentioned above has otherwise become known as)
6 W( an ``interface logic.'' In)
7 W( [32],)
SH( Josh)7 W
9504 44902 MT
(Guttman informally calls an interface logic a)51 W
/Times-Italic SF
28052 XM
(lingua franca)51 W
/Times-Roman SF
33821 XM
(for verification \050page 2 of)
51 W( [32]\051.)
SH( However)
352 W( in)51 W
9504 46188 MT
(the introduction of the paper Guttman summarizes the most attractive benefits of an interface logic:)SH
9 SS
11921 47575 MT
(The goal of this report is)
35 W( to advocate the idea of an)36 W
/Times-Italic SF
30898 XM
(interface logic)36 W
/Times-Roman SF
36420 XM
(for verification environments. By this)36 W
11304 48589 MT
(we mean a logic with a syntax that is simple for machines)
89 W( to generate and parse, and that has a standard)88 W
11304 49603 MT
(semantics and a sufficient degree of expressiveness. It is intended to codify logical presuppositions that)
20 W( are)21 W
11304 50617 MT
(common to a considerable number of efforts in specification and verification.)SH
11921 52917 MT
(Our hope is that it will become possible largely to separate the work of developing)
92 W( formula-generators,)91 W
11304 53931 MT
(such as verification-condition generators and specification-language processors, from the effort)
377 W( of)378 W
11304 54945 MT
(developing theorem-proving software.)SH
10 SS
9504 57517 MT
(That hope is well-founded. It is clearly possible to separate the)
53 W( development of formula generators from)52 W
9504 58803 MT
(the development)
83 W( of theorem provers. To the extent that formula generators are an attempt to define the)84 W
9504 60089 MT
(semantics of a computational engine, such work has nothing to do)
209 W( with automatic theorem proving.)208 W
9504 61375 MT
(However, it has everything to do with logic.)SH
9504 63947 MT
(It is possible to develop a formula)
173 W( generator without selecting a theorem prover. However, it is not)174 W
9504 65233 MT
(possible to develop a formula generator)
55 W( without selecting a logic. The process of generating verification)54 W
9504 66519 MT
(conditions \050say\051 requires mapping from programming constructs \050such as the ``)309 W
/Courier-Bold SF
(+)SH
/Times-Roman SF
('' symbol in)
309 W( the)310 W
9504 67805 MT
(programming language\051 to logical symbols \050such as the ``integer addition modulo)
31 W( 2)30 W
8 SS
43313 67460 MT
(32)SH
10 SS
44113 67805 MT
('' function symbol\051.)30 W
9504 69091 MT
(These logical symbols must be defined by axioms. Generally)
272 W( speaking, the particular axioms are)273 W
9504 70377 MT
(intimately connected)
152 W( to the programming language. Modulo addition is pretty common and might be)151 W
9504 71663 MT
(expected to be ``predefined'' in)
19 W( some available logical theory. But other functions, such as ``compute the)20 W
ES
%%Page: 12 14
61200 79200 BS
0 SI
10 /Times-Roman AF
51200 4286 MT
(12)SH
9504 7886 MT
(effective address,'' are unlikely to be predefined.)
114 W( The)
476 W( creation of the axioms is an integral part of the)113 W
9504 9172 MT
(development of the formula generator. Thus, one)
104 W( cannot undertake the creation of a formula generator)105 W
9504 10458 MT
(without having)SH
/Times-Italic SF
15782 XM
(some)SH
/Times-Roman SF
18087 XM
(logic in mind.)SH
9504 13030 MT
(Having chosen a logic, the formula generator developers create a formula generator and a large)
126 W( pot of)125 W
9504 14316 MT
(axioms in)
126 W( their chosen logic. They then enter the theorem proving market and shop for a system that)127 W
9504 15602 MT
(supports their logic. Logic being what it is, they must find an)36 W
/Times-Italic SF
34888 XM
(exact)SH
/Times-Roman SF
37284 XM
(match or else the whole point)
36 W( is lost.)35 W
9504 16888 MT
(But unless they considered the available theorem provers before)
65 W( they started, they probably won't find a)66 W
9504 18174 MT
(suitable one because of their tendency to ``roll their own'' logics.)SH
9504 20746 MT
(Mike Gordon [email message to)50 W
/Courier-Bold SF
22891 XM
(deftpi)SH
/Times-Roman SF
26791 XM
(mailing list on 14 October, 1991])
50 W( proposed what we believe is)49 W
9504 22032 MT
(the best way to ease the pain of the formula generator people: publish)
53 W( a catalog of all the logics that are)54 W
9504 23318 MT
(supported by automated reasoning systems. Gordon's proposal was:)SH
9 SS
11921 24705 MT
(One way to address this)
126 W( need is to provide a catalog of available theorem proving tools. This should)125 W
11304 25719 MT
(include, for example, how to get the tool, \050availability, costs etc\051, details)
126 W( of the logic supported \050formal)127 W
11304 26733 MT
(syntax and semantics\051, infrastructure required \050e.g.)
95 W( X-windows and Common Lisp\051, ease of use, cost and)94 W
11304 27747 MT
(availability of training, example case studies, characterization of which kinds)
61 W( of problems the tool is good)62 W
11304 28761 MT
(for, lists of existing users and other general remarks of interest to potential users. Those of)
60 W( us in the field)59 W
11304 29775 MT
(may know this information anyway, but such a catalog might help others.)SH
11921 32075 MT
(I think the only way to get such a catalog would be to pay someone to compile it.)SH
11921 34375 MT
(My current feeling is that compiling such a catalog should be prior to any)
68 W( attempt to define an interface)69 W
11304 35389 MT
(logic -- and after it is compiled maybe we won't need the interface logic after all!)SH
10 SS
9504 36845 MT
(We would add that the catalog should begin with a dire warning that once)
24 W( a formula generator project has)23 W
9504 38131 MT
(selected a logic they must refrain from ``modifying'' it unless they want)
179 W( to write their own theorem)180 W
9504 39417 MT
(prover.)SH
9504 41989 MT
(An alternative approach is the adoption of an interface logic. We discuss some perils)
44 W( of that approach in)43 W
9504 43275 MT
(more detail in [1].)SH
9504 45847 MT
(We do not believe there is much merit in adopting an)
102 W( ``interface logic.'' Suppose there is an interface)103 W
9504 47133 MT
(logic and all theorem proving groups undertake to translate from a subset)
107 W( of it to their particular logic.)106 W
9504 48419 MT
(That is, given a problem in the)
3 W( interface logic IL suppose one can mechanically determine whether it has a)4 W
9504 49705 MT
(rendering in the logic PL of some prover and what that rendering is.)
87 W( \050Here)
422 W( we are assuming that if the)86 W
9504 50991 MT
(rendering is a theorem in PL)
159 W( then the original formula is a theorem of IL, and we simply ignore the)160 W
9504 52277 MT
(necessary consideration of the axioms and their renderings.\051)
14 W( We)
277 W( suspect that most PLs will accommodate)13 W
9504 53563 MT
(only a fragment of the IL, and that fragment will not be as well managed by the host)
28 W( theorem prover as is)29 W
9504 54849 MT
(necessary to handle large problems. Unless some)
74 W( theorem prover is designed to support the entire logic)73 W
9504 56135 MT
(IL, the formula generator people are likely to end up in the disastrous position of not having the means)
31 W( to)32 W
9504 57421 MT
(prove their formulas.)
55 W( They)
358 W( will nevertheless have to discipline themselves to understand and live within)54 W
9504 58707 MT
(the interface logic. And finally, even when a suitable theorem prover is available, they will have)
19 W( to suffer)20 W
9504 59993 MT
(the inefficiency of seeing two levels of transducers between their)
437 W( problem \050some program or)436 W
9504 61279 MT
(specification\051 and the machinations of the proof engine: their own)
165 W( formula generator followed by the)166 W
9504 62565 MT
(translation from IL to PL. In our experience,)
90 W( such transducers significantly complicate and obscure the)89 W
9504 63851 MT
(problem.)SH
9504 66423 MT
(Given that the formula generator people must educate themselves on a)
169 W( particular logic and discipline)170 W
9504 67709 MT
(themselves to use it, why not simply provide the catalog so they have a choice?)SH
9504 70281 MT
(Turning from Guttman's)
6 W( proposal to the ``)5 W
/Courier-Bold SF
(deftpi)SH
/Times-Roman SF
('' online discussion and the purposes of this workshop,)5 W
9504 71567 MT
(it seems to us that the whole interface logic idea has become a sort of coat tree upon which a host)
42 W( of less)43 W
ES
%%Page: 13 15
61200 79200 BS
0 SI
10 /Times-Roman AF
51200 4286 MT
(13)SH
9504 7886 MT
(considered objectives have been hung \050considered in)
119 W( [1]\051.)
SH( In)
486 W( particular, the whole connection between)118 W
9504 9172 MT
(interface logics and)
24 W( system verification is spurious. Interface logics were an attempt to solve the problem)25 W
9504 10458 MT
(faced by formula generators. System verification is an activity that requires supreme integration)
215 W( of)214 W
9504 11744 MT
(verification components across a spectrum of)
139 W( computational paradigms and layers of abstraction. The)140 W
9504 13030 MT
(juxtaposition of those two ideas \050as in the)
109 W( inclusion of this Item 4 in the Call for Papers\051 suggests that)108 W
9504 14316 MT
(interface logics may let us accomplish that integration. Wrong. If)
95 W( two formula generators are made to)96 W
9504 15602 MT
(output formulas in the same logical language then)
174 W( it)173 W
/Times-Italic SF
32094 XM
(is)SH
/Times-Roman SF
33184 XM
(possible to process their output with a single)173 W
9504 16888 MT
(theorem prover. But)
115 W( that is not ``integration.'' In particular, it does not allow us to relate the models)116 W
9504 18174 MT
(implemented by the formula generators. It does not permit system verification.)SH
9504 20746 MT
(As we have already argued, the formula generation approach to semantics)
247 W( is antithetical to system)246 W
9504 22032 MT
(verification because it splits the semantics into formal and informal parts.)
516 W( No)
1284 W( amount of)517 W
9504 23318 MT
(``harmonization'' of the formalized part will put the two back together to create a)
63 W( formal whole that can)62 W
9504 24604 MT
(be integrated with other levels.)SH
12 /Times-Bold AF
9504 28288 MT
(5. User)
300 W( Interfaces and Interaction Styles)SH
10 /Times-Italic AF
9504 30756 MT
(5. The effectiveness of alternative user interfaces and interaction styles for automated reasoning tools.)SH
/Times-Roman SF
9504 33328 MT
(One factor in Nqthm's success, as already mentioned, is the)
92 W( tradition among Nqthm users to follow the)93 W
9504 34614 MT
(fundamental admonition and formalize their problems. But a)
399 W( number of)398 W
/Times-Italic SF
43053 XM
(engineering decisions)398 W
/Times-Roman SF
9504 35900 MT
(significantly increase the user's ability to get the job done with Nqthm. We discuss these here.)SH
11 /Times-Bold AF
9504 38797 MT
(5.1 The)
275 W( Balance of Expressivity and Proof Power)SH
10 /Times-Roman AF
9504 41135 MT
(Logical power seems to come at the cost of effective proof techniques.)
20 W( When)
291 W( we are formalizing models,)21 W
9504 42421 MT
(we want great expressive power; the urge is to)
10 W( design a rich, elaborate logic. When we are automating \050or)9 W
9504 43707 MT
(even just mechanizing\051 effective proof techniques, the urge is toward simple,)
30 W( even decidable, logics. The)31 W
9504 44993 MT
(designers of automated reasoning systems must understand this tension in order)
287 W( to build effective)286 W
9504 46279 MT
(reasoning tools. Too)
132 W( much expressivity frustrates the serious user because it is so hard to prove even)133 W
9504 47565 MT
(simple utterances. Too little expressivity frustrates the serious user because little of)
210 W( interest can be)209 W
9504 48851 MT
(formalized.)SH
9504 51423 MT
(Throughout Nqthm's 20 year evolution it has constantly been applied, both)
63 W( by its developers and others.)64 W
9504 52709 MT
(We believe this ``applications driven'' methodology is one of the keys to)
223 W( Nqthm's success and we)222 W
9504 53995 MT
(recommend it to the developers of other mechanized logics.)
280 W( For)
811 W( example, Goldschlag's work on)281 W
9504 55281 MT
(Unity [17])
SH( was an)
36 W( important driving force in recent major extensions to Nqthm: the provision of two new)35 W
9504 56567 MT
(derived rules of inference permitting)
278 W( ``definition by constraint'' and ``functional instantiation'' \050an)279 W
9504 57853 MT
(apparently higher)
113 W( order act\051)
112 W( [33])
SH( and the nonconstructive allowance for full first-order quantification in)112 W
9504 59139 MT
(function definitions [34].)SH
9504 61711 MT
(In the case of Nqthm, the tension has created a rather weak logic)
133 W( which is balanced somewhat by the)134 W
9504 62997 MT
(power of its proof techniques.)SH
9504 65569 MT
(The weakness of the logic works in)
137 W( Nqthm's favor for people who stay the course. Work devoted to)136 W
9504 66855 MT
(formalizing a model pays off when Nqthm's heuristics manipulate the model ``naturally.'' Of)
9 W( course, it is)10 W
9504 68141 MT
(not ``natural,'')
173 W( it is just that the system extracts a great deal of strategic information from the user's)172 W
9504 69427 MT
(constructive, recursive definitions. This has two)
57 W( good effects. It ``front loads'' the cost of using Nqthm)58 W
9504 70713 MT
(into the formalization phase, giving users better control over the management of projects that are)
10 W( expected)9 W
9504 71999 MT
(to produce models)3 W
/Times-Italic SF
17151 XM
(and)SH
/Times-Roman SF
18904 XM
(proofs. Secondly,)
257 W( it allows the user to provide strategic guidance while engaged in)4 W
ES
%%Page: 14 16
61200 79200 BS
0 SI
10 /Times-Roman AF
51200 4286 MT
(14)SH
9504 7886 MT
(the creative, high-level activity of modeling.)SH
11 /Times-Bold AF
9504 10783 MT
(5.2 User)
275 W( Guidance: Strategy or Tactics?)SH
10 /Times-Roman AF
9504 13121 MT
(Consider the spectrum from proof checker to fully automatic theorem)
1 W( prover. While many people think of)SH
9504 14407 MT
(Nqthm as a)
47 W( fully automatic tool it is in fact far from it. Nqthm has many interactive features. But while)48 W
9504 15693 MT
(Nqthm can be guided by the user, the)
106 W( guidance is not generally at the tactical level of individual proof)105 W
9504 16979 MT
(steps but rather at the strategic level. The system's behavior is largely determined by)
100 W( the)101 W
/Times-Italic SF
46961 XM
(theorems)SH
/Times-Roman SF
50978 XM
(the)SH
9504 18265 MT
(user has caused it to)
34 W( prove. Thus, the experienced user's attention is largely focused on mathematics: the)33 W
9504 19551 MT
(formal explication of the)
135 W( concepts in the model and their relationships. The system is responsible for)136 W
9504 20837 MT
(applying these theorems and slogging through the enormous detail involved.)SH
9504 23409 MT
(For example, consider our port of)
173 W( the short stack proof from the FM8502 to the fabricated FM9001.)172 W
9504 24695 MT
(Suppose the proof had been done with a proof checker and stored as a series of)
164 W( explicit proof steps.)165 W
9504 25981 MT
(Converting that)
313 W( script to ``replay'' with the FM9001 would have been difficult because the new)312 W
9504 27267 MT
(functionality at the bottom introduced new cases, new argument positions, and new hypotheses into over)58 W
9504 28553 MT
(2,000 theorems or their proofs. Detailed proof steps would have been rendered obsolete.)
22 W( But)
292 W( the original)21 W
9504 29839 MT
(proof was encoded as a series of rules that explicated a strategy for Nqthm to follow. The strategy)
2 W( worked)3 W
9504 31125 MT
(for the new machine and so the port was nearly painless.)SH
9504 33697 MT
(It should be noted that the explicated strategy worked partly because of the)
99 W( experience of the user who)98 W
9504 34983 MT
(designed it. Less experienced users might have described)
5 W( a less powerful strategy and made the port more)6 W
9504 36269 MT
(painful. ``Tactics'')
690 W( as provided, for)
220 W( example, in HOL)
219 W( [35])
SH( offer many of the same advantages and)219 W
9504 37555 MT
(disadvantages.)SH
9504 40127 MT
(The Nqthm proof checker, Pc-Nqthm, provides users direct control over the construction of a proof of)
44 W( an)45 W
9504 41413 MT
(Nqthm theorem.)
11 W( Among)
271 W( the commands is the invocation of Nqthm itself, so that within the proof checker)10 W
9504 42699 MT
(one can direct some proofs at a low level or with tactics, and let the system handle others with)
28 W( the rules it)29 W
9504 43985 MT
(has been ``taught.'' A common use of the proof checker is to explore)
51 W( the search space of a problem and)50 W
9504 45271 MT
(find useful strategies for proving theorems. These strategies are then codified as)
206 W( rules for Nqthm's)207 W
9504 46557 MT
(automatic use. Sometimes, as)
140 W( in the Piton proof, scripts are produced that do not appeal to the proof)139 W
9504 47843 MT
(checker at all, even though its use was helpful in the formalization and discovery processes.)SH
11 /Times-Bold AF
9504 50740 MT
(5.3 Fully)
275 W( Supported Syntax)SH
10 /Times-Roman AF
9504 53078 MT
(The syntax of Nqthm's)
74 W( logic is fully supported by many text editors, window systems, and all Common)75 W
9504 54364 MT
(Lisp programming environments. Furthermore, the formulas seen when)
106 W( you look inside the system \050as)105 W
9504 55650 MT
(with various)
36 W( lemma trace and break packages, to see what the system is doing\051 is suitable for input to the)37 W
9504 56936 MT
(system; indeed, except for)
51 W( some abbreviations commonly used when formulas are typed, the internal and)50 W
9504 58222 MT
(external representation is identical. The lack of barriers between)
28 W( the user and system contributes much to)29 W
9504 59508 MT
(the ease of use.)SH
9504 62080 MT
(While Nqthm formulas often look large, they are usually created)
1 W( with a few keystrokes from text that is on)SH
9504 63366 MT
(the screen. A typical action by the user is to realize \050by observing a)
104 W( failing proof\051 that Nqthm doesn't)105 W
9504 64652 MT
(``know'' a certain fact. That fact)
70 W( is then expressed with a series of keystrokes that grab things from the)69 W
9504 65938 MT
(screen and deposit them into the emerging formula: ``This \050)32 W
/Times-Italic SF
(click)SH
/Times-Roman SF
(\051)SH
/Courier-Bold SF
36208 XM
(AND)SH
/Times-Roman SF
38290 XM
(this \050)32 W
/Times-Italic SF
(click)SH
/Times-Roman SF
(\051)SH
/Courier-Bold SF
42853 XM
(IMPLY)SH
/Times-Roman SF
46135 XM
(that this \050)33 W
/Times-Italic SF
(click)SH
/Times-Roman SF
(\051)SH
9504 67224 MT
(is)SH
/Courier-Bold SF
10551 XM
(EQUAL)SH
/Times-Roman SF
13931 XM
(to this \050)130 W
/Times-Italic SF
(click)SH
/Times-Roman SF
(\051.'' The)
510 W( size of such a formula is independent of the time it takes to create it,)130 W
9504 68510 MT
(thanks largely to the support)SH
/Times-Italic SF
21142 XM
(other systems)SH
/Times-Roman SF
26808 XM
(provide for ``our'' syntax.)SH
ES
%%Page: 15 17
61200 79200 BS
0 SI
10 /Times-Roman AF
51200 4286 MT
(15)SH
11 /Times-Bold AF
9504 7937 MT
(5.4 Powerful)
275 W( Command Environment)SH
10 /Times-Roman AF
9504 10275 MT
(Nqthm's command language is Common Lisp. Thus, many users have developed their)
161 W( own personal)162 W
9504 11561 MT
(commands. The)
428 W( verification environment for)
89 W( our formal hardware description language includes a Lisp)88 W
9504 12847 MT
(command that means)
155 W( ``generate the standard recognizer definition and decomposition lemmas for this)156 W
9504 14133 MT
(module.'' The)
504 W( Piton environment includes the command)
127 W( ``disable all rules except function definitions)126 W
9504 15419 MT
(and the primitives.'')SH
11 /Times-Bold AF
9504 18316 MT
(5.5 Effective)
275 W( Interaction Style)SH
10 /Times-Roman AF
9504 20654 MT
(We have developed a style of interacting with Nqthm that has been explained at length in)
76 W( [2].)
SH( The)
403 W( first)77 W
9504 21940 MT
(rule is that you should)
90 W( have a good proof sketch in mind before you present a formula to Nqthm. This)89 W
9504 23226 MT
(forces you to develop the basic lemma)
203 W( decomposition and proof structure. The second rule is that,)204 W
9504 24512 MT
(tactically speaking, you should ``let the theorem)
45 W( prover have its head but keep it on a short leash.'' That)44 W
9504 25798 MT
(is, you should not try overly hard to direct the system.)
108 W( If)
468 W( you begin to fight the system, by constantly)109 W
9504 27084 MT
(giving it tactical advice, you probably have not adequately explicated a strategy)
12 W( for handling the concepts.)11 W
9504 28370 MT
(Once you begin to fight it, you must fight)
39 W( it forever;)40 W
/Times-Italic SF
31046 XM
(its ability to tolerate detail and keep slogging works)40 W
9504 29656 MT
(against you)104 W
/Times-Roman SF
14600 XM
(because it keeps throwing out problems for you to solve. It is thus better to read its proof)103 W
9504 30942 MT
(attempts as it goes, stop it as soon)
34 W( as it has gotten off the ``right'' path, and explain a strategy by proving)35 W
9504 32228 MT
(rules. This)
480 W( harnesses its tolerance for detail)
115 W( to work in your favor. In the end, input proof scripts are)114 W
9504 33514 MT
(collaborative efforts between the user and the system.)SH
12 /Times-Bold AF
9504 37198 MT
(6. Significant)
300 W( System Verification Applications)SH
10 /Times-Italic AF
9504 39666 MT
(6. Significant applications of automated reasoning technology to system development.)SH
/Times-Roman SF
9504 42238 MT
(A characteristic difference between ``system verification'' on)
68 W( the one hand and ``hardware verification'')69 W
9504 43524 MT
(or ``program verification'')
142 W( on the other is one of scale: systems, in our usage, are composed of many)141 W
9504 44810 MT
(component hardware and/or software modules.)
139 W( Another)
529 W( characteristic of systems is that their analysis)140 W
9504 46096 MT
(involves multiple layers)
72 W( of abstraction. These layers often include general purpose computing machines)71 W
9504 47382 MT
(or languages. In this section we simply name some significant applications of Nqthm in system)291 W
9504 48668 MT
(development.)SH
9504 51240 MT
(Our first example is an unusual one: We assert that the formal metamathematical work)
65 W( done by Shankar)64 W
9504 52526 MT
(in [19])
SH( is an excellent example of system)
236 W( verification. The work involves mind-boggling levels of)237 W
9504 53812 MT
(abstraction and several equivalent computational models. In the work,)
75 W( Shankar uses Nqthm's logic as a)74 W
9504 55098 MT
(metalanguage to formalize)
389 W( propositional calculus, Shoenfield's first-order logic, Church's lambda)390 W
9504 56384 MT
(calculus, and Cohen's hereditarily finite set theory Z2. He then proceeds to construct mechanically)209 W
9504 57670 MT
(checked proofs of such important properties of these)
26 W( systems as the metatheorem that every tautology has)27 W
9504 58956 MT
(a proof, the Church-Rosser property of lambda calculus, and Goedel's incompleteness theorem.)SH
9504 61528 MT
(We have already offered the two)
16 W( CLI short stacks as significant applications. But even the)15 W
/Times-Italic SF
46325 XM
(components)SH
/Times-Roman SF
51367 XM
(of)SH
9504 62814 MT
(the stacks qualify as interesting)SH
/Times-Italic SF
22308 XM
(systems)SH
/Times-Roman SF
(:)SH
/Symbol SF
11794 64267 MT
(\267)SH
/Times-Roman SF
12504 XM
(the verification of)
85 W( the gate level design of FM9001 involves 85 modules whose composite)86 W
12504 65372 MT
(behavior implements a computing machine best described via four successive layers)
218 W( of)217 W
12504 66477 MT
(abstraction \050user, two-valued logic, four-valued logic, and netlist\051;)SH
/Symbol SF
11794 68235 MT
(\267)SH
/Times-Roman SF
12504 XM
(the Piton assembler/linker involves hundreds)
358 W( of functions implementing a transducer)359 W
12504 69340 MT
(described in four successive)
199 W( layers \050user, resource model, relocatable symbolic machine)198 W
12504 70445 MT
(code, and absolute binary\051.)SH
ES
%%Page: 16 18
61200 79200 BS
0 SI
10 /Times-Roman AF
51200 4286 MT
(16)SH
9504 7886 MT
(We offer Yu's MC68020 work [12] as a significant example.)SH
9504 10458 MT
(We offer the work William R. Bevier, of)
132 W( CLI, in which a ``separation kernel'' implemented in binary)133 W
9504 11744 MT
(machine code on a uniprocessor was shown to provide multitasking and interprocess communication)
69 W( via)68 W
9504 13030 MT
(message buffers [4].)SH
9504 15602 MT
(Finally, we offer the)
16 W( work of David M. Goldschalg, formerly of CLI, who used Nqthm to formalize Misra)17 W
9504 16888 MT
(and Chandy's Unity system for concurrent programming)
110 W( [17].)
SH( He)
470 W( then developed a reusable)
110 W( library of)109 W
9504 18174 MT
(proof rules, reproducing those)
314 W( in Misra and Chandy's book)
315 W( [36],)
SH( causing Nqthm to ``become'' a)315 W
9504 19460 MT
(verification engine for Unity.)
88 W( He)
424 W( has demonstrated the utility of this proof environment by proving the)87 W
9504 20746 MT
(correctness of several Unity programs,)
21 W( including solutions to the mutual exclusion problem, the minimum)22 W
9504 22032 MT
(node value in a tree, dining philosophers, and a n-bit delay insensitve FIFO queue.)SH
12 /Times-Bold AF
9504 25716 MT
(7. Verification)
300 W( as an Engineering Exercise)SH
10 /Times-Roman AF
9504 28186 MT
(It is our opinion that the great logicians, e.g., Goedel and von Neumann, did a ``good)
124 W( enough'' job in)123 W
9504 29472 MT
(inventing logic and foundations for mathematics \050set theory,)
14 W( recursive functions\051. This received logic and)15 W
9504 30758 MT
(foundations is suitable for stating and checking, mechanically, any part of mathematics at a cost not more)30 W
9504 32044 MT
(that an order of magnitude greater than the time it takes to write proofs down at the detail of)
246 W( an)247 W
9504 33330 MT
(undergraduate math textbook. \050This experience is)
44 W( confirmed by numerous other proof checking systems,)43 W
9504 34616 MT
(not just Nqthm.\051 Computing is just a rather tiny and relatively easy part of mathematics.)SH
9504 37188 MT
(We believe that those who have for the last 30)
88 W( years been ``improving'' the logic or the foundations of)89 W
9504 38474 MT
(computing are fooling themselves if they think that)
41 W( they are easing the task of mechanically checking the)40 W
9504 39760 MT
(correctness of programs. Yet it seems to us that a disproportionately large segment of the)
64 W( community is)65 W
9504 41046 MT
(focusing on)
63 W( this misguided enterprise. We believe this is due to the desire to publish papers suitable for)62 W
9504 42332 MT
(obtaining academic fame and promotion. In our opinion, the building and use of verification systems is)75 W
9504 43618 MT
(largely an)49 W
/Times-Italic SF
13823 XM
(engineering)SH
/Times-Roman SF
18899 XM
(enterprise, the key scientific breatkthroughs)
49 W( for which were made many years ago)48 W
9504 44904 MT
(by people like Frege, Skolem, Church, Goedel, Turing, von Neumann, and McCarthy.)SH
9504 47476 MT
(As noted above, Nqthm's logic is very weak.)44 W
8 SS
27837 47131 MT
(5)SH
10 SS
28825 47476 MT
(We are personally amazed at how far you can)
44 W( go towards)43 W
9504 48762 MT
(systems verification with a few discrete data structures and a)
68 W( little recursion. We cite the success of the)69 W
9504 50048 MT
(Nqthm project as)
116 W( evidence that the need for some new, powerful, universal logic is not the bottleneck.)115 W
9504 51334 MT
(The bottleneck)
18 W( is getting people to do the hard work of formalizing and explicating computational models)19 W
9504 52620 MT
(with formal reasoning tools.)SH
9504 55192 MT
(Our belief that this approach)
260 W( can be ``scaled'' into industrial application is based on the fact that)259 W
9504 56478 MT
(explicated computational models and shared, reusable theories make system verification easier. As)
69 W( time)70 W
9504 57764 MT
(goes on, less work is)
329 W( involved in creating the models because so many components are readily)328 W
9504 59050 MT
(available. [38, 39, 40])
SH( Less)
294 W( work)
22 W( is involved in proving new theorems because the strategic work done to)23 W
9504 60336 MT
(prove old ones is often directly applicable. This is especially)
355 W( true in the context of ``minor'')354 W
9504 61622 MT
(modifications to previously verified components. Finally, the)
90 W( nature of the enterprise)
100 91 WX(\320)
100 MX(which requires,)91 W
9504 62908 MT
(encourages and)147 W
/Times-Italic SF
16240 XM
(most importantly)147 W
/Times-Roman SF
23590 XM
(rewards the explicit specification of clean)
147 W( interfaces between system)146 W
9504 64194 MT
(components)
100 MX(\320)
100 MX(permits system)
92 W( verification to be carried on in a concurrent fashion between independent)93 W
9504 65480 MT
(groups which may share a)
119 W( few common models and theories but are otherwise free to adopt their own)118 W
9504 66766 MT
(most productive strategies. The cost of system verification will drop)
202 W( substantially when there are a)203 W
10800 50 9504 69428 UL
6 SS
10304 70767 MT
(5)SH
8 SS
10604 71076 MT
(It is obtained roughly by throwing out the quantifiers from first order predicate)
14 W( calculus with equality and induction and adding a)15 W
9504 72000 MT
(principle of recursive definition based on Shoenfield's [37].)SH
ES
%%Page: 17 19
61200 79200 BS
0 SI
10 /Times-Roman AF
51200 4286 MT
(17)SH
9504 7886 MT
(number of verified systems and computational models upon which to build.)SH
/Times-Italic SF
9504 10458 MT
(The biggest obstacle to the successful application of verification technology to commercial systems is)
46 W( the)45 W
9504 11744 MT
(lack of money and trained technicians.)SH
/Times-Roman SF
9504 14316 MT
(The key to the industrialization of formal verification is cost effectiveness. It would be)
2 W( useful, we believe,)3 W
9504 15602 MT
(for sponsors to attempt to quantify the cost of verification today, as a benchmark against which progress)63 W
9504 16888 MT
(can be measured.)SH
9504 19460 MT
(But cost effectiveness requires)
248 W( assigning dollar values to expected benefits and these are harder to)249 W
9504 20746 MT
(evaluate. What)
610 W( is the cost to the U.S. economy)
180 W( of unreliable software? Because of the ubiquity of)179 W
9504 22032 MT
(software, this is an exceedingly)
65 W( difficult question to answer. Clearly one should consider the cost to the)66 W
9504 23318 MT
(manufacturer of fixing bugs, recalling products, etc. But one must also consider the cost)
97 W( of down time)96 W
9504 24604 MT
(and recalls to)
114 W( customers and their industries. How much productivity is lost due to faulty applications)115 W
9504 25890 MT
(software? What)
547 W( is the cost of protecting one's business against such losses \050e.g., via redundant, 19th)148 W
9504 27176 MT
(century backup accounting, filing and inventory systems as well as)
152 W( excessive investment in electronic)153 W
9504 28462 MT
(spares, maintenance, etc.\051? How much money is)
32 W( lost or stolen due to software flaws? How much money)31 W
9504 29748 MT
(is lost simply by delays caused by unreliability or redundancy? What)
162 W( is the value of data stolen via)163 W
9504 31034 MT
(software flaws? What)
48 W( is cost of lost sales opportunities due to chronic poor reliability? What is the cost)47 W
9504 32320 MT
(of a life lost to a software error? What happens to the U.S.)
82 W( if all digital computers stopped running for)83 W
9504 33606 MT
(just one particular hour? We believe that)
37 W( sponsors should undertake a study to answer these questions so)36 W
9504 34892 MT
(that it is possible to answer the larger one, ``Is verification cost-effective?'')SH
9504 37464 MT
(Finally, in our opinion, the sponsors of verification research ought to)
62 W( hold a workshop to figure out how)63 W
9504 38750 MT
(much it might cost to,)
52 W( say, generate a mechanically verified Mach, and then decide whether they want to)51 W
9504 40036 MT
(pay that much for one. If so, they ought to organize a suitably funded effort.)SH
12 /Times-Bold AF
9504 43720 MT
(8. Acknowledgements)300 W
10 /Times-Roman AF
9504 46190 MT
(This paper could not have been written \050except as)
10 W( an unconvincing theoretical exercise\051 were it not for the)11 W
9504 47476 MT
(work of)
17 W( our colleagues. We would especially like to acknowledge Bill Bevier, Bob Boyer, Bishop Brock,)16 W
9504 48762 MT
(Art Flatau, David Goldschlag, Warren Hunt, Bill Schelter, Natarajan Shankar,)
58 W( Ann Siebert, Larry Smith,)59 W
9504 50048 MT
(Mike Smith, David Russinoff, Matt Wilding,)
14 W( Bill Young, and Yuan Yu for their faith in this approach and)13 W
9504 51334 MT
(their hard work to)
201 W( demonstrate its viability. The opinions expressed herein are strictly those of the)202 W
9504 52620 MT
(authors.)SH
ES
%%Page: 18 20
61200 79200 BS
0 SI
10 /Times-Roman AF
51200 4286 MT
(18)SH
13 /Times-Bold AF
27820 8071 MT
(References)SH
10 /Times-Roman AF
9504 10444 MT
(1.)SH
12504 XM
(M. Kaufmann and J Strother)
104 W( Moore, ``Should We Begin a Standardization Process for Interface)103 W
12504 11549 MT
(Logics?'', Tech. report CLI Technical Report 72,)
SH( Computational Logic, Inc., 1717 W. Sixth Street,)1 W
12504 12654 MT
(Suite 290, Austin, TX 78703, January 1992.)SH
9504 14445 MT
(2.)SH
12504 XM
(R. S. Boyer and J S. Moore,)SH
/Times-Italic SF
23976 XM
(A Computational Logic Handbook,)SH
/Times-Roman SF
38282 XM
(Academic Press, New York, 1988.)SH
9504 16236 MT
(3.)SH
12504 XM
(Matt Kaufmann, ``A User's Manual for)
34 W( an Interactive Enhancement to the Boyer-Moore Theorem)33 W
12504 17341 MT
(Prover'', Technical Report 19, Computational Logic, Inc., May 1988.)SH
9504 19132 MT
(4.)SH
12504 XM
(W.R. Bevier, W.A. Hunt, J S. Moore, and W.D. Young, ``Special Issue on)
50 W( System Verification'',)51 W
/Times-Italic SF
12504 20237 MT
(Journal of Automated Reasoning)SH
/Times-Roman SF
(, Vol. 5, No. 4, 1989, pp. 409-530.)SH
9504 22028 MT
(5.)SH
12504 XM
(J S. Moore, ``Piton: A Verified Assembly Level)
174 W( Language'', Tech. report 22, Computational)173 W
12504 23133 MT
(Logic, Inc., 1717 West Sixth Street, Suite 290 Austin, TX 78703, 1988.)SH
9504 24924 MT
(6.)SH
12504 XM
(J S. Moore, ``Mechanically Verified Hardware Implementing an 8-Bit)
243 W( Parallel IO Byzantine)244 W
12504 26029 MT
(Agreement Processor'', Tech.)
310 W( report Technical Report 69, Computational Logic, Inc., 1717)309 W
12504 27134 MT
(W. Sixth Street, Suite 290, Austin, TX 78703, August 1991.)SH
9504 28925 MT
(7.)SH
12504 XM
(Warren A. Hunt, Jr. and Bishop Brock , ``A Formal HDL and its use in the FM9001)
2 W( Verification'',)3 W
/Times-Italic SF
12504 30030 MT
(Proceedings of the Royal Society)SH
/Times-Roman SF
(, 1992, to appear April 1992)SH
9504 31821 MT
(8.)SH
12504 XM
(J S.)
168 W( Moore, ``A Formal Model of Asynchronous Communication and Its Use in Mechanically)167 W
12504 32926 MT
(Verifying a Biphase Mark)
255 W( Protocol'', Tech. report CLI Technical Report 68, Computational)256 W
12504 34031 MT
(Logic, Inc., 1717 W. Sixth Street, Suite 290, Austin, TX 78703, August 1991.)SH
9504 35822 MT
(9.)SH
12504 XM
(R. S. Boyer and J S.)
55 W( Moore, ``A Mechanical Proof of the Turing Completeness of Pure Lisp'', in)54 W
/Times-Italic SF
12504 36927 MT
(Automated Theorem Proving:)
34 W( After)
319 W( 25 Years,)35 W
/Times-Roman SF
31467 XM
(W.W. Bledsoe and D.W. Loveland, eds., American)35 W
12504 38032 MT
(Mathematical Society, Providence, R.I., 1984, pp. 133-167.)SH
9504 39823 MT
(10.)SH
12504 XM
(N. Shankar, ``Towards Mechanical Metamathematics'',)65 W
/Times-Italic SF
35434 XM
(Journal of Automated)
65 W( Reasoning)64 W
/Times-Roman SF
(, Vol. 1,)64 W
12504 40928 MT
(No. 1, 1985.)SH
9504 42719 MT
(11.)SH
12504 XM
(W.A. Hunt, ``FM8501:)
51 W( A)
354 W( Verified Microprocessor'', PhD Thesis, University of Texas at Austin,)52 W
12504 43824 MT
(December 1985, Also available through Computational Logic, Inc., Suite 290,)
121 W( 1717 West Sixth)120 W
12504 44929 MT
(Street, Austin, TX 78703.)SH
9504 46720 MT
(12.)SH
12504 XM
(R.S. Boyer and Y. Yu, ``Automated Correctness)
312 W( Proofs of Machine Code Programs for a)313 W
12504 47825 MT
(Commercial Microprocessor'', Tech. report TR-91-33, Computer)
5 W( Sciences Department, University)4 W
12504 48930 MT
(of Texas, Austin, November 1991.)SH
9504 50721 MT
(13.)SH
12504 XM
(W. Young, ``A Verified Code-Generator for)
10 W( a Subset of Gypsy'', PhD Thesis, University of Texas)11 W
12504 51826 MT
(at Austin, 1988, Also available through)
129 W( Computational Logic, Inc., Suite 290, 1717 West Sixth)128 W
12504 52931 MT
(Street, Austin, TX 78703.)SH
9504 54722 MT
(14.)SH
12504 XM
(Donald I. Good, Ann E. Siebert, William D. Young, ``Middle Gypsy 2.05 Definition'',)
182 W( Tech.)183 W
12504 55827 MT
(report CLI Technical Report 59, Computational Logic, Inc., 1717 W. Sixth)
195 W( Street, Suite 290,)194 W
12504 56932 MT
(Austin, TX 78703, June 1990.)SH
9504 58723 MT
(15.)SH
12504 XM
(Michael K. Smith, Dan Craigen,)
132 W( and Mark Saaltink, ``The nanoAVA Definition'', Tech. report)133 W
12504 59828 MT
(CLI Technical Report 21, Computational Logic, Inc., 1717 W. Sixth Street, Suite 290, Austin, TX)30 W
12504 60933 MT
(78703, May 1988.)SH
9504 62724 MT
(16.)SH
12504 XM
(W. Bevier, ``A Verified Operating System Kernel'', PhD Thesis, University of Texas at)
101 W( Austin,)102 W
12504 63829 MT
(1987, Also available through Computational Logic, Inc., Suite 290, 1717 West Sixth)
248 W( Street,)247 W
12504 64934 MT
(Austin, TX 78703.)SH
9504 66725 MT
(17.)SH
12504 XM
(D.M. Goldschlag, ``Mechanizing Unity'', in)96 W
/Times-Italic SF
31009 XM
(Programming Concepts)
96 W( and Methods,)97 W
/Times-Roman SF
46923 XM
(M. Broy and)97 W
12504 67830 MT
(C. B. Jones, eds., North Holland, Amsterdam, 1990.)SH
9504 69621 MT
(18.)SH
12504 XM
(Motorola, Inc.,)SH
/Times-Italic SF
18753 XM
(MC68020 32-bit Microprocessor User's Manual,)SH
/Times-Roman SF
38807 XM
(1989.)SH
9504 71412 MT
(19.)SH
12504 XM
(N. Shankar, ``Proof Checking Metamathematics'', PhD Thesis, University of Texas at)
180 W( Austin,)179 W
ES
%%Page: 19 21
61200 79200 BS
0 SI
10 /Times-Roman AF
51200 4286 MT
(19)SH
12504 7886 MT
(1986, Also)
247 W( available through Computational Logic, Inc., Suite 290, 1717 West Sixth Street,)248 W
12504 8991 MT
(Austin, TX 78703.)SH
9504 10782 MT
(20.)SH
12504 XM
(Kaufmann, Matt J. and David Basin, ``The)
191 W( Boyer-Moore Prover and Nuprl: An Experimental)190 W
12504 11887 MT
(Comparison'', Proceedings of Workshop for)
380 W( Basic Research Action, Logical Frameworks,)381 W
12504 12992 MT
(Antibes, France. Also published as CLI Technical Report 58)SH
9504 14783 MT
(21.)SH
12504 XM
(D. Kapur and H. Zhang, ``RRL: A Rewrite Rule Laboratory -- A User's Manual'', Tech.)
65 W( report,)64 W
12504 15888 MT
(General Electric Research and Development Center, Schenectady, N.Y., June 1987.)SH
9504 17679 MT
(22.)SH
12504 XM
(J. Rushby and F. von Henke, ``Formal Verification of the Interactive Convergence Clock)334 W
12504 18784 MT
(Synchronization Algorithm using EHDM'',)
273 W( Tech. report, Computer Science Laboratory, SRI)272 W
12504 19889 MT
(International, Menlo Park, CA 94025, January 1989, Draft)SH
9504 21680 MT
(23.)SH
12504 XM
(W.D. Young, ``Verifying)
SH( the Interactive Convergence Clock Synchronization Algorithm Using the)1 W
12504 22785 MT
(Boyer-Moore Theorem Prover)
138 W( '', Internal Note 199, Computational Logic, Inc., 1717 W. Sixth)137 W
12504 23890 MT
(Street, Suite 290, Austin, TX 78703, January 1991.)SH
9504 25681 MT
(24.)SH
12504 XM
(R. S. Boyer and J S. Moore,)SH
/Times-Italic SF
23976 XM
(A Computational Logic,)SH
/Times-Roman SF
33866 XM
(Academic Press, New York, 1979.)SH
9504 27472 MT
(25.)SH
12504 XM
(B. Pase and S. Kromodimoeljo,)
96 W( ``m-NEVER User's Manual'', Tech. report TR-87-5420-13, I.P.)97 W
12504 28577 MT
(Sharpe Associates Ltd., 265 Carling Ave., Ottawa Canada, November 1987.)SH
9504 30368 MT
(26.)SH
12504 XM
(R. S. Boyer and)
39 W( J S. Moore, ``Integrating Decision Procedures into Heuristic Theorem Provers: A)38 W
12504 31473 MT
(Case Study with Linear Arithmetic'',)
67 W( in)68 W
/Times-Italic SF
29101 XM
(Machine Intelligence 11,)68 W
/Times-Roman SF
39525 XM
(Oxford University Press, 1988,)68 W
12504 32578 MT
(Also available through Computational Logic, Inc., Suite 290, 1717 West Sixth)
56 W( Street, Austin, TX)55 W
12504 33683 MT
(78703.)SH
9504 35474 MT
(27.)SH
12504 XM
(L. Hodes, ``Solving)
40 W( Problems by Formula Manipulation'',)41 W
/Times-Italic SF
36455 XM
(Proc. Second Inter. Joint Conf. on Art.)41 W
12504 36579 MT
(Intell.)SH
/Times-Roman SF
(, The British Computer Society, 1971, pp. 553-559.)SH
9504 38370 MT
(28.)SH
12504 XM
(W. W. Bledsoe, ``A New Method for Proving Certain Presburger Formulas'',)135 W
/Times-Italic SF
45289 XM
(Advance Papers,)135 W
12504 39475 MT
(Fourth Int. Joint Conf. on Art. Intell.)SH
/Times-Roman SF
(, Tbilisi, Georgia, U.S.S.R., September 1975, pp. 15-20.)SH
9504 41266 MT
(29.)SH
12504 XM
(R. Shostak, ``On the SUP-INF Method)
113 W( for Provign Presburger Formulas'',)114 W
/Times-Italic SF
43831 XM
(JACM)SH
/Times-Roman SF
(, Vol. 24, No.)114 W
12504 42371 MT
(4, 1977, pp. 529-543.)SH
9504 44162 MT
(30.)SH
12504 XM
(G. Nelson and D.)
322 W( C. Oppen, ``Simplification by Cooperating Decision Procedures'',)321 W
/Times-Italic SF
50089 XM
(ACM)SH
12504 45267 MT
(Transactions of Programming Languages)SH
/Times-Roman SF
(, Vol. 1, No. 2, 1979, pp. 245-257.)SH
9504 47058 MT
(31.)SH
12504 XM
(Randal E. Bryant, ``Graph-Based Algorithms for Boolean)
417 W( Function Manipulation'',)418 W
/Times-Italic SF
50034 XM
(IEEE)SH
12504 48163 MT
(Transactions on Computers)SH
/Times-Roman SF
(, Vol. C-35, No. 8, August 1986, pp. 677--691.)SH
9504 49954 MT
(32.)SH
12504 XM
(Joshua D. Guttman,)
123 W( ``A Proposed Interface Logic for Verification Environments'', Tech. report)122 W
12504 51059 MT
(M91-19, The MITRE Corporation, March 1991.)SH
9504 52850 MT
(33.)SH
12504 XM
(R.S. Boyer, D. Goldschlag, M. Kaufmann, J S. Moore,)
126 W( ``Functional Instantiation in First Order)127 W
12504 53955 MT
(Logic'', in)67 W
/Times-Italic SF
17165 XM
(Artificial Intelligence and Mathematical Theory)
67 W( of Computation: Papers in Honor of)66 W
12504 55060 MT
(John McCarthy,)SH
/Times-Roman SF
19253 XM
(V. Lifschitz, ed., Academic Press, 1991, pp. 7-26.)SH
9504 56851 MT
(34.)SH
12504 XM
(Matt Kaufmann, ``An Extension of the Boyer-Moore)
225 W( Theorem Prover to Support First-Order)226 W
12504 57956 MT
(Quantification'', Tech.)
20 W( report CLI Technical Report 43, Computational Logic, Inc., 1717 W. Sixth)19 W
12504 59061 MT
(Street, Suite 290, Austin, TX 78703, May 1989, To appear in J. of Automated Reasoning)SH
9504 60852 MT
(35.)SH
12504 XM
(M. Gordon, ``HOL: A Proof Generating System for Higher-Order Logic'', Tech. report)
223 W( 103,)224 W
12504 61957 MT
(University of Cambridge, Computer Laboratory, 1987.)SH
9504 63748 MT
(36.)SH
12504 XM
(K.M. Chandy and J.)
383 W( Misra,)382 W
/Times-Italic SF
25555 XM
(Parallel Program Design: A Foundation,)382 W
/Times-Roman SF
44930 XM
(Addison Wesley,)382 W
12504 64853 MT
(Massachusetts, 1988.)SH
9504 66644 MT
(37.)SH
12504 XM
(J. R. Shoenfield,)SH
/Times-Italic SF
19393 XM
(Mathematical Logic,)SH
/Times-Roman SF
27976 XM
(Addison-Wesley, Reading, Ma., 1967.)SH
9504 68435 MT
(38.)SH
12504 XM
(Bill Bevier, ``A Library for Hardware)
35 W( Verification'', Internal Note 57, Computational Logic, Inc.,)36 W
12504 69540 MT
(1717 W. Sixth Street, Suite 290, Austin, TX 78703, June 1988.)SH
9504 71331 MT
(39.)SH
12504 XM
(Matt Kaufmann, ``An Integer Library for)
163 W( NQTHM'', Internal Note 182, Computational Logic,)162 W
ES
%%Page: 20 22
61200 79200 BS
0 SI
10 /Times-Roman AF
51200 4286 MT
(20)SH
12504 7886 MT
(Inc., 1717 W. Sixth Street, Suite 290, Austin, TX 78703, 1990.)SH
9504 9677 MT
(40.)SH
12504 XM
(Matthew Wilding, ``Events for a Reproof of the Search)
293 W( Theorems Using a New Rationals)294 W
12504 10782 MT
(Library'', Internal Note 223, Computational)
63 W( Logic, Inc., 1717 W. Sixth Street, Suite 290, Austin,)62 W
12504 11887 MT
(TX 78703, March 1991.)SH
ES
%%Page: i 23
61200 79200 BS
0 SI
10 /Times-Roman AF
30713 75600 MT
(i)SH
13 /Times-Bold AF
26229 11604 MT
(Table of Contents)SH
12 /Times-Roman AF
9504 16027 MT
(Preface .)
1 W( . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .)SH
51600 XM
(1)SH
11 SS
11704 18068 MT
(1. Applying Different Tools to the Same Problem)
SH( .)
186 W( . . . . . . . . . . . . . . . . . . . . . . . . . . .)SH
51650 XM
(3)SH
10 SS
12504 19173 MT
(1.1. An Integrated System Verification Environment)
SH( .)
475 W( . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .)SH
51700 XM
(3)SH
12504 20278 MT
(1.2. The FM8502 Short Stack)
SH( .)
111 W( . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .)SH
51700 XM
(3)SH
12504 21383 MT
(1.3. Nqthm: A Verification Shell?)
SH( .)
140 W( . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .)SH
51700 XM
(3)SH
12504 22488 MT
(1.4. The FM9001 Short Stack)
SH( .)
111 W( . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .)SH
51700 XM
(4)SH
12504 23593 MT
(1.5. Integrating Verification Tools)
SH( .)
252 W( . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .)SH
51700 XM
(4)SH
12504 24698 MT
(1.6. Does the Approach Scale?)
SH( .)
170 W( . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .)SH
51700 XM
(6)SH
13504 25803 MT
(1.6-A. The Complexity of the FM9001 Short Stack)
SH( .)
28 W( . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .)SH
51700 XM
(6)SH
13504 26908 MT
(1.6-B. The Complexity of the Motorola MC68020)
SH( .)
389 W( . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .)SH
51700 XM
(7)SH
12504 28013 MT
(1.7. Conclusion: Logic Comes First)
SH( .)
471 W( . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .)SH
51700 XM
(8)SH
11 SS
11704 29209 MT
(2. Exchanging Data)
SH( .)
95 W( . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .)SH
51650 XM
(9)SH
11704 30405 MT
(3. Exchanging Code)
SH( .)
399 W( . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .)SH
51100 XM
(10)SH
11704 31601 MT
(4. Interface Logics)
SH( .)
525 W( . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .)SH
51100 XM
(11)SH
11704 32797 MT
(5. User Interfaces and Interaction Styles)
SH( .)
498 W( . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .)SH
51100 XM
(13)SH
10 SS
12504 33902 MT
(5.1. The Balance of Expressivity and Proof Power)
SH( .)
420 W( . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .)SH
51200 XM
(13)SH
12504 35007 MT
(5.2. User Guidance: Strategy or Tactics?)
SH( .)
4 W( . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .)SH
51200 XM
(14)SH
12504 36112 MT
(5.3. Fully Supported Syntax)
SH( .)
249 W( . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .)SH
51200 XM
(14)SH
12504 37217 MT
(5.4. Powerful Command Environment)
SH( .)
195 W( . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .)SH
51200 XM
(15)SH
12504 38322 MT
(5.5. Effective Interaction Style)
SH( .)
197 W( . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .)SH
51200 XM
(15)SH
11 SS
11704 39518 MT
(6. Significant System Verification Applications)
SH( .)
521 W( . . . . . . . . . . . . . . . . . . . . . . . . . . . .)SH
51100 XM
(15)SH
11704 40714 MT
(7. Verification as an Engineering Exercise)
SH( .)
70 W( . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .)SH
51100 XM
(16)SH
11704 41910 MT
(8. Acknowledgements)
SH( .)
64 W( . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .)SH
51100 XM
(17)SH
ES
%%Trailer
%%Pages: 23
%%DocumentFonts: Times-Roman Times-Bold Times-Italic Symbol Courier-Bold