Email Gateway (Aug 22 2022 at 10:26): Email Gateway (Aug 22 2022 at 10:26):From: Andrei Popescu <a.popescu@mdx.ac.uk>
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.
Email Gateway (Aug 22 2022 at 10:26):From: Magnus Myreen <mom22@cam.ac.uk>
Dear Andrei,
Email Gateway (Aug 22 2022 at 10:26):From: Gerwin Klein <Gerwin.Klein@nicta.com.au>
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
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.
Last updated: Nov 21 2024 at 12:39 UTC