--- layout: fc_discuss_archives title: Message 75 from Frama-C-discuss on October 2013 ---
-- Fran?ois Bobot (2013-10-18) > > If you are using the plugin Jessie or the plugin WP, you can already prove your goal using why3. And why3 has a session mechanism through the commands why3ide, why3replayer and why3session. A session allow you the kind of cache David is referring. > > In fact GNATprove also use why3 for that ;). not only! :) We use compiler-like dependencies plus semantic dependencies to completely avoid regenerating VCs that cannot be impacted by a source code change. And on top of that, we use Why3 session mechanism (with hashes computed for VCs) to avoid calling the prover on a VC already proved. -- Yannick Moy, Senior Software Engineer, AdaCore