--- layout: fc_discuss_archives title: Message 9 from Frama-C-discuss on January 2010 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Jessie+Why 2.23+Gappa 0.12.3 unable to prove many binary_search VCs



David A. Wheeler a ?crit :

> Gappa 0.12.3 cannot handle most of the VCs.

Seeing that there isn't even a single floating-point number in your 
code, the contrary would have been surprising. (In fact, it comes as a 
good surprise to me that Gappa is able to prove 30% of the VCs on your 
example.)

Gappa is not a generic (SMT) prover like Alt-Ergo, CVC3, Z3, Simplify, 
etc. It is a specialized prover dedicated to proving properties on 
floating-point expressions, as they are usually out of reach of the 
above tools. It comes as a complement to the other tools, not as a 
replacement.

Best regards,

Guillaume