[langsec-discuss] Proving Code

Scott Guthery sbg at acw.com
Wed Jul 9 13:05:42 UTC 2014


The cache of documents at Computational Logic, Inc., (CLI) 
(http://computationallogic.com/) may be of interest.

CLI was founded, spiritually if not legally, in 1983 by two University of 
Texas computer science professors, Robert S. Boyer and J Strother Moore. 
(Note
that Moore's first name is the alphabetic character "J" and thus does not 
get a period.) Boyer and Moore wrote a number of books about automated
theorem proving, the most famous of which is probably A Computational Logic. 
They are also and quite obviously the inventors of the eponymous string
search algorithm.  CLI shut down in 1997.

One of the notable achievements of CLI during its brief life was proving an 
entire computational stack from the netlist of the hardware up through the 
instruction set, an assembler, a programming language (Gypsy) together with 
its compiler, and even, as I dimly recall, a linker. Richard Cohen's paper, 
Proving Gypsy Programs 
(http://www.cs.utexas.edu/users/boyer/ftp/cli-reports/004.ps) is a readable 
overview of CLI's approach.

The work of George Necula on proof-carrying code and the use of physical 
unclonable function (PUFs) may also be of interest.

Cheers, Scott



More information about the langsec-discuss mailing list