GamaSlicer : an online laboratory for program verification and analysis

• Author(s): Cruz, Daniela da ; Henriques, Pedro Rangel ; Pinto, Jorge Sousa
• Date: 2010
• Persistent ID: http://hdl.handle.net/1822/13274
• Origin: RepositóriUM - Universidade do Minho
• Subject(s): Program slicing; Verification conditions; Program visualization
• Document Type: Article
• Language: English

Description

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.