--- layout: fc_discuss_archives title: Message 7 from Frama-C-discuss on May 2020 ---
Hello Mike, > Finally, for debugging is there any kind of symbolic debugger or way to get counterexample information? The VeriFast tool has a nice IDE where you can forward/back-step through a program with a symbolic heap. At the moment, when a proof fails, I just stare hard at it and try to figure out how to fix it, but I would expect power-users have a few more things in their bag of tricks. The WP tutorial did not have a lot of information on this aspect. I can totally understand this feeling because I have been working (https://github.com/fraunhoferfokus/acsl-by-example) with WP for a long time and also know VeriFast very well. The truth, however, is that I got used to it. At the same time, proving is expected to require a lot of thinking which sometimes might involve staring for a long time on some snippets of code and writing tests to check whether some assumptions that one has made are really valid. In fact, Frama-C also supports the combination of formal verification and testing but other people can tell you more about this. I am not a Frama-C developer but as far as I understand, Frama-C in general and WP in particular have been originally developed for domains where safety is of utmost importance. Think of air planes and nuclear power plants. These safety-related domains are regulated by very strict system/software development processes. Quick turn-arounds or agile development have only slowly entered these domains. In particular, it is often required in these domains that during the process of verification no (accidental) code changes can occur. The simplest way to achieve this is to omit the editor in the gui of the verification tool⦠Regards Jens