From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: Received: from mail2-relais-roc.national.inria.fr (mail2-relais-roc.national.inria.fr [192.134.164.83]) by sympa.inria.fr (Postfix) with ESMTPS id 0CC357EE4B for ; Tue, 8 Oct 2013 17:30:33 +0200 (CEST) Received-SPF: None (mail2-smtp-roc.national.inria.fr: no sender authenticity information available from domain of gabriel.scherer@gmail.com) identity=pra; client-ip=209.85.214.44; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="gabriel.scherer@gmail.com"; x-sender="gabriel.scherer@gmail.com"; x-conformance=sidf_compatible Received-SPF: Pass (mail2-smtp-roc.national.inria.fr: domain of gabriel.scherer@gmail.com designates 209.85.214.44 as permitted sender) identity=mailfrom; client-ip=209.85.214.44; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="gabriel.scherer@gmail.com"; x-sender="gabriel.scherer@gmail.com"; x-conformance=sidf_compatible; x-record-type="v=spf1" Received-SPF: None (mail2-smtp-roc.national.inria.fr: no sender authenticity information available from domain of postmaster@mail-bk0-f44.google.com) identity=helo; client-ip=209.85.214.44; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="gabriel.scherer@gmail.com"; x-sender="postmaster@mail-bk0-f44.google.com"; x-conformance=sidf_compatible X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: AjkBAOAjVFLRVdYsm2dsb2JhbABZFoMpUq5MkleBFwgWDgEBAQEBBgsLCRQogiUBAQMCQAEbEgsBAwwGBQsDCg0hIQEBEQEFAQoSBhMSh2EBAw8MnB2MU4MKhB4KGScDCmSJAQEFDIxLgReBVAeEIwOUJIF0gWmBL4sbg0sYKYRQOg X-IPAS-Result: AjkBAOAjVFLRVdYsm2dsb2JhbABZFoMpUq5MkleBFwgWDgEBAQEBBgsLCRQogiUBAQMCQAEbEgsBAwwGBQsDCg0hIQEBEQEFAQoSBhMSh2EBAw8MnB2MU4MKhB4KGScDCmSJAQEFDIxLgReBVAeEIwOUJIF0gWmBL4sbg0sYKYRQOg X-IronPort-AV: E=Sophos;i="4.90,1057,1371074400"; d="scan'208";a="36096626" Received: from mail-bk0-f44.google.com ([209.85.214.44]) by mail2-smtp-roc.national.inria.fr with ESMTP/TLS/RC4-SHA; 08 Oct 2013 17:30:31 +0200 Received: by mail-bk0-f44.google.com with SMTP id mz10so3314033bkb.17 for ; Tue, 08 Oct 2013 08:30:32 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20120113; h=mime-version:in-reply-to:references:from:date:message-id:subject:to :cc:content-type; bh=K4gaw3+wEJYK8TqEOlSca7h58865Dn7ucw4fYYN9VZ8=; b=FDb8asJvp9dvEikZ0Bmb7tPAOQU4rVPfLWRNtNTyXNHlMaWZuhVNXUf74RxAPS9oz5 Nrh1dVi4IZSnFN3FtmNY14+75NCZK7hbktdDDMx0hz8mCTUVp0Idnyi8fmsA09ge66Uz TjHpRuZKN3N6LGjDSa34z3+ZaAUvXLJAmkE7KoG7XcPg/1pyEgbb5TIu7kurYPRGbrOr bV/B67c3q65C6p/r75wVk42AdC2+s8+Ef/RpD0VCjePzEpX6zlRBT/rmZsUkSYdmTyVv 9lWNIBvbn5yyY5HiGtb9ed1ieLzpiOc+r04sjd73d1XF7oi5YIoO1uwVK5ttVdoWvAsI gRkg== X-Received: by 10.205.65.17 with SMTP id xk17mr2100082bkb.19.1381246232005; Tue, 08 Oct 2013 08:30:32 -0700 (PDT) MIME-Version: 1.0 Received: by 10.204.236.193 with HTTP; Tue, 8 Oct 2013 08:29:50 -0700 (PDT) In-Reply-To: <20131008152753.43eb5a2f@jakobro-VirtualBox> References: <37811b09.6ff.141695f3e3c.Coremail.syshen@nudt.edu.cn> <20130929165650.34da2e99@oberon> <1d5abd41.7b2.1416c429ca3.Coremail.syshen@nudt.edu.cn> <20130930145358.GF8693@frosties> <20131008152753.43eb5a2f@jakobro-VirtualBox> From: Gabriel Scherer Date: Tue, 8 Oct 2013 17:29:50 +0200 Message-ID: To: Robert Jakob Cc: caml users Content-Type: text/plain; charset=ISO-8859-1 Subject: Re: [Caml-list] equivalent checking of ocaml program? 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 wrote: > On Mon, 30 Sep 2013 17:49:11 +0200 > Gabriel Scherer 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