We formalize and study business process systems that are centered around "business artifacts", or simply "artifacts". This approach focuses on data records, known as artifacts, that correspond to key businessrelevant objects, and that flow through a business process specified by a set of services. The artifactcentric approach has been introduced by IBM, and has enabled significant improvements to the operations of medium- and large-sized businesses. In this paper, artifacts carry attribute records and internal state relations, that services can consult and update. In addition, services can access an underlying database and can introduce new values from an infinite domain, thus modeling external inputs or partially specified processes described by pre-and-post conditions. The services are associated to the artifacts using declarative, condition-action style rules. We consider the problem of statically verifying whether all runs of an artifact system satisfy desirabl...