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! Cheers, --mlp On Wed, Jul 9, 2014 at 7:20 AM, Jacob Torrey <ja...@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. > > Jacob > > > On Wed, Jul 9, 2014 at 7:05 AM, Scott Guthery <s...@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@mail.langsec.org >> https://mail.langsec.org/cgi-bin/mailman/listinfo/langsec-discuss >> > > > _______________________________________________ > langsec-discuss mailing list > langsec-discuss@mail.langsec.org > https://mail.langsec.org/cgi-bin/mailman/listinfo/langsec-discuss > >
_______________________________________________ langsec-discuss mailing list langsec-discuss@mail.langsec.org https://mail.langsec.org/cgi-bin/mailman/listinfo/langsec-discuss
