Re: [isabelle] large system verification



I completely agree with Magnus.

There are also examples of larger systems being developed in Dafny, which is more towards (1), although in this case Dafny *is* the programming language, so itâs really more a mix of the two.

Ultimately I think a mix will give you the highest productivity at the moment, but (1) will only work with non-verification-experts if the language you are using in the proof assistant is a full programming language by itself.

Cheers,
Gerwin

> On 29.06.2015, at 23:23, Magnus Myreen <mom22 at cam.ac.uk> wrote:
>
> Dear Andrei,
>
>> (1) Develop (the core of) the system in the proof assistant and
>> extract code to a programming language.
>>
>> (2) Develop the system in the programming language directly and
>> extract a model to be verified in the proof assistant.
>>
>> My 5 cents here are that, while (1) can be convenient for getting
>> things done reliably, (2) is more realistic regarding the prospect
>> of collaborating with developers without verification expertise, and
>> ultimately with the industry.
>
> I think you are right. However, I'd like to add that it is very
> difficult (if not practically impossible) to verify functional
> properties of large systems that were developed *without* verification
> as a goal from the start. The reason is that the verifier has to guess
> what the programmers were thinking. The resulting reverse-engineered
> invariants tend to become messier than invariants for clean
> verification-friendly programs. Messier invariants cause pain in
> verification proofs.
>
> There is a danger with approach (2): seemingly small changes to the
> source code can have a significant impact on the carefully developed
> proofs. Proofs that once worked can easily get far out of step with
> the continuously developed source code.
>
> As far as I know, the most noteworthy example in the second category
> (2) is the OS verification done at NICTA. The OS that they verified
> was developed with verification in mind from the start, see:
> http://ssrg.nicta.com.au/projects/TS/l4.verified/
>
> Another successful application of approach (2) is the hardware
> verification that's done at Centaur Technology using ACL2, see:
> https://www.cs.utexas.edu/users/hunt/talks/itp-2011.pdf
>
> I would also like to add that it is possible and useful to mix (1) and
> (2), e.g. use performance-tuned code through method (2) in a context
> that in general uses method (1). I've done this in various projects,
> see http://www.cl.cam.ac.uk/~mom22/stacks.html for pointers.
>
> Kind regards,
> Magnus
>
> On 29 June 2015 at 13:44, Andrei Popescu <a.popescu at mdx.ac.uk> wrote:
>> Dear (large) system verification experts,
>>
>> I am surveying the literature on this topic and I identified two approaches to verifying software systems in a proof assistant with acquiring solid adequacy guarantees:
>>
>> (1) Develop (the core of) the system in the proof assistant and extract code to a programming language.
>>
>> (2) Develop the system in the programming language directly and extract a model to be verified in the proof assistant.
>>
>> My 5 cents here are that, while (1) can be convenient for getting things done reliably, (2) is more realistic regarding the prospect of collaborating with developers without verification expertise, and ultimately with the industry. Or can we hope that in the near future "the industry" will embrace the initial development of systems in a proof assistant?
>>
>> Of course, there are nuances here, e.g., is one aiming at verifying a large monolithic system or an open-ended class of systems (the latter being closer to the goal of a program verification framework)?
>> I know there have been successful projects in both categories and I would be interested to hear opinions and examples concerning these two approaches.
>>
>> (This question is related to the thread "proof engineering for program verification", but has a slightly different scope.)
>>
>> Many thanks in advance,
>>  Andrei
>>
>>
>>
>> ---------------------------------------------------------------------------
>>
>>
>> Please note that Middlesex University's preferred way of receiving all correspondence is via email in line with our Environmental Policy. All incoming post to Middlesex University is opened and scanned by our digital document handler, CDS, and then emailed to the recipient.
>>
>> If you do not want your correspondence to Middlesex University processed in this way please email the recipient directly. Parcels, couriered items and recorded delivery items will not be opened or scanned by CDS.  There are items which are "exceptions" which will be opened by CDS but will not be scanned a full list of these can be obtained by contacting the University.
>>
>>
>


________________________________

The information in this e-mail may be confidential and subject to legal professional privilege and/or copyright. National ICT Australia Limited accepts no liability for any damage caused by this email or its attachments.


This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.