Misplaced Pages

CPAchecker

Article snapshot taken from Wikipedia with creative commons attribution-sharealike license. Give it a read and then ask your questions in the chat. We can research this topic together.
Software testing tool written in Java

CPAchecker is a framework and tool for formal software verification, and program analysis, of C programs. Some of its ideas and concepts, for example lazy abstraction, were inherited from the software model checker BLAST. CPAchecker is based on the idea of configurable program analysis which is a concept that allows expression of both model checking and program analysis with one formalism. When executed, CPAchecker performs a reachability analysis, i.e., it checks whether a certain state, which violates a given specification, can potentially be reached.

One application of CPAchecker is the verification of Linux device drivers.

Achievements

CPAchecker came first in two categories (Overall and ControlFlowInteger) in the 1st Competition on Software Verification (2012) that was held at TACAS 2012 in Tallinn.

CPAchecker came first (category Overall) in the 2nd Competition on Software Verification (2013) that was held at TACAS 2013 in Rome.

Architecture

CPAchecker operates on a control-flow automaton (CFA); before a given C program can be analyzed by the CPA algorithm, it gets transformed into a CFA. A CFA is a directed graph whose edges represent either assumptions or assignments and its nodes represent program locations.

References

  1. Official website of CPAchecker: http://cpachecker.sosy-lab.org
  2. Dirk Beyer and Thomas A. Henzinger and Ranjit Jhala and Rupak Majumdar (2007). "The Software Model Checker BLAST: Applications to Software Engineering" (PDF). International Journal on Software Tools for Technology Transfer. 9: 505–525. doi:10.1007/s10009-007-0044-z. S2CID 1662778.
  3. Dirk Beyer and Thomas A. Henzinger and Grégory Théoduloz (2007). "Configurable Software Verification: Concretizing the Convergence of model Checking and program analysis" (PDF). Proceedings of the 19th International Conference on Computer Aided Verification. Springer-Verlag, Heidelberg. ISBN 978-3-540-73367-6.
  4. Dirk Beyer and M. Erkan Keremoglu (2011). "CPAchecker: A Tool for Configurable Software Verification" (PDF). Proceedings of the 23rd International Conference on Computer Aided Verification. Springer-Verlag, Heidelberg. ISBN 978-3-642-22109-5.
  5. Linux Driver Verification: http://linuxtesting.org/project/ldv
  6. Dirk Beyer (2012). "Competition on Software Verification (SV-COMP)" (PDF). Proceedings of the 18th International Conference on Tools and Algorithms for the Construction and of Analysis Systems. Springer-Verlag, Heidelberg.
  7. Dirk Beyer (2013). "Second Competition on Software Verification (Summary of SV-COMP 2013)" (PDF). Proceedings of the 19th International Conference on Tools and Algorithms for the Construction and of Analysis Systems. Springer-Verlag, Heidelberg.

External links

Categories: