Comparison of functional program verifiers

This is a comparison of various tools for “verifying” that a piece of code (written in a functional programming style) fulfils a specification, with some degree of automation, to various degrees of confidence.

I’m not putting this on Wikipedia, because many Wikipedia editors will summarily delete supposedly “non-notable” table rows in tables, despite there being no Wikipedia policy to do so.

Note: DSolve is currently not included because the published version does not support recursive types, such as List.

Basics

Name Available for download Mode(s) Solvers Operates on
Leon Yes Automated Z3 Scala
Isabelle Yes Interactive Various Various4
Coq Yes Interactive2 Built-in2 Various4
Dafny Yes Automated1 Z3 Dafny
ScalaCheck3 Yes Stochastic None – direct execution Scala / Any
HMC No Automated Various ML
ACL2 Yes Automated, stochastic Built-in ACL2

1 Dafny really shows that the lines between interactive and automated provers have blurred. It has an intriguing feature – the ability to prove lemmas by giving the solver enough hints to let it prove it by itself, and then have those lemmas be automatically employed by the solver. I am not sure whether any other system offers such a feature, as such.2

2 Coq does not yet integrate with any solvers (other than its built-in decision procedures), though a project is underway to change this. So why would you want to use Coq instead of Isabelle at the present time? Well, one possible reason is that Coq supports dependent types (although not in such a convenient way as languages specifically designed for dependently-typed programming), whereas Isabelle doesn’t.

3 ScalaCheck is one of a family of independently-developed tools named something-Check, which began with QuickCheck (which is for Haskell).

4 These tools (Coq and Isabelle) both support code extraction to proper programming languages. Alternatively, there are front-ends to both which can read e.g. Java code and specifications, and create corresponding proof obligations. So don’t worry about being able to execute your code with reasonable performance outside of the tool – you will be able to.

Features

Name Static typing Proof by induction Verifying higher-order functions Natively supports imperative code IDE
Leon Yes Yes No No No
Isabelle Yes Yes Yes No Emacs or JEdit
Coq Yes Yes Yes No1 Emacs or CoqIDE
Dafny Yes Yes ? Yes Emacs
ScalaCheck Yes No Yes Yes Any
HMC Yes ? Yes ? ?
ACL2 No Yes No No Emacs or Eclipse

1 Coq does not support imperative programming “natively”, but it can be done in Coq, using e.g. Ynot or Bedrock.

Corrections and additions can be supplied by comment below or by email; please supply a citation to a reliable source in every case.

Tweet about this on Twitter10Share on Reddit0Share on Facebook1Share on Google+5Share on TumblrShare on LinkedIn1Pin on Pinterest0Share on StumbleUpon0Email this to someonePrint this page

2 comments

  1. gasche says:

    Coq has some integration with externals tools such as the “gappa” verifier for floating-point arithmetic: http://gappa.gforge.inria.fr/
    (But it’s right that there is currently no standard way to call a general-purpose first-order prover.)

    You may also be interested in the “Why3″ tool, which has done a lot of work on integration of programming and specification by calling external solvers. You are here focusing on tools that help reason on one or several languages; Why3 is more like a language on which you can reason with one or several tools. (You could also debate whether it’s “functional” given that it also has fairly imperative constructs; in practice verified program are often largely written in a functional style).
    http://why3.lri.fr/

  2. Liam says:

    Isabelle supports imperative code (as a library). For example, we translate C into SIMPL and verify it for seL4 in isabelle.

Leave a Reply

Your email address will not be published. Required fields are marked *

this site uses the awesome footnotes Plugin