CPAlien

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.

Tarballs

• CPAlien-svcomp14.tar.bz2: The version of CPAlien as appearing on SV-COMP'14

People

• Petr Müller
• Tomas Vojnar
• Many thanks to Alexander Driemeyer (University of Passau) for SMG code contribution