[langsec-discuss] Proving Code

Jacob Torrey jacob at jacobtorrey.com
Wed Jul 9 14:20:11 UTC 2014


In this vein of discussion, is there (and if not, should we try and make
one) a basic "Dummies Guide" to the current capabilities and limitations of
formal verification/proofs of correctness? I've seen a huge range of
opinions and comments on FM and I think a easily approachable entry-point
would be a helpful contribution. One of the issues that should be
highlighted is some of the implicit or explicit assumptions and tying this
back to LangSec, the example from the workshop about failures in PCC if the
author did not fully define an assumption.

Jacob


On Wed, Jul 9, 2014 at 7:05 AM, Scott Guthery <sbg at acw.com> wrote:

> 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
>
> _______________________________________________
> langsec-discuss mailing list
> langsec-discuss at mail.langsec.org
> https://mail.langsec.org/cgi-bin/mailman/listinfo/langsec-discuss
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://mail.langsec.org/pipermail/langsec-discuss/attachments/20140709/c290e17f/attachment.html>


More information about the langsec-discuss mailing list