proof double checking and verified compilers

William McCune (mccune@mcs.anl.gov)
Tue, 12 Dec 1995 15:47:17 -0600

Messages sorted by: [ date ][ thread ][ subject ][ author ]
Next message: Amy Felty: "CADE-13 Second Call for Papers (text & LaTeX)"
Previous message: Roman Matuszewski: "QED II - final report - available"

A funny QED-motivating thing happened to me yesterday:
(1) Compile Otter unoptimized, it seems to run correctly
and gets a correct proof. (2) Compile Otter optimized,
run it on the same input and get an unsound proof---no core
dump, no error, proof "looks" ok, but has a bad
inference. (Compiler is gcc 2.5.8.)

Bill McCune

Next message: Amy Felty: "CADE-13 Second Call for Papers (text & LaTeX)"
Previous message: Roman Matuszewski: "QED II - final report - available"