Verification of imperative programs means reasoning about modifications of a program state. So proper representation of state spaces is crucial for the usability of a corresponding verification environment. In this paper we discuss various existing state space models under different aspects like strong typing, modularity and scalability. We also propose a variant based on the locale infrastructure of Isabelle. Thus we manage to combine the advantages of previous formulations (without suffering from their disadvantages), and gain extra flexibility in composing state space components (inherited from the modularity of locales).

Online Copy

Available as PDF-File

BibTeX Entry

@InProceedings{Schirmer:SSV09-161, author = "Norbert Schirmer and Makarius Wenzel", title = "State Spaces -- {The} Locale Way", pages = "161--179", ee = "http://dx.doi.org/10.1016/j.entcs.2009.09.065", booktitle = "4th International Workshop on Systems Software Verification (SSV 2009)", year = "2009", publisher = "Elsevier Science B.V.", series = "Electronic Notes in Theoretical Computer Science", volume = "254", }