We concentrate on automatic addition of UNITY properties unless, stable, invariant, and leads-to to programs. We formally define the problem of adding UNITY properties to programs while preserving thenexisting properties. For cases where one simultaneously adds a single leads-to property along with a conjunction of unless, stable, and invariant properties to an existing program, we present a sound and complete algorithm with polynomial time complexity (in program state space). However, for cases where one simultaneously adds two leads-to properties to a program, we present a somewhat unexpected result that such addition is NP-complete. Therefore, in general, adding one leads-to property is significantly easier than adding two (or more) leads-to properties. © Springer-Verlag Berlin Heidelberg 2006.
CITATION STYLE
Ebnenasir, A., Kulkarni, S. S., & Bonakdarpour, B. (2006). Revising UNITY programs: Possibilities and limitations. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 3974 LNCS, pp. 275–290). https://doi.org/10.1007/11795490_22
Mendeley helps you to discover research relevant for your work.