Tools to formally verify programs written in languages supported by the GNU Compiler (GCC)

Question

Is there a website that maintains a list, or is there a list, of tools that support verification of programs written in languages supported by the GCC compiler front ends: C, C++, Objective-C, Fortran, Ada, Go, and D.

There seems to be various webpages for each project but no one curated website with a large list of up to date projects. A current copy of the list (if there are such websites, I've found none) should be included in any forthcoming answers, no link-only answers.

I presume that better answers will propose tools with human readable and executable specifications embedded in the target language, a tool that simply reads the code and proclaims a result is probably a "checker", "linter" or "unit tester"; such tools are not what I am asking about. For want of a better explanation I guess that it would be Design by Contract styled specifications, put another way, for the D language ddoc falls short; because it can't be proven or compiled.

A complete answer would include most of the above languages (that list is chosen because that's what GCC directly supports, without extension), I appreciate that Objective-C doesn't have an agreed upon specification; though a tool supporting the implementation used in GCC or Clang would be useful.

Example:

• C - Frama-C / ACSL

Example Frama-C code: ^{_{(from: https://www.open-do.org/wp-content/uploads/2010/08/E-ACSL.pdf)}}

/* @
requires \valid ( root ) && finite_list ( root );
assigns \nothing ;
ensures mem ( \result , root );
ensures
  \forall integer n ; mem (n , root ) == >
    \result >= n ;
*/
int max_list ( list * root );

int max_list ( list * root ) {
  int max = root - > element ;
  while ( root - > next ) {
    root = root - > next ;
    if ( root - > element > max )
      max = root - > element ;
  }
  return max ;
}

/* @ loop invariant \valid ( root ) &&
   reachable ( \at( root , Pre ) , root ) &&
   mem ( max ,\at( root , Pre )) &&
   \forall int n ;
     mem_sub (n , \at( root , Pre ) , root ) == >
       max >= n ;
*/
while ( root - > next ) {
  ...
}

Note that the annotated specifications can be proven and compiled separately from the C program, and that the toolset includes modules to assist with the writing and testing of the programs; it's a complete framework.

Note: The author of this question knows very little about this subject but is interested in learning, it is his belief that this might be an easier method to both learn proof checking and be productive use of his existing programming language's knowledge. Hopefully there are no great shortcomings in this question, and that it isn't overly complicated to answer.

Distantly related questions:

• "Which programming languages are most similar to proof assistants?"

• "Could proof assistants be used to prove that some piece of code is free of bugs?"

Answer 1

As an aside

better answers will propose tools with human readable and executable specifications embedded in the target language

FWIW, this programming style is not that far away from the notion of literate programming.

Deductive verification tools

To directly answer your question about deductive verification tools targeting GCC front-ends, there is no "official list" TTBOMK, but one such list would definitely include:

• for C programs, the Frama-C platform, relying on the ACSL specification language;
• for Ada programs, the SPARK toolset, relying on a well-delimited subset of the Ada language;

Next, some curated lists of static-analysis tools are available in the following pages:

• https://en.wikipedia.org/wiki/List_of_tools_for_static_code_analysis

• https://github.com/analysis-tools-dev/static-analysis

(Both lists mention SPARK, Frama-C and Astrée.)

Finally if you may consider adding the Coq proof assistant in your toolchain, you might also be interested in the following page:

• https://coq-community.org/awesome-coq/ (a curated list of Coq libraries, plugins and tools, which notably mentions the Verified Software Toolchain project for verifying C programs)

Further remarks

You mentioned several synonyms, while suggesting to "exclude static-analysis tools" somehow:

a tool that simply reads the code and proclaims a result is probably a "checker", "linter" or "unit tester"; such tools are not what I am asking about.

So the sequel of my answer just aims at recalling a bit of terminology, and suggesting that a tool listed as a static analyzer (possibly allowing for some literate-programming inline specification) might just as well be considered for your use case.

Admittedly, all the kinds of tools you mentioned above are "similar" but they are not necessarily "weaker" than interactive tools needing human input; they just focus on different scopes, which naturally lead to more or less expressivity… and thereby the problem under study is often undecidable; in which case we have to give up with at least one goal among correctness, completeness, or full automation… (see below).

So albeit your question specifically focuses on the GNU Compiler Collection front-ends, it may be worth it to summarize the differences between the various verification tools that can be applied to a program:

• Dynamic analysis tools (including unit testing, and profiling tools like valgrind): require to run the program, and generally can't reach exhaustive testing.
• Static analysis tools: can give a report without running the program (e.g., at compilation time);
  roughly speaking, a report is either OK (no error detected), Failed (errors detected), or No answer (timeout or so…);
  • the tools from this category that can't raise false-negatives are said to be sound;
    in other words, an OK report will guarantee the absence of runtime error (w.r.t. the kind of runtime error handled by the tool, of course);
  • the tools from this category that can't raise false-positives (a.k.a. false alarms) are said to be complete;
    in other words, a Failed report will guarantee the presence of a runtime error, if ever the program is run in this context.
• The study of sound static-analysis tools is part of the formal methods research domain, which also encompasses that of proof assistants.
  And there are several bridges between the various subdomains of formal methods:
  • for instance we can combine deductive-verification tools and proof assistants to formally verify a C program: annotate the C code using ACSL, use the Frama-C static analyzer to generate Proof-Obligations, and use one of the plugins available (Jessie or WP) to discharge them in an interactive proof assistant like Coq; and finally compile the verified C code using gcc (or a verified compiler like CompCert C, as said in the comments).