In this paper we present an approach for developing adaptable software applications. The problem we are facing is that of a (possibly mobile) user who wants to download and execute an application from a remote server. The user’s hosting device can be of different kinds (laptops, personal digital assistants, cellular phones, communicators, etc.) with specific hardware and software capabilities. The problem is to be able to decide whether the user’s current device characteristics are compatible with the application requirements in order to prevent execution failures. In the negative case we want to identify the reasons that determined the incompatibility and perform an automatic adaptation of the application, so that it can match the user’s device capabilities. We adopt a declarative approach: we provide each device with a declarative description of its characteristics and, possibly, context constraints. Inspired by Proof Carrying Code (PCC), we use first-order logic formulae t...