Proof-Carrying Code Usando Cálculo de Hoare

Juliana Carpes ImperialEdward Hermann Haeusler

Since programs source are usually unknown, it is necessary to besure that the code of the program behaves as expected. The ideal solutionwould be verifying the code against a specification of safety policies.However, this can take too much time. Another approach is making the codeitself prove that it is safe. The concept of proof-carrying code (PCC) is basedon this idea: a program carries a proof of its conformity with certain safetypolicies. Therefore, the same formal methods employed in formal verificationof programs can be used in this technology. Due to this fact, this work studieshow Hoare logic applied to source codes written in an imperativeprogramming language can be useful to PCC.

Caso o link acima esteja inválido, faça uma busca pelo texto completo na Web: Buscar na Web

Biblioteca Digital Brasileira de Computação - Contato:
     Mantida por: