CPAlien is an extension of CPAChecker (or an analysis implemented in CPAChecker framework, depending on your point of view), implementing an analysis over Symbolic Memory Graph fomralism introduced in Predator tool. CPAlien is an analysis of C programs manipulating with pointers, and hopefully later, with complex dynamic data structures like trees

CPAChecker, and therefore CPAlien, too is written in Java and is distributed under Apache Licence 2.0.