From mboxrd@z Thu Jan 1 00:00:00 1970 X-Spam-Checker-Version: SpamAssassin 3.4.4 (2020-01-24) on polar.synack.me X-Spam-Level: X-Spam-Status: No, score=-1.9 required=5.0 tests=BAYES_00 autolearn=ham autolearn_force=no version=3.4.4 X-Google-Thread: 103376,5bc4be576204aa20 X-Google-Attributes: gid103376,public X-Google-Language: ENGLISH,ASCII-7-bit Newsgroups: comp.lang.ada Subject: Re: Buffer overflow Article - CACM References: <3tr6hiFu7jr6U1@individual.net> <1133252164.539307.165050@g49g2000cwa.googlegroups.com> From: Brian May Date: Thu, 01 Dec 2005 08:21:28 +1100 Message-ID: User-Agent: Gnus/5.1007 (Gnus v5.10.7) Emacs/21.4 (gnu/linux) Cancel-Lock: sha1:ne/Kc55vegzNgfZp7PY25RQv/Ls= MIME-Version: 1.0 Content-Type: text/plain; charset=us-ascii NNTP-Posting-Host: snoopy.microcomaustralia.com.au X-Trace: news.melbourne.pipenetworks.com 1133385688 202.173.153.89 (1 Dec 2005 07:21:28 +1000) X-Complaints-To: abuse@pipenetworks.com X-Abuse-Info: Please forward all headers to enable your complaint to be properly processed. Path: g2news1.google.com!news4.google.com!news.glorb.com!newsfeeds.ihug.co.nz!ihug.co.nz!news.xtra.co.nz!news-south.connect.com.au!duster.adelaide.on.net!news.melbourne.pipenetworks.com!not-for-mail Xref: g2news1.google.com comp.lang.ada:6689 Date: 2005-12-01T08:21:28+11:00 List-Id: >>>>> "Harald" == Harald Korneliussen writes: Harald> I though that with SPARK, you have to write your program Harald> with no moving parts (or dynamic data structures) and then Harald> supply a suite of proofs, which may be quite hard, even Harald> with the assistant? How often is this practical? Another issue with SPARK is that it appears to be non-free software (unless you can meet the criteria for academic use where you can use it for 0 cost), and no prices are given online the website. This makes me suspect it will be out of reach for average free software authors, and most of the software I use falls into this category. On the other hand, please correct me if I am wrong... -- Brian May