Danicic, Sebastian; Daoudi, Mohammed; Fox, Chris; Harman, Mark; Hierons, Robert; Howroyd, John; Ouarbya, Lahcen and Ward, Martin. 2005. ConSUS: A lightweight program conditioner. Journal of Systems and Software, 77(3), pp. 241-262. ISSN 0164-1212 [Article]

No full text available

Abstract or Description

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.

Item Type:	Article
Identification Number (DOI):	https://doi.org/10.1016/j.jss.2004.03.034
Departments, Centres and Research Units:	Computing
Dates:	Date Event 2005 Published
Item ID:	15215
Date Deposited:	02 Dec 2015 13:10
Last Modified:	20 Jun 2017 11:22
Peer Reviewed:	Yes, this version has been peer-reviewed.
URI:	https://research.gold.ac.uk/id/eprint/15215

Edit Record (login required)