91
$\begingroup$

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?

Improve this question
$\endgroup$
9
  • 3
    $\begingroup$ I 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. $\endgroup$
    – Raphael
    Commented Aug 17, 2013 at 12:13
  • 3
    $\begingroup$ I 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? $\endgroup$
    – Frank
    Commented Aug 17, 2013 at 15:03
  • 2
    $\begingroup$ So that's four questions, then. 1) is probably better off on Software Engineering 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 Software Engineering with the first and think hard on whether you can expect an objective (!) answer here (!) before posting 2). $\endgroup$
    – Raphael
    Commented Aug 18, 2013 at 10:57
  • 12
    $\begingroup$ You'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). $\endgroup$
    – Yuval Filmus
    Commented Aug 19, 2013 at 0:27
  • 9
    $\begingroup$ The 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. $\endgroup$
    – Andrej Bauer
    Commented Aug 21, 2013 at 11:13

8 Answers 8

Reset to default
49
$\begingroup$

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.

Improve this answer
$\endgroup$
3
  • 1
    $\begingroup$ 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... $\endgroup$
    – Frank
    Commented Aug 20, 2013 at 19:14
  • 9
    $\begingroup$ The 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. $\endgroup$
    – cody
    Commented Aug 29, 2013 at 20:25
  • $\begingroup$ 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). $\endgroup$
    – Frank
    Commented Aug 29, 2013 at 20:34
22
$\begingroup$

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.

  1. 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.

  2. 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.

  3. 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.

Improve this answer
$\endgroup$
6
$\begingroup$

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.

Improve this answer
$\endgroup$
1
  • 7
    $\begingroup$ Thanks 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. $\endgroup$
    – David Richerby
    Commented Nov 4, 2014 at 11:58
4
$\begingroup$

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.

Improve this answer
$\endgroup$
2
  • $\begingroup$ The advantage of formal verification is that .... A second disadvantage of formal verification is that ... This is confusing. $\endgroup$
    – hengxin
    Commented Jan 23, 2016 at 6:16
  • $\begingroup$ I think mismatch between specification and informal task is a software requirement analysis issue not a programming issue. $\endgroup$
    – Kaveh
    Commented Jan 24, 2016 at 0:17
2
$\begingroup$

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.

Improve this answer
$\endgroup$
12
  • 3
    $\begingroup$ It'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". $\endgroup$
    – Martin Berger
    Commented Aug 23, 2013 at 11:20
  • 2
    $\begingroup$ did 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. $\endgroup$
    – vzn
    Commented Aug 23, 2013 at 15:03
  • 2
    $\begingroup$ agreed 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. $\endgroup$
    – vzn
    Commented Aug 23, 2013 at 15:30
  • 2
    $\begingroup$ by the way there seem to be some formal verification principles also used in the JRE, java runtime engine, eg dynamic optimization, etc... $\endgroup$
    – vzn
    Commented Aug 24, 2013 at 18:57
  • 3
    $\begingroup$ that 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! $\endgroup$
    – vzn
    Commented Aug 25, 2013 at 16:01
2
$\begingroup$

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.

Improve this answer
$\endgroup$
1
$\begingroup$

Hi I work in the hardware space, and I can let you know that there are industry tools made by the EDA companies which make this effort a lot more dumbed-down than the expertise required to learn and work with theorem provers.

Although the current tools are catered more towards hardware verification, but internally I know they are developing and deploying tools that abstract out all the "fun" elements of theorem proving at the backend so that the users work on a plug-n-play sort of an interface. It is kind of getting closer to a tester ecosystem although not perfect.

I believe you'd need higher order logic to actually reason about programs and hence there is no replacing the theorem provers. As @cody and @hengxin point out there are software companies that do employ teams with the skillset to verify their safety-critical code portions. But widespread adoption can only come through plug-n-play type tools that I know the hardware industry is heavily investing in through the above companies listed.

Improve this answer
$\endgroup$
0
$\begingroup$

Symbolic Execution is a concept which has gained traction due to the advances in constraint solving, increasing computational power and recently DARPA Cyber Grand Challenge, which can be used for Formal Verification.

Roughly speaking, it executes the program using symbolic values (variables) instead of actual inputs, and as the execution proceeds it gathers constraints on the symbols. Given a precondition and postcondition, we can use rules of inference to verify whether the constraints gather imply the postcondition, assuming it starts from the precondition.

There are many tools available for symbolic execution, which can handle fairly large codebases and are used in the industry, although many of the use cases arise from a cybersecurity perspective.

Improve this answer
$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.