Abstract: 

Program analysis forms an integral part of theorem proving, formal verification or simply showing the absence of bugs. In this talk we present a Turing-complete model of computation, called logically constrained term rewrite systems, and discuss the possibilities to prove certain properties of programs. We focus on the confluence property and how sufficient criteria for it are developed. Additionally, we put emphasis on the automation of these criteria and therefore present our tool crest, including recent experiments.