Garbage collection techniques have become common-place in actual programming environments, helping programmers to avoid memory fragmentation and invalid referencing problems. In order to efficiently model check programs that use garbage collection, similar functionalities have to be embedded in model checkers. This paper focuses on the implementation of two classic garbage collection algorithms in dSPIN, an extension of the model checker SPIN which supports dynamic memory management. Experiments carried out show that, besides making a large class of programs tractable, garbage collection can also be a mean to reduce the number of states generated by our model checking tool.
Using Garbage Collection in Model Checking / Iosif, R.; Sisto, Riccardo. - 1885:(2000), pp. 20-33. (Intervento presentato al convegno 7th International SPIN Workshop tenutosi a Stanford, CA (USA) nel August 30 - September 1, 2000) [10.1007/10722468_2].
Using Garbage Collection in Model Checking
SISTO, Riccardo
2000
Abstract
Garbage collection techniques have become common-place in actual programming environments, helping programmers to avoid memory fragmentation and invalid referencing problems. In order to efficiently model check programs that use garbage collection, similar functionalities have to be embedded in model checkers. This paper focuses on the implementation of two classic garbage collection algorithms in dSPIN, an extension of the model checker SPIN which supports dynamic memory management. Experiments carried out show that, besides making a large class of programs tractable, garbage collection can also be a mean to reduce the number of states generated by our model checking tool.Pubblicazioni consigliate
I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.
https://hdl.handle.net/11583/1418131
Attenzione
Attenzione! I dati visualizzati non sono stati sottoposti a validazione da parte dell'ateneo