Formal program verification in practice

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?

Frank

Posted 2013-08-17T01:51:39.910

Reputation: 1 392

I would also suggest at looking at Eric Hehner's 'A Practical Theory of Programming', which he offers online for free. (http://www.cs.toronto.edu/~hehner/aPToP/) His theory doesn't have a proof assistant to my knowledge, but for software development I believe it has a greater potential since you could refine a program as you prove its correctness.

– Francesco Gramano – 2016-09-27T17:59:16.273

3I get and appreciate your problem, but I don't understand what this question is after (as an SE post). Discussion? Experience? Neither is suitable for SE. The "Whatever can I do?" tone makes me feel this is too broad a question, too. – Raphael – 2013-08-17T12:13:26.597

3I see... I agree this question was not formulated clearly. So, let's say: 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 have Coq generate C++/Java from that? 4) Could this approach cope with threading and performance optimizations? – Frank – 2013-08-17T15:03:22.947

2So that's four questions, then. 1) is probably better off on [programmers.SE] since you are unlikely to run into (many) industry professionals here. 2) tastes somewhat subjective, but we may have people here that can offer an objective perspective. 3) is, as far as I can tell, completely subjective. 4) Is a nice questions for this site. In summary: please separate your questions, go to [programmers.SE] with the first and think hard on whether you can expect an objective (!) answer here (!) before posting 2). – Raphael – 2013-08-18T10:57:08.040

1IMHO, 3 is not necessarily subjective: I do not know if it is possible/efficient to generate code from Coq. I would like to know if someone has done it/can share their experience. 2) IMHO is a little bit of the same. It would be great to get feedback, for example that Coq is not suited for that, but Krakatoa is (maybe) :-) – Frank – 2013-08-18T14:52:36.017

10You're describing the dream of formal verification, but we're very far from being there. AFAIK, program verification is a non-routine task, and only applies to very simple programs. That said, I think that this question is spot-on for the site, and I would appreciate someone from the area admitting the limits of their field, explaining the state-of-the-art and the limitations (perhaps by linking to some survey). – Yuval Filmus – 2013-08-19T00:27:04.747

9The trouble with verifying C++ programs is that C++ is not a well-defined language. I do not think large-scale verification is possible until many parts of software systems (OS, libraries, programming languages) actually get redesigned to support verification. As is well known, you cannot just dump 200000 lines of code on someone and say "verify!". You need to verify and write code together, and you need to adapt your programming habits to the fact that you're also verifying. – Andrej Bauer – 2013-08-21T11:13:56.723

some tiein to this TCS question, "how to create mission critical software"

– vzn – 2013-08-22T15:45:34.167

Answers

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.

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++.
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!).
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.
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.

cody

Posted 2013-08-17T01:51:39.910

Reputation: 7 463

Thanks for this post and the references you added. IMHO, the goal for software engineers is to be able to quickly release systems that will 1) always provide correct results, 2) never fail. I could see a regression problem here, where you might want to prove that the specification itself is "bug free" :-) kind of like trying to define "true proposition of a language" with a meta-language, then needing another meta-language for that, then another one... – Frank – 2013-08-20T19:14:49.230

6The problem is that what the user "wants" is usually not expressed in a formal language! There is generally no formal answer to the question: "does this formal specification conform to my informal idea?". It's possible to test a formal specification, and prove that it has certain mathematical properties, but ultimately you need to relate the mathematics to the real world, which is a non-formal process. – cody – 2013-08-29T20:25:08.133

Yes of course - I always realized the formal methods could only start from a well defined point. If that specification conforms or not to the conscious/unconscious/undiscovered needs of real-life users is another problem, not addressable with formal methods (but certainly a problem for engineers). – Frank – 2013-08-29T20:34:04.297

I would like to mention three remarkable applications of formal methods/formal verification tools in industry or non-trivial real systems. Note that I have little experience on this topic and I only learn them from reading papers.

