A Flexible Framework for Program Evolution and Verification

We propose a flexible framework for modeling of distributed systems, supporting evolution by means of unrestricted modifications in such systems, and with support of verification and re-verification. We focus on the setting of concurrent and object-oriented programs, and consider a core high-level modeling language supporting active, concurrent objects. We show that our framework can deal with verification of software changes that are not possible to verify in comparable frameworks. We demonstrate the approach by variations over a simple example.