[langsec-discuss] Proving Code
Meredith L. Patterson
clonearmy at gmail.com
Wed Jul 9 16:06:49 UTC 2014
I think that would be a great thing to have, have never seen one, and am
totally down to help with writing one.
Also, Scott, I hadn't seen the CLI papers before -- thank you for the link!
On Wed, Jul 9, 2014 at 7:20 AM, Jacob Torrey <jacob at jacobtorrey.com> wrote:
> 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.
> 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.
>> 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
>> 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
>> 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
> langsec-discuss mailing list
> langsec-discuss at mail.langsec.org
-------------- next part --------------
An HTML attachment was scrubbed...
More information about the langsec-discuss