@conference {1622,
	title = {GamaSlicer: an online laboratory for program verification and analysis},
	booktitle = {Proceedings of the of the Tenth Workshop on Language Descriptions, Tools and Applications - LDTA},
	year = {2010},
	month = {March},
	address = {Paphos, Cyprus},
	abstract = {<p>In this paper we present the GamaSlicer tool, which is primarily a semantics-based program slicer that also offers formal verification (generation of verification conditions) and program visualization functionality. The tool allows users to obtain slices using a number of different families of slicing algorithms (\precond-based, \postcond-based, and specification-based), from a correct software component annotated with pre and postconditions (contracts written in JML-annotated Java). Each family in turn contains algorithms of different precision (with more precise algorithms being asymptotically slower). A novelty of our work at the theoretical level is the inclusion of a new, much more effective algorithm for specification-based slicing, and in fact other current work at this level is being progressively incorporated in the tool.</p>
<p>The tool also generates (in a step-by-step fashion) a set of verification conditions (as formulas written in the SMT-lib language, which enables the use of different automatic SMT provers). This allows to establish the initial correctness of the code with respect to their contracts.</p>
},
	attachments = {https://haslab.uminho.pt/sites/default/files/jsp/files/ldta2010gamaslicervf.pdf},
	author = {Jorge Sousa Pinto and Pedro Rangel Henriques and Daniela Cruz}
}