GamaSlicer : an online laboratory for program verification and analysis

• Autor(es): Cruz, Daniela da ; Henriques, Pedro Rangel ; Pinto, Jorge Sousa
• Data: 2010
• Identificador Persistente: http://hdl.handle.net/1822/13274
• Origem: RepositóriUM - Universidade do Minho
• Assunto(s): Program slicing; Verification conditions; Program visualization
• Tipo de Documento: Artigo
• Idioma: Inglês

Descrição

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. 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.