Towards StarExec in the Cloud

StarExec has been central to much progress in logic solvers over the last 10 years. It was recently announced that StarExec Iowa will be decommissioned, and while StarExec Miami will continue to operate while funding is available, it will not be able to support all the logic solver communities currently using the larger StarExec Iowa. In the long term StarExec will necessarily have to migrate to new compute environments. This paper describes work being done to reengineer StarExec as a cloud-native application using container technology and infrastructure-as-code practices. The first step has been to containerise StarExec and ATP systems so that they can be run on a broad range of computer platforms. The next step in process is to write a new backend in StarExec so that Kubernetes can be used to orchestrate distribution of StarExec job pairs over whatever compute nodes are available. Supported by an Amazon Research Award, a new version of StarExec will be deployed in AWS.