Return-Path: <haskell-bounces@haskell.org>
Delivered-To: pop1021@pizza-005.intraserver.de
Received: (qmail 1818 invoked by uid 5018); 4 Nov 2005 16:10:56 -0000
Delivered-To: vdom5018-wolfgang@jeltsch.net
Received: (qmail 1815 invoked from network); 4 Nov 2005 16:10:55 -0000
Received: from bugs.haskell.org (HELO www.haskell.org) (128.36.229.215)
	by pizza-005.intraserver.de with SMTP; 4 Nov 2005 16:10:55 -0000
Received: from haskell.cs.yale.edu (localhost.localdomain [127.0.0.1])
	by www.haskell.org (Postfix) with ESMTP
	id C956E3242D3; Fri,  4 Nov 2005 10:50:21 -0500 (EST)
X-Original-To: haskell@haskell.org
Delivered-To: haskell@haskell.org
Received: from ciao.gmane.org (main.gmane.org [80.91.229.2])
	by www.haskell.org (Postfix) with ESMTP id 20D2E3242D3
	for <haskell@haskell.org>; Fri,  4 Nov 2005 10:50:06 -0500 (EST)
Received: from list by ciao.gmane.org with local (Exim 4.43)
	id 1EY46S-0003zE-IL
	for haskell@haskell.org; Fri, 04 Nov 2005 17:07:44 +0100
Received: from 66-90-154-160.dyn.grandenetworks.net ([66.90.154.160])
	by main.gmane.org with esmtp (Gmexim 0.1 (Debian))
	id 1AlnuQ-0007hv-00
	for <haskell@haskell.org>; Fri, 04 Nov 2005 17:07:44 +0100
Received: from nedunuri by 66-90-154-160.dyn.grandenetworks.net with local
	(Gmexim 0.1 (Debian)) id 1AlnuQ-0007hv-00
	for <haskell@haskell.org>; Fri, 04 Nov 2005 17:07:44 +0100
X-Injected-Via-Gmane: http://gmane.org/
To: haskell@haskell.org
From: "Srinivas Nedunuri" <nedunuri@cs.utexas.edu>
Date: Fri, 4 Nov 2005 09:42:07 -0600
Lines: 31
Message-ID: <dkg0pi$hr3$1@sea.gmane.org>
References: <200511041213.04185.wolfgang@jeltsch.net>
X-Complaints-To: usenet@sea.gmane.org
X-Gmane-NNTP-Posting-Host: 66-90-154-160.dyn.grandenetworks.net
X-MSMail-Priority: Normal
X-Newsreader: Microsoft Outlook Express 6.00.2900.2180
X-MimeOLE: Produced By Microsoft MimeOLE V6.00.2900.2180
X-RFC2646: Format=Flowed; Original
Subject: [Haskell] Re: formal verification for functional programming
 languages
X-BeenThere: haskell@haskell.org
X-Mailman-Version: 2.1.5
Precedence: list
Reply-To: Srinivas Nedunuri <nedunuri@cs.utexas.edu>
List-Id: The Haskell Mailing List <haskell.haskell.org>
List-Unsubscribe: <http://www.haskell.org/mailman/listinfo/haskell>,
	<mailto:haskell-request@haskell.org?subject=unsubscribe>
List-Archive: <http://www.haskell.org//pipermail/haskell>
List-Post: <mailto:haskell@haskell.org>
List-Help: <mailto:haskell-request@haskell.org?subject=help>
List-Subscribe: <http://www.haskell.org/mailman/listinfo/haskell>,
	<mailto:haskell-request@haskell.org?subject=subscribe>
Sender: haskell-bounces@haskell.org
Errors-To: haskell-bounces@haskell.org
Content-Type: 
MIME-Version: 1.0

Are you familiar with Hoare and Misra's Verification Grand Challenge? Here 
are a couple of pointers to recent workshops

http://www.csl.sri.com/users/shankar/VGC05/
and
http://vstte.ethz.ch/index.html

FWIW, I personally feel that transforming specifications into programs via 
synthesis or refinement or whatever is going to net you a better return than 
after the fact verification. That's just IMHO. Right now I'm looking at 
different possibilities for specification languages, and I feel that Haskell 
gets you 70-80% of the way there (I think that Hoare himself said something 
along those lines sometime back)

cheers


"Wolfgang Jeltsch" <wolfgang@jeltsch.net> wrote in message 
news:200511041213.04185.wolfgang@jeltsch.net...
> Hello,
>
> where can I find information about formal verification techniques and 
> tools
> for functional programming languages?  Both introductionary texts and 
> current
> research papers etc. are welcome.
>
> Best wishes,
> Wolfgang 



_______________________________________________
Haskell mailing list
Haskell@haskell.org
http://www.haskell.org/mailman/listinfo/haskell