Theorem Proving for Verification - UT Computer Science

Prologue. When I look at the state of our science today, I am amazed and proud of how far we've come and what is routinely possible today with mechanized ...
896KB Sizes 1 Downloads 269 Views
Theorem Proving for Verification the Early Days

J Strother Moore Department of Computer Sciences University of Texas at Austin 1

Prologue When I look at the state of our science today, I am amazed and proud of how far we’ve come and what is routinely possible today with mechanized verification. But how did we get here?

2

A personal perspective on the journey

Xerox PARC & SRI ’74−81

University of Edinburgh ’70−73

UT Austin & CLI

MIT ’66−70 Dickinson, Texas −, 1966

3

Hope Park Square, Edinburgh, 1970

4

Hope Park Square, Edinburgh, 1970 Rod Burstall Donald Michie Bernard Meltzer Bob Kowalski Pat Hayes

5

Hope Park Square, Edinburgh, 1970 Rod Burstall Donald Michie Bernard Meltzer Bob Kowalski Pat Hayes Gordon Plotkin 1968

6

Hope Park Square, Edinburgh, 1970 Rod Burstall Donald Michie Bernard Meltzer Bob Kowalski Pat Hayes Gordon Plotkin 1968 Mike Gordon 1970 J Moore 1970

7

Hope Park Square, Edinburgh, 1970 Rod Burstall Donald Michie Bernard Meltzer Bob Kowalski Pat Hayes Gordon Plotkin 1968 Mike Gordon 1970 J Moore 1970 Bob Boyer 1971 Alan Bundy 1971

8

Hope Park Square, Edinburgh, 1970 Rod Burstall Donald Michie Bernard Meltzer Bob Kowalski Pat Hayes Gordon Plotkin 1968 Mike Gordon 1970 J Moore 1970 Bob Boyer 1971 Alan Bundy 1971 Robin Milner 1973

9

Our Computing Resources

64KB of RAM, paper tape input

10

11

Instead of debugging a program, one should prove that it meets its specifications, and this proof should be checked by a computer program. — John McCarthy, “A Basis for a Mathematical Theory of Computation,” 1961

12

Theorem Proving in 1970 resolution: a complete, first-order, uniform proof-procedure based on unification and cut

13

{

x

y

z

}{

x

y

z

}

14

{

x

y

z

}{

u

v

w

}

15

{

}{

}

16

{ {x u

}{

}

(F u (G v)), (H z)}

Most General Unifier

17

{ {x u

}{

}

(F u (G v)), (H z)}

Most General Unifier

18

{ {x u

}{

}

(F u (G v)), (H z)}

Most General Unifier

19

{

}

20

{

}{

}

Resolve

{

} 21

{

}{

}

Resolve

{

} 22

Structure Sharing clause: a record of the two parents and binding environment Memory

k

{

}

{

} n

Left Parent Right Parent k n var L/R term

Selected Lits L/R

var L/R term

L/R

Most General Unifier

‘‘Frame’’ aka ‘‘clause’’

23

Structure Sharing clauses are their own derivations standardizing apart is implicit (free) linear resolution can be done on a stack of frames resolvents cost fixed space plus a “binding environment” 24

all terms are specific instances of original ones unifiers can be preprocessed easy to attach pragmas (and other metadata) to variables and clauses

25

Such observations encouraged in Edinburgh the view that predicate calculus could be viewed as a programming language

26

But Boyer and I were interested in computational logic: • a logic convenient for talking about computat