This paper presents the formalization of an algorithm for slicing Java event spaces in PVS. In short, Java event spaces describe how multi-threaded Java programs operate in memory. We show that Java event spaces can be sliced following an algorithm introduced in previous work and still preserve properties in a subset of CTL. The formalization and proof presented in this paper can be extended to other state-space reduction techniques as long as some sufficient conditions are fulfilled. © Springer-Verlag Berlin Heidelberg 2005.
CITATION STYLE
Cataño, N. (2005). Formal modeling of a slicing algorithm for Java event spaces in PVS. In Lecture Notes in Computer Science (Vol. 3603, pp. 82–97). Springer Verlag. https://doi.org/10.1007/11541868_6
Mendeley helps you to discover research relevant for your work.