Re: [Caml-list] equivalent checking of ocaml program?

[Gabriel Scherer <gabriel.scherer@gmail.com>]

Shortly after writing my email, I found out that Ong had co-written a
recent article (CAV'12) on using those techniques precisely for
equivalence checking:

  Hector: An Equivalence Checker for a Higher-Order Fragment of ML
  David Hopkins' Andrzej S. Murawski and C.-H Luke Ong
  2012
  http://www.cs.ox.ac.uk/files/4786/cav12.pdf

They restrict themselves to a order-bounded fragment of higher-order
function types (and only allow ground reference types) suggested by
game-semantics considerations, on which equivalence checking is
decidable, and leave extensions to more complex settings where
equivalence becomes indecidable to future work.
You probably know more about this than I do (this is not my field at
all), but my understanding is that whether the problems are decidable
or not is not an actual concern with model checking, as even in
decidable cases the tools most often run out of time; actual
feasability on concrete examples seems the most useful way to evaluate
those, so I don't think going to undecidable fragments would be a
problem in principle. Of course, the more complex the fragment, the
more expansive the computations.

On Tue, Oct 8, 2013 at 3:27 PM, Robert Jakob <rj@robertjakob.de> wrote:
> On Mon, 30 Sep 2013 17:49:11 +0200
> Gabriel Scherer <gabriel.scherer@gmail.com> wrote:
>
>> This thread may be a good opportunity to advertize for some work on
>> static program verification that has been applied to OCaml (sadly, it
>> is actually quite rare to see program verification efforts for
>> functional programming languages, in large part because funding
>> bodies and reviewers appreciate applications to mainstream language
>> with larger codebases). I am aware of the following, feel free to add
>> more suggestions:
>> - MoCHi http://www-kb.is.s.u-tokyo.ac.jp/~ryosuke/mochi/
>>   Based on foundational work on model-checking of higher-order
>> programs by Ong, Kobayashi and others (see the citations of the
>> papers on the webpage), MoCHi can work with a subset of OCaml. It is
>> not ready to handle real-world programs, both in term of verification
>> time and the ocaml feature it understands, but going in the right
>> direction -- and the underlying tools are rapidly improving, see e.g.
>> the recent work on C-SHORe
> The approaches by Ong, Kobayashi, Broadbent et al. work on higher-order
> recursion schemes (HORS) to represent output/states of functional
> programs. Yet, it is not known if the equivalence of two HORS is
> decidable. So this might be applicable to deciding the equivalency of
> ocaml programs (wrt. outputs/state), but it is not clear.
>
> r.
>
> --
> Caml-list mailing list.  Subscription management and archives:
> https://sympa.inria.fr/sympa/arc/caml-list
> Beginner's list: http://groups.yahoo.com/group/ocaml_beginners
> Bug reports: http://caml.inria.fr/bin/caml-bugs