Formal program verification in practice

Question Detail: 

As a software engineer, I write a lot of code for industrial products. Relatively complicated stuff with classes, threads, some design efforts, but also some compromises for performance. I do a lot of testing, and I am tired of testing, so I got interested in formal proof tools, such as Coq, Isabelle... Could I use one of these to formally prove that my code is bug-free and be done with it? - but each time I check out one of these tools, I walk away unconvinced that they are usable for everyday software engineering. Now, that could only be me, and I am looking for pointers/opinions/ideas about that :-)

Specifically, I get the impression that to make one of these tools work for me would require a huge investment to properly define to the prover the objects, methods... of the program under consideration. I then wonder if the prover wouldn't just run out of steam given the size of everything it would have to deal with. Or maybe I would have to get rid of side-effects (those prover tools seem to do really well with declarative languages), and I wonder if that would result in "proven code" that could not be used because it would not be fast or small enough. Also, I don't have the luxury of changing the language I work with, it needs to be Java or C++: I can't tell my boss I'm going to code in OXXXml from now on, because it's the only language in which I can prove the correctness of the code...

Could someone with more experience of formal proof tools comment? Again - I would LOVE to use a formal prover tool, I think they are great, but I have the impression they are in an ivory tower that I can't reach from the lowly ditch of Java/C++... (PS: I also LOVE Haskell, OCaml... don't get the wrong idea: I am a fan of declarative languages and formal proof, I am just trying to see how I could realistically make that useful to software engineering)

Update: Since this is fairly broad, let's try the following more specific questions: 1) are there examples of using provers to prove correctness of industrial Java/C++ programs? 2) Would Coq be suitable for that task? 3) If Coq is suitable, should I write the program in Coq first, then generate C++/Java from Coq? 4) Could this approach handle threading and performance optimizations?

Asked By : Frank

Best Answer from StackOverflow

Question Source : http://cs.stackexchange.com/questions/13785

Answered By : cody

I'll try to give a succinct answer to some of your questions. Please bear in mind that this is not strictly my field of research, so some of my info may be outdated/incorrect.

1. There are many tools that are specifically designed to formally prove properties of Java and C++.

   However I need to make a small digression here: what does it mean to prove correctness of a program? The Java type checker proves a formal property of a Java program, namely that certain errors, like adding a float and an int, can never occur! I imagine you are interested in much stronger properties, namely that your program can never enter into an unwanted state, or that the output of a certain function conforms to a certain mathematical specification. In short, there is a wide gradient of what "proving a program correct" can mean, from simple security properties to a full proof that the program fulfills a detailed specification.

   Now I'm going to assume that you are interested in proving strong properties about your programs. If you are interested in security properties (your program can not reach a certain state), then in general it seems the best approach is model checking. However if you wish to fully specify the behavior of a Java program, your best bet is to use a specification language for that language, for instance JML. There are such languages for specifying the behavior of C programs, for instance ACSL, but I don't know about C++.

2. Once you have your specifications, you need to prove that the program conforms to that specification.

   For this you need a tool that has a formal understanding of both your specification and the operational semantics of your language (Java or C++) in order to express the adequacy theorem, namely that the execution of the program respects the specification.

   This tool should also allow you to formulate or generate the proof of that theorem. Now both of these tasks (specifying and proving) are quite difficult, so they are often separated in two:

   • One tool that parses the code, the specification and generates the adequacy theorem. As Frank mentioned, Krakatoa is an example of such a tool.

   • One tool that proves the theorem(s), automatically or interactively. Coq interacts with Krakatoa in this manner, and there are some powerful automated tools like Z3 which can also be used.

   One (minor) point: there are some theorems which are much too hard to be proven with automated methods, and automatic theorem provers are known to occasionally have soundness bugs which make them less trustworthy. This is an area where Coq shines in comparison (but it is not automatic!).

3. If you want to generate Ocaml code, then definitely write in Coq (Gallina) first, then extract the code. However, Coq is terrible at generating C++ or Java, if it is even possible.

4. Can the above tools handle threading and performance issues? Probably not, performance and threading concerns are best handled by specifically designed tools, as they are particularly hard problems. I'm not sure I have any tools to recommend here, though Martin Hofmann's PolyNI project seems interesting.

In conclusion: formal verification of "real world" Java and C++ programs is a large and well-developed field, and Coq is suitable for parts of that task. You can find a high-level overview here for example.