[ROU04c] Slicing concurrent programs using the Quasar tool

Conférence Internationale avec comité de lecture : ICSSEA'04, January 2004,

Auteurs: P. Rousseau

motcle:

Résumé: Systems requiring a high degree of reliability and safety have to support concurrents process. However, the indeterminism related to concurrency is a barrier to their use. Quasar is a tool designed to solve this problem. Quasar proves, in a formal way, properties on concurrent programs using a formal model, obtained by automatic translation of the source code. However, to avoid the modeling of the complete source code, we eliminate from it the statements that don't have any effect on the property to validate. This is called program slicing. It is the first step of the process followed by Quasar to validate a property. Slicing can be used independently because the slice obtained by this method has the same behavior as the original source code from the point of view of the studied property. In this article, we give a short outline of Quasar as well as general principles of program slicing and its use. Then we study the techniques used by Quasar to carry it out.

BibTeX

@inproceedings {
	ROU04c,
	title	=	"{Slicing concurrent programs using the Quasar tool}",
	author	=	" P. Rousseau ",
	booktitle	=	"{ICSSEA'04}",
	year	=	2004,
	month	=	"January",
}