From: Mark Lorenzen <mark.lorenzen@gmail.com>
Subject: Re: SPARK and integer arithmetic
Date: Mon, 3 Oct 2016 03:09:08 -0700 (PDT)
Date: 2016-10-03T03:09:08-07:00 [thread overview]
Message-ID: <0d01480e-ddd4-4746-99ad-4f1e6adab436@googlegroups.com> (raw)
In-Reply-To: <87poo1a57p.fsf@mid.deneb.enyo.de>
On Sunday, September 18, 2016 at 12:10:36 PM UTC+2, Florian Weimer wrote:
> I'm trying to find out the capabilities of the SPARK when it comes to
> verifying the correctness of integer arithmetic (and absence of
> constraint errors).
>
> The Barnes book (in the 2006 edition) is not really that helpful. I'm
> not even using the current SPARK tools, but the SPARK 2012 GPL
> edition, but the command line options still are different from those
> described in the book.
I would really like to advice you to use the latest SPARK GPL toolset and the SPARK book
https://www.amazon.co.uk/Building-High-Integrity-Applications-Spark/dp/1107656842/ref=sr_1_1?ie=UTF8&qid=1475489273&sr=8-1&keywords=high+integrity+applications
The new SPARK language and toolset are major improvements over the old ones.
Regards,
Mark L
next prev parent reply other threads:[~2016-10-03 10:09 UTC|newest]
Thread overview: 9+ messages / expand[flat|nested] mbox.gz Atom feed top
2016-09-18 10:10 SPARK and integer arithmetic Florian Weimer
2016-09-18 15:37 ` Simon Wright
2016-09-18 18:01 ` Florian Weimer
2016-09-18 19:33 ` Paul Rubin
2016-09-18 19:49 ` Florian Weimer
2016-09-19 7:14 ` Paul Rubin
2017-08-09 19:47 ` moy
2016-10-03 10:09 ` Mark Lorenzen [this message]
2016-10-03 15:39 ` Florian Weimer
replies disabled
This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox