Spin Model Checker, The: Primer and Reference Manual

Appendix B. The Great Debates

	“It is not necessary to understand things in order to argue about them.”
	--(Pierre Augustin Caron de Beaumarchais, 1732–1799)

Quite a few issues in formal verification have sparked heated debates over the years, without ever coming to a clear resolution. Perhaps the first such issue came up when temporal logic was first being explored, in the late seventies, as a suitable formalism for reasoning about concurrent systems. The issue was whether it was better to use a branching-time or a linear-time logic. Much later, the debate was between symbolic or explicit verification methods. Many of these issues directly relate to design decisions that have to be made in any verifier, including SPIN. We discuss the more important ...