Proof-Carrying Code (PCC) ist ein 1996 von George Necula und Peter Lee entwickelter, effizienter Algorithmus für Computer, mit dessen Hilfe die Eigenschaften von Anwendungssoftware und insbesondere die Einhaltung von Sicherheitsrichtlinien überprüft und verifiziert werden können. Der automatische Algorithmus benutzt ein Axiomensystem, um den P...