Achtung:

Sie haben Javascript deaktiviert!
Sie haben versucht eine Funktion zu nutzen, die nur mit Javascript möglich ist. Um sämtliche Funktionalitäten unserer Internetseite zu nutzen, aktivieren Sie bitte Javascript in Ihrem Browser.

Info-Icon Diese Seite ist nicht in Deutsch verfügbar

CRC 901 – On-The-Fly Computing (OTF Computing)

Software Certification Tools (SoCeTs)

The Software Certification Tools (SoCeTs) are extensions/components of the existing software analysis tool CPAchecker. The extensions to CPAchecker integrate our proof carrying code and programs-from-proofs approaches. The proof-carrying code extensions is also part of the OTF Proof-of-Concept.

Former Developers:

  • Marie-Christine Jakobs

Current Developers:

  • Manuel Töws
  • Prof. Dr. Heike Wehrheim

Features

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.

Die Universität der Informationsgesellschaft