--- layout: fc_discuss_archives title: Message 5 from Frama-C-discuss on October 2010 ---
Hi, this is a proposal for a feature: When writing and verifying code, you typically do the following: repeat change some lines in your code or specification run Jessie until verified I'd like to considerably reduce the time needed for Jessie in this loop. The Visual Studio plugin for Spec# has a feature that lets the verifier run each time the content of the buffer has been changed. This gives immediate feedback and greatly improves productivity because you can very quickly narrow down the reason why the code doesn't verify. Is a similar feature possible for Frama-C/Jessie? For example, Frama-C may watch the source file. Each time a change is detected, Jessie is run again, but only for the parts that changed. Thus, contracts for unaltered functions that had previously been verified don't have to be verified again, which will save a lot of time. Caching of proofs and failed proofs may also speed up Jessie. -- Regards, Boris