PORTO @ 
Archivio Istituzionale della Ricerca
IRIS è la soluzione IT che facilita la raccolta e la gestione dei dati relativi alle attività e ai prodotti della ricerca. Fornisce a ricercatori, amministratori e valutatori gli strumenti per monitorare i risultati della ricerca, aumentarne la visibilità e allocare in modo efficace le risorse disponibili.
EnglishGarbage 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 R.. - 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].
| Titolo: | Using Garbage Collection in Model Checking | |
| Autori: | ||
| Data di pubblicazione: | 2000 | |
| Rivista: | ||
| Abstract: | Garbage collection techniques have become common-place in actual programming environments, helpin...g 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. | |
| ISBN: | 3540410309 | |
| Appare nelle tipologie: | 4.1 Contributo in Atti di convegno |
File in questo prodotto:
| File | Descrizione | Tipologia | Licenza | |
|---|---|---|---|---|
| 1418131.pdf | 2. Post-print / Author's Accepted Manuscript | Non Pubblico - Accesso privato/ristretto | Administrator Richiedi una copia |
http://hdl.handle.net/11583/1418131
Copyright © 2022