By the same authors

Efficient re-resolution of SMT specifications for evolving software architectures

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Published copy (DOI)



Publication details

Title of host publicationQoSA 2014
DatePublished - 1 Jan 2014
Number of pages10
PublisherAssociation for Computing Machinery (ACM)
Original languageEnglish
ISBN (Print)9781450325769


We present a generic method for the effcient constraint re- resolution of a component-based software architecture after changes such as addition, removal and modification of components. Given a formal description of an evolving system as a constraint-specification problem, our method identifies and executes the re-resolution steps required to verify the system's compliance with constraints after each change. At each step, satisfiability modulo theory (SMT) techniques determine the satisfiability of component constraints expressed as logical formulae over suitably chosen theories of arithmetic, reusing results obtained in previous steps. We illustrate the application of the approach on a constraint- satisfaction problem arising from cloud-deployed software services. The incremental method is shown to re-resolve sys- tem constraints in a fraction of the time taken by standard SMT resolution.

    Research areas

  • Domain-Specific Languages, Incremental Re-resolution, Sat-isfiability Modulo Theory


Discover related content

Find related publications, people, projects, datasets and more using interactive charts.

View graph of relations