Revising UNITY Programs: Possibilities and
Limitations
Ali Ebnenasir, Sandeep S. Kulkarni, and Borzoo Bonakdarpour
Abstract
We concentrate on automatic addition of UNITY properties
{\sf unless, stable, invariant}, and {\sf leads-to} to programs. We formally define the problem of adding UNITY properties to programs
while preserving their existing properties. For the cases where one simultaneously adds a single {\sf leads-to} property along with a
conjunction of {\sf unless, stable}, and {\sf invariant} properties to an existing program, we present a sound and complete algorithm
with polynomial time complexity (in program state space). However, for the cases where one adds more than one {\sf leads-to} properties
to a program, we present a somewhat unexpected result that such addition is NP-complete. Therefore, in general, adding one {\sf
leads-to} property is significantly easier than adding two (or more) {\sf leads-to} properties.
Paper:
Return to the publication list
Return to the Sandeep's home page