CPAchecker

CPAchecker is a tool for configurable software verification, based on the concept of configurable program analysis (CPA). It verifies C programs against specifications such as the reachability of error locations, using techniques like predicate abstraction, explicit-value analysis, k-induction and bounded model checking, which can be combined in configurations.

CPAchecker is developed by the Software and Computational Systems Lab at LMU Munich, written in Java and distributed under the Apache License 2.0. Version 4.2.2 is the latest release and development is ongoing.