6
$\begingroup$

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:

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:

$\endgroup$
5
  • $\begingroup$ Searching all sites I can see at least half a dozen similarly styled questions, that are not duplicates of this one. $\endgroup$
    – Rob
    Feb 25, 2022 at 22:07
  • 1
    $\begingroup$ there is a Coq-certified compiler for C, COMCERT, cf. vst.cs.princeton.edu $\endgroup$ Feb 26, 2022 at 16:15
  • $\begingroup$ What is the role of GCC in this question? Are you interested in tools for those languages individually (which are likely to be very different from each other and likely not based on the GCC toolchain) or something which can show the correctness of GCC-compiled code? $\endgroup$ Feb 26, 2022 at 21:57
  • $\begingroup$ @GregoryNisbet, that question ("What is the role of GCC in this question?") is answered in my question. $\endgroup$
    – Rob
    Feb 26, 2022 at 22:55
  • $\begingroup$ A similar question has been asked specifically about Fortran (with no answers): fortran-lang.discourse.group/t/… and this might assist in researching an answer: en.wikipedia.org/wiki/Verification_condition_generator $\endgroup$
    – Rob
    Mar 1, 2022 at 1:22

1 Answer 1

-1
$\begingroup$

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:

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

(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:

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).
$\endgroup$
3
  • $\begingroup$ Let me make my prior comment clearer. I think the first two paragraphs of my question are very clear (as is the remainder), this answer doesn't attempt to answer the question. This answer, in its current state, is unacceptable. $\endgroup$
    – Rob
    Mar 1, 2022 at 0:26
  • $\begingroup$ OK… (BTW, it seems your prior comment was lost). So I refactored my answer to make the structure clearer (the "direct answer" was a bit melded with the extra context); and I added two more lists on this topic. $\endgroup$
    – ErikMD
    Mar 1, 2022 at 0:58
  • 2
    $\begingroup$ I was shocked to see this flagged as a VLQ. $\endgroup$ Mar 1, 2022 at 14:48

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.