[bitc-dev] Carrying proofs of BitC code

Pierre THIERRY nowhere.man at levallois.eu.org
Fri Jul 7 18:00:22 EDT 2006


Hi,

I was wondering if you guys have already made a decision about which
tool(s) to carry proofs on BitC code.

As I'm just learning them, I'd like to know if extracting verfication
conditions with a tool like Why[1] and then prooving the obligations
with Coq[2], possibly after discharging some of them automatically with
a decision procedure, would be a viable modus operandi for Coyotos.

Curiously,
Nowhere man
 
[1] http://coq.inria.fr/
[2] http://why.lri.fr/
-- 
nowhere.man at levallois.eu.org
OpenPGP 0xD9D50D8A
-------------- next part --------------
A non-text attachment was scrubbed...
Name: not available
Type: application/pgp-signature
Size: 189 bytes
Desc: Digital signature
Url : http://www.coyotos.org/pipermail/bitc-dev/attachments/20060708/2057e956/attachment.bin 


More information about the bitc-dev mailing list