Revising UNITY Programs: Possibilities and Limitations

Ali Ebnenasir, Sandeep S. Kulkarni, and Borzoo Bonakdarpour


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.


Return to the publication list
Return to the Sandeep's home page