The open-source tool Java Pathfinder (JPF for short) released by NASA in 2005 is a system to verify executable Java bytecode programs (see Java Pathfinder@wiki). It has been used to detect inconsistencies in the executive software for the K9 Rover at NASA Ames.
This paper: Using Model Checking to Find Serious File System Errors@OSDI'04 shows how to use model checking to find serious errors in file systems. A system called FiSC is applied to three widely-used, heavily-tested file systems: ext3, JFS, and ReiserFS, and 32 serious bugs are found. It won the Best Paper Award.
This paper: How Amazon Web Services Uses Formal Methods@CACM'15 describes how AWS applies formal methods to its products like S3, DynamoDB, EBS, and Internal distributed lock manager. It focuses on Lamport's TLA+ tool. By the way, Lamport has intensively used his own TLA toolbox. He often gives a (quite complete) formal verification in TLA of the algorithms/theorems proposed by himself (as well as coauthors) in appendixes to the papers.

hengxin

Posted 2013-08-17T01:51:39.910

Reputation: 8 823

Formal verification is now possible for programs written a subset of C++ designed for safety-critical embedded systems. See http://eschertech.com/papers/CanCPlusPlusBeMadeAsSafeAsSpark.ppt for a short presentation, and http://eschertech.com/papers/CanCPlusPlusBeMadeAsSafeAsSpark.pdf for the full paper.

dc42

Posted 2013-08-17T01:51:39.910

Reputation: 49

5Thanks for the links. At least a brief overview of their content would be useful, to guard against link-rot, especially since your links are to a corporate website: those tend to get periodically reorganized, killing all links into the site. – David Richerby – 2014-11-04T11:58:18.713

A formal specification of a program is (more or less) a program written in another programming language. As a result, the specification will certainly include its own bugs.

The advantage of formal verification is that, as the program and the specification are two separate implementations, their bugs will be different. But not always: one common source of bugs, overlooked cases, will often match. Thus, formal verification is not a panacea: it can still miss a non-trivial number of bugs.

