The Coq mailing list

[Ron <iampure AT gmail.com>]

Hi,

I am new to this list and interested in using a theorem prover to
semi-automatically prove that a certain executable containing binary
code(thus a dissassembly needs to be generated first) on e.g. Linux
contains no possibility for e.g. a buffer-overflow. Coq seems to be a
well developed theorem prover, however, I read in Chapter 1 of Coq'Art
that Coq can't prove theorems about all computable functions(in
particular those that not terminate). So, it seems I can't use Coq for
my purposes, since I need to prove things over programs that are
possibly interactive, and hence don't need to terminate. Could anyone
provide some pointers, in case, it is possible to still use Coq?

 More in general, it seems everyone ignores I/O (I have only seen the
proof of the correctness of simple functions like max, sum, average,
etc in some high-level language in the papers I skimmed). Is there
some "trick" which makes I/O a non-issue? (I have seen dependent types
approaches, but those seem to be still at the theoretical level).

More on the limitations of Coq. I have been taught that predicate
calculus can represent programs, so this would imply Coq can't do
this. OTOH, I read somewhere else that someone embedded predicate
logic in Coq. So, some of the above assertions must be wrong. Which
one?

In case Coq is not up to the task, what theorem provers are?

Regards, R.

P.S. I would greatly appreciate pointers to papers tackling the
problem of proving general properties given plain binaries which do
I/O.