Currently, the software certification tools consists of three components: a component certification for the integration of PCC into CPAchecker, a second component programs-from-proofs integrating PfP concepts into CPAchecker and another component which translates SSL specifications into inputs for the software analysis tool CPAchecker.
This extension integrates the configurable program certification concept with its current improvements into CPAchecker as well other experimental PCC concepts.
- Two forms of certificates: abstract reachability graph or set of abstract states
- Certificate reduction providing different strategies
- Store only a subset of the abstract states
- Block abstraction memoization to store similar subproofs only once
- Certificate compression via ZIP
- Implementation of certificate validation
- Parallization of certificate validation based on various strategies
- Parallel checking
- Parallel certificate reading
- Certificate reading and checking in parallel
This extension provides the necessary components to provide the PfP concept in CPAchecker.
- Transformation of program after verification based on abstract reachability graph (ARG)
- Translation of abstract reachability graph into C program
- Predicate refinement based on failure of dataflow analyses
This extension allows the transformation of specification given in the SFB 901 service specification language into the input language of verification tools. The translations are provided as plugins in SSE. Currently, only a translation from protocol specifications into CPAchecker's specification language - a language based on the BLAST query language - is available. Note that the two languages are not identical and a semantics preserving translation is only possible under certain constraints.
If you have any questions concerning certification in CPAchecker, the integration of programs-from-proofs in CPAchecker or the transformation of SSL specifications into CPAchecker specification, please contact Marie-Christine Jakobs.