From: Alexander Senier <mail@senier.net>
Subject: Re: Mechanisms for proving rules in .rlu files
Date: Fri, 17 Aug 2012 23:37:59 +0200
Date: 2012-08-17T23:37:59+02:00 [thread overview]
Message-ID: <20120817233759.43de8cad@t400> (raw)
In-Reply-To: 4365f56f-d4d3-440b-87bb-5cfe868608f5@googlegroups.com
On Fri, 17 Aug 2012 13:39:47 -0700 (PDT)
Ben Hocking <benjaminhocking@gmail.com> wrote:
> What mechanisms do others use for proving user-defined rules?
We do not prove user-defined rules, but work on the SIV (or VCG) files
directly, using the HOL-SPARK verification environment [1] of Isabelle.
Regards
Alex
[1]
http://isabelle.in.tum.de/library/HOL/HOL-Word/HOL-SPARK/Manual/document.pdf
next prev parent reply other threads:[~2012-08-17 21:38 UTC|newest]
Thread overview: 3+ messages / expand[flat|nested] mbox.gz Atom feed top
2012-08-17 20:39 Mechanisms for proving rules in .rlu files Ben Hocking
2012-08-17 21:37 ` Alexander Senier [this message]
2012-08-19 16:33 ` Phil Thornley
replies disabled
This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox