Automatic Verification

Citation: Marc Spielmann, "Automatic Verification of Abstract State Machines", in N. Halbwachs and D. Peled, eds., Proceedings of the 11th International Conference on Computer-Aided Verification (CAV'99), Springer LNCS 1633, 1999, 431--442.
Summary: A class of restricted ASM programs is introduced, along with a PSPACE algorithm for verifying the correctness of properties of such programs. Limits on verifiability of generalizations of this class are also discussed.
Subjects: Mechanical Verification
Download: From the author's web page in PostScript.
Notes: See also later work by the author.