Currently, the software certification tools consists of two components: a component certification for the integration of PCC into CPAchecker and a second component programs-from-proofs integrating PfP concepts into 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
- Support of various configuarable program analysis
- among others interval, information flow, octagon, predicate, reaching definition, sign, uninitilized variables and value analyses
- Certificate reduction providing different strategies
- Store only a subset of the abstract states
- Reduction of stored information (only value analysis)
- Reduction of property-irrelevant information (only information flow analysis)
- 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
- Partialization of certificates
- Partition of analysis results into several smaller certificates
- Aggregation of partial certificate validation results during validation
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
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 Manuel Töws.