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.
2000
3540410309
File in questo prodotto:
Non ci sono file associati a questo prodotto.
Pubblicazioni consigliate

I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.

Utilizza questo identificativo per citare o creare un link a questo documento: https://hdl.handle.net/11583/1418131
 Attenzione

Attenzione! I dati visualizzati non sono stati sottoposti a validazione da parte dell'ateneo