Home

PVS goes open source

The PVS Specification and Verification System from SRI is being released as open source.

Also coming with version 4.0 is the PVS wiki.

By Ehud Lamm at 2006-12-06 12:18 | General | other blogs | 6957 reads

Comment viewing options

Select your preferred way to display the comments and click "Save settings" to activate your changes.

PVS, ACL2, Coq ...

As an autodidact in PL, I have much interest in formal methods and program verification, but very little experience or context for their theoretical bases and practical applications. Could someone provide me with some insight into PVS, ACL2, Coq, and other such theorem proving systems? I am particularly interested in comparisons of their design choices, and in their strengths when applied in industrial settings.

By steven_h at Wed, 2006-12-06 20:57 | login or register to post comments

Seventeen Proof Assistants

Freek Wiedijk lists seventeen proof assistants and their proofs of the irrationality of sqrt(2). The accompanying consumer test succinctly presents various aspects of the proof assistants. In section 1.3 on related work, you'll find references to other comparisons of proof assistants applied in computer science.

By Ronny Wichers Schreur at Fri, 2006-12-08 21:37 | login or register to post comments

One categorisation of these

One categorisation of these systems is in terms of the expressiveness of their logics. In order from least expressive to most, I'd order some of the well-known systems as follows: ACL2, HOL, Isabelle/HOL, (PVS & Coq).

All of these systems are capable of mechanising big chunks of mathematics and logic. All have been used in industrial applications. I'd say ACL2 has probably been most used in this way, particularly because of its amazing support for efficient execution of logical models.

Isabelle/HOL, HOL and Coq are all implemented in ML and follow the "LCF approach" of using the ML type system to implement theorems as an abstract datatype. In this way, the programming language plus what you'd hope would be a small kernel of fundamental operations are used to guarantee soundness of the rest of the system.

By michaeln at Thu, 2006-12-07 23:51 | login or register to post comments

Applications in medical systems?

Thank you for your comments and links.

Having read about the famous Therac-25 incidents, I have always wondered what steps the software engineers have taken to improve the reliability of critical software. I understand that large portions of safety controls are implemented as hardware locks, but do they also apply formal methods in medical systems?

By steven_h at Mon, 2006-12-11 13:35 | login or register to post comments

Z

I'm not sure about PVS, but Z has definitely seen some use in the medical domain. Jonathan Jacky has made excerpts of a Z spec for a radiation therapy machine available on his website. Jacky is the author of the excellent The Way of Z, which is one of the more accessible and practically oriented books on formal methods that I've seen, and which builds on his experiences working with Z on the development of various medical devices.

By Allan McInnes at Tue, 2006-12-12 04:36 | login or register to post comments