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.

Certification

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

Programs-from-Proofs

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

&nbs

Contact

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.