Paper Info
Title
GamaSlicer: an online laboratory for program verification and analysis
Abstract
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 (precondition-based, postcondition-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.
Year
DOI
Venue
2010
10.1145/1868281.1868284
LDTA
Keywords
Field
DocType
software component,formal verification,program slicing,weakest precondition
Program slicing,Functional verification,Programming language,Intelligent verification,Computer science,Runtime verification,Verification,High-level verification,Software verification,Formal verification
Conference
Citations 
PageRank 
References 
4
0.52
12
Authors
3
Name
Order
Citations
PageRank
Daniela Carneiro da Cruz112613.69
Pedro Rangel Henriques227757.91
Jorge Sousa Pinto316023.19