Please use this identifier to cite or link to this item:
Title: ConSUS: A light-weight program conditioner
Authors: Danicic, S
Daoudi, M
Fox, CJ
Harman, M
Hierons, RM
Howroyd, J
Ourabya, L
Ward, M
Keywords: Program conditioning;Slicing;Program transformation;Decision procedures
Issue Date: 2005
Publisher: Elsevier
Citation: Journal of Systems and Software, 77(3): 241-262, Jan 2005
Abstract: Program conditioning consists of identifying and removing a set of statements which cannot be executed when a condition of interest holds at some point in a program. It has been applied to problems in maintenance, testing, re-use and re-engineering. All current approaches to program conditioning rely upon both symbolic execution and reasoning about symbolic predicates. The reasoning can be performed by a ‘heavy duty’ theorem prover but this may impose unrealistic performance constraints. This paper reports on a lightweight approach to theorem proving using the FermaT Simplify decision procedure. This is used as a component to ConSUS, a program conditioning system for the Wide Spectrum Language WSL. The paper describes the symbolic execution algorithm used by ConSUS, which prunes as it conditions. The paper also provides empirical evidence that conditioning produces a significant reduction in program size and, although exponential in the worst case, the conditioning system has low degree polynomial behaviour in many cases, thereby making it scalable to unit level applications of program conditioning.
Appears in Collections:Computer Science
Dept of Computer Science Research Papers
Software Engineering (B-SERC)

Files in This Item:
File Description SizeFormat 
ConSUS 2005.pdf575.63 kBAdobe PDFView/Open

Items in BURA are protected by copyright, with all rights reserved, unless otherwise indicated.