| Hello, Spin stands apart from the other systems that you mention in that it is a model checker whose language is deliberately restricted so that verification becomes efficient. In fact, Spin translates a Promela model into a C program that contains a model checker that is specific to that particular model. Concerning proof assistants such as Agda, Coq, HOL, Isabelle, NuPRL, PVS etc., they differ according to their logical foundations (and you'll find strong opinions in the various sub-communities on why some logic is more appropriate than another one), but for all practical purposes I personally do not think that differences in expressiveness are relevant. You will be able to express any system specification, correctness property, and proof, or even your favorite mathematical theory, in any of these systems. Of course, each system may have its idiosyncrasies and you may feel more or less comfortable with how the concepts you are interested in are expressed. After all, the most powerful system is of no use to you if you feel that you constantly need to work against your intuitions for expressing them in the language of the system. For advanced use, the existence of a standard library of theories (definitions and proofs) relevant for your formalization will become a decisive factor. Other dimensions are the degree of proof automation, maturity of the system, trustworthiness of the kernel, IDE support etc. A somewhat dated, but still relevant comparison was published as an LNCS volume by Freek Wiedijk in 2007 [1] and is worth reading. Regards, Stephan [1] http://www.cs.ru.nl/~freek/comparison/, see also https://dblp.uni-trier.de/db/conf/tphol/lncs3600.html and http://www.cs.ru.nl/~freek/comparison/comparison.pdf.
|