A disadvantage of formal verification is that it can impose something like twice the implementation cost, probably more (you need a specialist in formal specification, and you need to use the more or less experimental tools that come with it; that won't come cheap).

I'd guess setting up test cases and scaffolding to run them automatically would be a better use of your time.

vonbrand

Posted 2013-08-17T01:51:39.910

Reputation: 12 507

The advantage of formal verification is that .... A second disadvantage of formal verification is that ... This is confusing. – hengxin – 2016-01-23T06:16:34.917

I think mismatch between specification and informal task is a software requirement analysis issue not a programming issue. – Kaveh – 2016-01-24T00:17:40.433

You ask a few different questions. I agree it does appear that formal verification methods for industrial/commercial applications are not so common. one should realize however that a lot of "formal verification" principles are built into compilers to determine program correctness! so in a way, if you use a modern compiler, you're using much of the state-of-the-art in formal verification.

You say "I'm tired of testing" but formal verification is not really a substitute for testing. in a way its a variation on testing.

You mention Java. there are many advanced formal verification methods built into a java verification program called FindBugs which indeed can be run over large codebases. Note it will turn up both "false positives and false negatives" and the results need to be reviewed/analyzed by a human developer. But note even if it is not turning up real functional defects, it does generally turn up "antipatterns" that should be avoided in code anyway.

You make no more mention of your particular application other than "industrial". Formal verification in practice tends to depend on the particular application.

Formal verification techniques seem to be widely used in EE to prove circuit correctness e.g. in microprocessor design.

Here is an example of a survey of formal verification tools in the EE field by Lars Philipson.

vzn

Posted 2013-08-17T01:51:39.910

Reputation: 10 652

@MartinBerger, you are presumably aware that proving two programs to be equivalent is undecidable. Not merely hard, but can't be done even in theory (given unlimited resources). – vonbrand – 2016-01-23T14:09:13.813

1@vonbrand Yes, I am. I teach this kind of stuff to my students every year. Why? – Martin Berger – 2016-01-23T15:03:47.450

2It's misleading to say that "a lot of "formal verification" principles are built into compilers to determine program correctness". What you refer to is static type-checking which some compilers do, but the properties verified that way are rather simple, e.g. avoiding adding a number and a string. This is helpful, but a far cry from what is usually understodd by "formal verification". – Martin Berger – 2013-08-23T11:20:10.600

2did not refer to static type checking specifically, although that is one simple/common example. imho compiler optimization techniques, which are widespread and advanced, are roughly similar to formal verification principles, because they involve advanced techniques to determine/show equivalence of optimized program variants. so it seems it is important to avoid the "moving goalposts" issue here and not assume that merely because a compiler does it or its built into the compiler, its not formal verification. – vzn – 2013-08-23T15:03:23.783

1OK, fair enough. However, even the program equivalence checks that you refer to only do simple stuff, e.g. could not show that mergesort have equivalent externally visible behaviour to quicksort etc. The original question clearly asked if using tools like Coq, Isabelle, Agda are usable in practise to show whether programs written in eg. C++ satisfy their specifications. (The short answer to this question is: no, not at this point.) – Martin Berger – 2013-08-23T15:25:05.517

2agreed this is not a common understanding. the optimization techniques roughly are creating a model of program behavior eg of a loop or subroutine, and optimizing that model, and then generating new code that is provably equivalent. so some of these optimizations are quite sophisticated in rearranging code & to me they make use of formal verification principles. there seem to be many other examples of formal verification methods in the compiler... the original question asked many different questions as many have noted, am defn not attempting to answer all the questions contained therein. – vzn – 2013-08-23T15:30:44.013

IMHO, unfortunately, just being able to compile e.g. a C++ program really doesn't mean that it doesn't have bugs... To me, verification entails a lot more "guarantees" than merely being able to compile. That bar is too low to be really useful for quality in software engineering, IMHO. – Frank – 2013-08-24T04:49:08.833

1verification does not guarantee you have no bugs either. nothing in the response says merely compiling is sufficient and it explicitly states exactly the opposite, verification is not a substitute for testing. – vzn – 2013-08-24T18:54:51.293

2by the way there seem to be some formal verification principles also used in the JRE, java runtime engine, eg dynamic optimization, etc... – vzn – 2013-08-24T18:57:25.243

1@vzn - I don't know... mathematical theorems do not require "testing". I'd like to move from testing programs to proving they are correct given a specification. IMHO, that would be a lot more productive than testing. Also, testing is inductive, whereas proving would be deductive. Moving from induction to deduction would be very fruitful, IMHO. – Frank – 2013-08-24T20:25:31.333

3that is "the dream of formal verification" referred to by filmus above, imho a chimeric abstraction, and pragmatic/utilitarian/realistic industry largely recognizes it as such. large codebases have been known for decades to inherently have $x$ bugs/defects per $y$ K-lines of code and this will never change no matter how theory/technology advances, its a fact of human nature. and in fact human-created mathematical theorems have the same properties, although this is not widely appreciated! – vzn – 2013-08-25T16:01:16.337

this is again a not widely understood concept, but what really is different from test-driven-development or junit testing from formal verification? the boundaries where one starts and one ends off are really not so distinct when (re)considered! in a way these two widespread development methodologies are the accepted industry best-practice/design pattern formulations of formal verification principles from academia!

– vzn – 2013-08-25T16:11:38.230

Perhaps, a model checker may be helpful.

http://alloytools.org/documentation.html Alloy is a model checker.

A nice presentation explaining the concept of model checking using Alloy: https://www.youtube.com/watch?v=FvNRlE4E9QQ

In the same family of tools comes 'property-based testing', they all try to find a counter-example for the given specification model of your software.

ticktock

Posted 2013-08-17T01:51:39.910

Reputation: 111