CPAchecker
CPAchecker is a framework and tool for formal software verification,[1] and program analysis, of C programs. Some of its ideas and concepts, for example lazy abstraction, were inherited from the software model checker BLAST.[2] CPAchecker is based on the idea of configurable program analysis [3] 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. [4]
One application of CPAchecker is the verification of Linux device drivers.[5]
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.[6]
CPAchecker came first (category Overall) in the 2nd Competition on Software Verification (2013) that was held at TACAS 2013 in Rome.[7]
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
- ↑ Official website of CPAchecker: http://cpachecker.sosy-lab.org
- ↑ Dirk Beyer and Thomas A. Henzinger and Ranjit Jhala and Rupak Majumdar (2007). "The Software Model Checker BLAST: Applications to Software Engineering". International Journal on Software Tools for Technology Transfer 9: 505–525. doi:10.1007/s10009-007-0044-z. http://www.sosy-lab.org/~dbeyer/Publications/2007-STTT.The_Software_Model_Checker_BLAST.pdf.
- ↑ Dirk Beyer and Thomas A. Henzinger and Grégory Théoduloz (2007). "Configurable Software Verification: Concretizing the Convergence of model Checking and program analysis". Springer-Verlag, Heidelberg. ISBN 978-3-540-73367-6. http://www.sosy-lab.org/~dbeyer/Publications/2007-CAV.Configurable_Software_Verification.pdf.
- ↑ Dirk Beyer and M. Erkan Keremoglu (2011). "CPAchecker: A Tool for Configurable Software Verification". Springer-Verlag, Heidelberg. ISBN 978-3-642-22109-5. http://www.sosy-lab.org/~dbeyer/Publications/2011-CAV.CPAchecker_A_Tool_for_Configurable_Software_Verification.pdf.
- ↑ Linux Driver Verification: http://linuxtesting.org/project/ldv
- ↑ Dirk Beyer (2012). "Competition on Software Verification (SV-COMP)". Springer-Verlag, Heidelberg. http://www.sosy-lab.org/~dbeyer/Publications/2012-TACAS.Competition_on_Software_Verification.pdf.
- ↑ Dirk Beyer (2013). "Second Competition on Software Verification (Summary of SV-COMP 2013)". Springer-Verlag, Heidelberg. http://www.sosy-lab.org/~dbeyer/Publications/2013-TACAS.Second_Competition_on_Software_Verification.pdf.
External links
 |  |
