[langsec-discuss] Proving Code
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.
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.
More information about the langsec-discuss