From: Florian Weimer <fw@deneb.enyo.de>
Subject: Re: SPARK and integer arithmetic
Date: Mon, 03 Oct 2016 17:39:08 +0200
Date: 2016-10-03T17:39:08+02:00 [thread overview]
Message-ID: <87mvil1lyb.fsf@mid.deneb.enyo.de> (raw)
In-Reply-To: 0d01480e-ddd4-4746-99ad-4f1e6adab436@googlegroups.com
* Mark Lorenzen:
> 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.
Indeed, but they do not cover this particular issue well (proving
correctness of wraparound arithmetic).
prev parent reply other threads:[~2016-10-03 15:39 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
2016-10-03 15:39 ` Florian Weimer [this message]
replies disabled
This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox